Thm*  InvFuns(A;B;f;g)  Surj(A; B; f)

To show Surj(A; B; f) is just to show that

b:B. a:A. f(a) = b

which is witnessed by g(b) thus:

b:B. f(g(b)) = b, which is implicit in our assumption.

About: IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html