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

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

provided

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