1. m : 
2. k : 
3. f : (m+1)(k+1)
4. Inj((m+1); (k+1); f)
5. Surj((m+1); (k+1); f)
6. b : k
7. a : (m+1)
8. f(a) = b
9. c : (m+1)
10. f(c) = k
11. a = m
  a:m. (Replace value k by f(m) in f)(a) = b

By:	Witness: c THEN Rewrite by Thm*  Inj((m+1); (k+1); f) Thm*   Thm*  (i:m. f(i) = k  (Replace value k by f(m) in f)(i) = f(m) k)

1

f(m) = b  k

1 step

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