1. b : 
2. a : 
3. f:(a onto b). (y.least x:. f(x)=y)  b inj a
4. f : (a onto b)
5. (y.least x:. f(x)=y)  b inj a
  (b inj a)

By:	UseWitness (y.least x:. f(x)=y)

None

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