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
9.
k = 1
10. (
j.f(j))(k-2) = k-2
f(k-1) = k-1
f:((k-1)(k-1)). increasing(f;k-1) (i:(k-1). f(i) = i)
kk
k
i:(k-1). (j.f(j))(i) = i
k = 1
j.f(j))(k-2) = k-2
f(k-1) = 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(k-1) = k-1 | 1 step |
About:
 |  |  |  |  |  |  |  |  |  |