scheme :: STACKS_1:sch 1
IndSeqD{ F₁() -> non empty set , P₁[ set ] } :

for p being FinSequence of F₁() holds P₁[p]

provided

A1: P₁[ <*> F₁()] and
A2: for p being FinSequence of F₁()
for x being Element of F₁() st P₁[p] holds
P₁[<*x*> ^ p]