1. B : Type
2. e : BB
3. IsEqFun(B;e)
4. a : 
5. f : aB
6. Surj(a; B; f)
7. f  a onto B
8. (y,x. (f(x)) e y)  B{p:(a)| i:a. p(i) }
9. (y.least x:. (f(x)) e y)  Ba
10. i1 : B
11. i2 : B
12. (least x:. (f(x)) e i1) = (least x:. (f(x)) e i2)
13. f(least x:. (f(x)) e i1) = f(least x:. (f(x)) e i2)
14. f(least x:. (f(x)) e i1) = f(least x:. (f(x)) e i2)
15. y : B
  f(least x:. (f(x)) e y) = y

By:	BackThru:  Thm*  e:(BB).  Thm*  IsEqFun(B;e)  (a:, f:(a onto B), y:B. f(least x:. (f(x)) e y) = y)

None

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