scheme :: INT_1:sch 7
FinInd{ F₁() -> Element of NAT , F₂() -> Element of NAT , P₁[ Nat] } :

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

provided

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