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: for j being Nat st S₁[j] holds
S₁[j + 1]

proof

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

per cases ( i <= j or i = j + 1 ) by A3, NAT_1:8;

suppose i <= j ; :: thesis: ex k being Nat st j + 1 = i + k

then consider k being Nat such that
A4: j = i + k by A2;
reconsider k1 = k + 1 as Nat ;
take k1 ; :: thesis: j + 1 = i + k1
thus j + 1 = i + k1 by A4; :: thesis: verum

end;

suppose B1: i = j + 1 ; :: thesis: ex k being Nat st j + 1 = i + k

reconsider k1 = 0 as Nat ;
take k1 ; :: thesis: j + 1 = i + k1
thus j + 1 = i + k1 by B1; :: thesis: verum

end;

end;

end;

A6: S₁[ 0 ]

proof

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

end;

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