1. k : 
2. 0<k
3. f:((k-1)(k-1)). increasing(f;k-1)  (i:(k-1). f(i) = i)
4. f : kk
5. increasing(f;k)
6. i : k
7. i:(k-1). (j.f(j))(i) = i
8. i = k-1
  f(i) = i

1

f(k-1) = k-1

5 steps

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