1. P : Prop
2. Q : Prop
3. f : {u:| P(u) }{v:| Q(v) }
4. Inj({u:| P(u) }; {v:| Q(v) }; f)
5. Surj({u:| P(u) }; {v:| Q(v) }; f)
6. m : {u:| P(u) }
7. k : {v:| Q(v) }
  Surj({u:| P(u) & u = m }; {v:| Q(v) & v = k };
  Surj(Replace value k by f(m) in f)

By:	(Replace value k by f(m) in f)  {u:| P(u) & u = m   }{v:| Q(v) & v = k   } Asserted THEN Analyze

1

8. (Replace value k by f(m) in f)  {u:| P(u) & u = m }{v:| Q(v) & v = k } 9. b : {v:| Q(v) & v = k }   a:{u:| P(u) & u = m }. (Replace value k by f(m) in f)(a) = b

8 steps

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