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. x : a
  (least x@0:. f(x@0)=f(x)) = x  a

By:	Use:[b:= a | y:= f(x)] Inst: Thm*  f:(a onto b), y:b. f(least x:. f(x)=y) = y

1

10. f(least x@0:. f(x@0)=f(x)) = f(x)   (least x@0:. f(x@0)=f(x)) = x  a

3 steps

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