let i, j be Nat; :: thesis: ( i <= j implies ex k being Nat st j = i + k )
defpred S₁[ Nat] means ( i <= $1 implies ex k being Nat st $1 = i + k );
A1: S₁[ 0 ]

proof

assume A2: i <= 0 ; :: thesis: ex k being Nat st 0 = i + k
take 0 ; :: thesis: 0 = i + 0
thus 0 = i + 0 by A2, Th2; :: thesis: verum

end;

A3: for j being Nat st S₁[j] holds
S₁[j + 1]

proof

let j be Nat; :: thesis: ( S₁[j] implies S₁[j + 1] )
assume A4: ( i <= j implies ex k being Nat st j = i + k ) ; :: thesis: S₁[j + 1]
assume A5: i <= j + 1 ; :: thesis: ex k being Nat st j + 1 = i + k

A6: now

assume i <= j ; :: thesis: ex k being Nat st j + 1 = i + k
then consider k being Nat such that
A7: j = i + k by A4;
(i + k) + 1 = i + (k + 1) ;
hence ex k being Nat st j + 1 = i + k by A7; :: thesis: verum

end;

now

assume i = j + 1 ; :: thesis: ex k being Nat st j + 1 = i + k
then j + 1 = i + 0 ;
hence ex k being Nat st j + 1 = i + k ; :: thesis: verum

end;

hence ex k being Nat st j + 1 = i + k by A5, A6, Th8; :: thesis: verum

end;

for j being Nat holds S₁[j] from NAT_1:sch 2(A1, A3);
hence ( i <= j implies ex k being Nat st j = i + k ) ; :: thesis: verum