let k be Nat; :: thesis: P_{1}[k]

defpred S_{1}[ Nat] means ( P_{1}[$1] & P_{1}[$1 + 1] );

A4: for k being Nat st S_{1}[k] holds

S_{1}[k + 1]
_{1}[ 0 ]
by A1, A2;

for k being Nat holds S_{1}[k]
from NAT_1:sch 2(A6, A4);

hence P_{1}[k]
; :: thesis: verum

defpred S

A4: for k being Nat st S

S

proof

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

A5: k + 2 = (k + 1) + 1 ;

assume S_{1}[k]
; :: thesis: S_{1}[k + 1]

hence S_{1}[k + 1]
by A3, A5; :: thesis: verum

end;A5: k + 2 = (k + 1) + 1 ;

assume S

hence S

for k being Nat holds S

hence P