scheme :: NUMBER17:sch 1
STEP2a{ F₁() -> Nat, P₁[ Nat] } :

for k being Nat st k >= F₁() holds
P₁[k]

provided

A1: P₁[F₁()] and
A2: P₁[F₁() + 1] and
A3: for k being Nat st k >= F₁() & P₁[k] & P₁[k + 1] holds
P₁[k + 2]