1. A : Type
2. B : Type
3. f : AB
4. Surj(A; B; f)  [not for witness]
5. a : 
6. s : aA
7. Surj(a; A; s)  [not for witness]
8. B Discrete
9. f o s  aB
10. Surj(a; B; f o s)  [not for witness]
11. e : BB
12. x,y:B. (x e y)  x = y
13. b : B
14. (i.((f o s)(i)) e b)  {p:(a)| i:a. p(i) }
  a:A. f(a) = b

By:	(least i:. ((f o s)(i)) e b)  a  Asserted THEN Witness: s(least i:. ((f o s)(i)) e b)

1	(least i:. ((f o s)(i)) e b)  a	1 step
2	4. Surj(A; B; f) 5. a :  6. s : aA 7. Surj(a; A; s) 8. B Discrete 9. f o s  aB 10. Surj(a; B; f o s) 11. e : BB 12. x,y:B. (x e y)  x = y 13. b : B 14. (i.((f o s)(i)) e b)  {p:(a)| i:a. p(i) } 15. (least i:. ((f o s)(i)) e b)  a   f(s(least i:. ((f o s)(i)) e b)) = b	2 steps

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