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₁[ 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₁[m] holds
S₁[m + 1]

proof

let m be Nat; :: thesis: ( S₁[m] implies S₁[m + 1] )
assume A3: for n being Nat st n <= m holds
N . n c= N . m ; :: thesis: S₁[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 A4, NAT_1:8; :: thesis: verum

end;

A6: S₁[ 0 ] by NAT_1:3;
thus for m being Nat holds S₁[m] from NAT_1:sch 2(A6, A2); :: thesis: verum