Proving the LOOP function

We must demonstrate that our guess is good, i.e.

   f = [WHILE]
     = ( R < Y --> ident ) | ( R >= Y and Y > 0 --> Q,R := Q+R/Y, R mod Y )

1. show f behaves like identity when the loop boolean is false
2. show dom(f) = dom([WHILE])