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 S1[ 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 S1[m] holds
S1[m + 1]
proof
let m be Nat; :: thesis: ( S1[m] implies S1[m + 1] )
assume A3: for n being Nat st n <= m holds
N . n c= N . m ; :: thesis: S1[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) )
proof
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;
assume n <= m + 1 ; :: thesis: N . n c= N . (m + 1)
hence N . n c= N . (m + 1) by ; :: thesis: verum
end;
A6: S1[ 0 ] by NAT_1:3;
thus for m being Nat holds S1[m] from NAT_1:sch 2(A6, A2); :: thesis: verum