1. A : Type
2. A' : Type
3. B : Type
4. B' : Type
5. f1 : AA'
6. g1 : A'A
7. InvFuns(A;A';f1;g1)
8. f : BB'
9. g : B'B
10. InvFuns(B;B';f;g)
11. x:B. g(f(x)) = x
12. y:B'. f(g(y)) = y
13. x:A. g1(f1(x)) = x
14. y:A'. f1(g1(y)) = y
15. Surj(A; A'; f1)
16. Surj(A'; A; g1)
17. Surj(B; B'; f)
18. Surj(B'; B; g)
19. (h.f o h o g1)  (A onto B)A' onto B'
20. (h.g o h o f1)  (A' onto B')A onto B
  InvFuns(A onto B;A' onto B';h.f o h o g1;h.g o h o f1)

1	21. x : A onto B   g o f o x o g1 o f1 = x  A onto B	5 steps
2	21. y : A' onto B'   f o g o y o f1 o g1 = y  A' onto B'	1 step

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