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.
k
7.
(k-1)
8. f(k-1)<k
9. i1 :
(k-1)
f(i1) 
(k-1)
f:((k-1)(k-1)). increasing(f;k-1) (i:(k-1). f(i) = i)
kk
k
(k-1)
(k-1)
f(i1) (k-1)| By: |
(  i.
(FwdThru Thm* k:, f:(k). increasing(f;k) (x,y:k. x<y f(x)<f(y))
([i]) |
| 1 |
x,y:k. x<y f(x)<f(y)
f(i1) (k-1) | 1 step |
About:
 |  |  |  |  |  |  |  |  |  |