scheme :: PRE_POLY:sch 1
Regr1{ F₁() -> Nat, P₁[ set ] } :

for k being Element of NAT st k <= F₁() holds
P₁[k]

provided

A1: P₁[F₁()] and
A2: for k being Element of NAT st k < F₁() & P₁[k + 1] holds
P₁[k]