2. 0<m
3.
P:(
(m-1)
Prop).
3. (
i:(m-1). Dec(P(i)))
3.
3. (
n,k:, f:(n(m-1)), g:(k(m-1)).
3. (increasing(f;n)
3. (& increasing(g;k)
3. (& (
i:n. P(f(i)))
3. (& (
j:k. 
P(g(j)))
3. (& (
i:(m-1). (j:n. i = f(j)) 
(j:k. i = g(j))))
4. P :
mProp
5.
i:m. Dec(P(i))
6. n :
7. k :
8. f :
n(m-1)
9. g :
k(m-1)
10. increasing(f;n)
11. increasing(g;k)
12.
i:n. P(f(i))
13.
j:k. P(g(j))
14.
i:(m-1). (j:n. i = f(j)) (j:k. i = g(j))
15.
P(m-1)
16. i :
m
17.
i = m-1
18.
j:n. i = f(j)
(j:(k+1). i = if j=
k
m-1 else g(j) fi) 
Type{1}
