1. a : 
2. f : a bij a
  InvFuns(a;a;f;y.least x:. f(x)=y)

By:	f  a onto a  By BackThru: Thm*  (A bij B)  (A onto B) THEN f  a bij a  Asserted THEN Analyze-1

1

3. f  a onto a 4. f  aa 5. Bij(a; a; f)  [not for witness]   InvFuns(a;a;f;y.least x:. f(x)=y)

7 steps

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