let i, j be natural Number ; ( i <= j implies ex k being Nat st j = i + k )
A0:
j is Nat
by TARSKI:1;
defpred S1[ Nat] means ( i <= $1 implies ex k being Nat st $1 = i + k );
A1:
for j being Nat st S1[j] holds
S1[j + 1]
proof
let j be
Nat;
( S1[j] implies S1[j + 1] )
assume A2:
(
i <= j implies ex
k being
Nat st
j = i + k )
;
S1[j + 1]
A3:
now ( i <= j implies S1[j + 1] )assume
i <= j
;
S1[j + 1]then consider k being
Nat such that A4:
j = i + k
by A2;
(i + k) + 1
= i + (k + 1)
;
hence
S1[
j + 1]
by A4;
verum end;
A5:
now ( i = j + 1 implies S1[j + 1] )assume
i = j + 1
;
S1[j + 1]then
j + 1
= i + 0
;
hence
S1[
j + 1]
;
verum end;
assume
i <= j + 1
;
ex k being Nat st j + 1 = i + k
hence
ex
k being
Nat st
j + 1
= i + k
by A3, A5, Th8;
verum
end;
A6:
S1[ 0 ]
for j being Nat holds S1[j]
from NAT_1:sch 2(A6, A1);
hence
( i <= j implies ex k being Nat st j = i + k )
by A0; verum