let f be Function; ( ( for i being Nat holds f . (i + 1) c= f . i ) implies for i, j being Nat st i <= j holds
f . j c= f . i )
assume A1:
for i being Nat holds f . (i + 1) c= f . i
; for i, j being Nat st i <= j holds
f . j c= f . i
let i, j be Nat; ( i <= j implies f . j c= f . i )
defpred S1[ Nat] means ( i + $1 <= j implies f . (i + $1) c= f . i );
A2:
now for k being Nat st S1[k] holds
S1[k + 1]end;
A5:
S1[ 0 ]
;
A6:
for k being Nat holds S1[k]
from NAT_1:sch 2(A5, A2);
assume
i <= j
; f . j c= f . i
then consider k being Nat such that
A7:
i + k = j
by NAT_1:10;
thus
f . j c= f . i
by A6, A7; verum