let N be Function; :: thesis: ( ( for n being Nat holds N . n c= N . (n + 1) ) implies for m, n being Nat st n <= m holds

N . n c= N . m )

defpred S_{1}[ Nat] means for n being Nat st n <= $1 holds

N . n c= N . $1;

assume A1: for n being Nat holds N . n c= N . (n + 1) ; :: thesis: for m, n being Nat st n <= m holds

N . n c= N . m

A2: for m being Nat st S_{1}[m] holds

S_{1}[m + 1]
_{1}[ 0 ]
by NAT_1:3;

thus for m being Nat holds S_{1}[m]
from NAT_1:sch 2(A6, A2); :: thesis: verum

N . n c= N . m )

defpred S

N . n c= N . $1;

assume A1: for n being Nat holds N . n c= N . (n + 1) ; :: thesis: for m, n being Nat st n <= m holds

N . n c= N . m

A2: for m being Nat st S

S

proof

A6:
S
let m be Nat; :: thesis: ( S_{1}[m] implies S_{1}[m + 1] )

assume A3: for n being Nat st n <= m holds

N . n c= N . m ; :: thesis: S_{1}[m + 1]

let n be Nat; :: thesis: ( n <= m + 1 implies N . n c= N . (m + 1) )

A4: ( n <= m implies N . n c= N . (m + 1) )

hence N . n c= N . (m + 1) by A4, NAT_1:8; :: thesis: verum

end;assume A3: for n being Nat st n <= m holds

N . n c= N . m ; :: thesis: S

let n be Nat; :: thesis: ( n <= m + 1 implies N . n c= N . (m + 1) )

A4: ( n <= m implies N . n c= N . (m + 1) )

proof

assume
n <= m + 1
; :: thesis: N . n c= N . (m + 1)
assume
n <= m
; :: thesis: N . n c= N . (m + 1)

then A5: N . n c= N . m by A3;

N . m c= N . (m + 1) by A1;

hence N . n c= N . (m + 1) by A5; :: thesis: verum

end;then A5: N . n c= N . m by A3;

N . m c= N . (m + 1) by A1;

hence N . n c= N . (m + 1) by A5; :: thesis: verum

hence N . n c= N . (m + 1) by A4, NAT_1:8; :: thesis: verum

thus for m being Nat holds S