scheme :: NAT_1:sch 2
NatInd{ P1[ Nat] } :
for k being Nat holds P1[k]
provided
A1: P1[ 0 ] and
A2: for k being Nat st P1[k] holds
P1[k + 1]