scheme :: INT_1:sch 8
FinInd2{ 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₂() & ( for j9 being Element of NAT st F₁() <= j9 & j9 <= j holds
P₁[j9] ) holds
P₁[j + 1]