1. a : 
2. (f.<f,y.least x:. f(x)=y>)  (a bij a)aa
3. (fg.fg/f,g. f)  (aa)a bij a
4. f : aa
5. g : aa
6. InvFuns(a;a;f;g)
7. f  a onto a
8. (y.least x:. f(x)=y)  aa
9. InvFuns(a;a;f;y.least x:. f(x)=y)
  <f,y.least x:. f(x)=y> = <f,g>  aa

By:	FwdThru:  Thm*  InvFuns(A;B;f;g)  InvFuns(A;B;f;h)  g = h on [ Hyp:6 | Hyp:9 ]

1

10. g = (y.least x:. f(x)=y)   <f,y.least x:. f(x)=y> = <f,g>  aa

1 step

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