scheme :: NAT_1:sch 10
Indfrom1{ P₁[ Nat] } :

for k being non zero Nat holds P₁[k]

provided

A1: P₁[1] and
A2: for k being non zero Nat st P₁[k] holds
P₁[k + 1]