m,k:, f:((m+1)(k+1)).
  Bij((m+1); (k+1); f)  Bij(m; k; Replace value k by f(m) in f)

1

1. m :  2. k :  3. f : (m+1)(k+1) 4. Inj((m+1); (k+1); f) 5. Surj((m+1); (k+1); f)   Bij(m; k; Replace value k by f(m) in f)

8 steps

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