let i, j be Nat; :: thesis: ( i <= j implies ex k being Nat st j = i + k )

defpred S_{1}[ Nat] means ( i <= $1 implies ex k being Nat st $1 = i + k );

A1: for j being Nat st S_{1}[j] holds

S_{1}[j + 1]
_{1}[ 0 ]
_{1}[j]
from NAT_1:sch 2(A6, A1);

hence ( i <= j implies ex k being Nat st j = i + k ) ; :: thesis: verum

defpred S

A1: for j being Nat st S

S

proof

A6:
S
let j be Nat; :: thesis: ( S_{1}[j] implies S_{1}[j + 1] )

assume A2: ( i <= j implies ex k being Nat st j = i + k ) ; :: thesis: S_{1}[j + 1]

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

end;assume A2: ( i <= j implies ex k being Nat st j = i + k ) ; :: thesis: S

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

proof

for j being Nat holds S
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;take 0 ; :: thesis: 0 = i + 0

thus 0 = i + 0 by A7; :: thesis: verum

hence ( i <= j implies ex k being Nat st j = i + k ) ; :: thesis: verum