scheme :: FUNCT_7:sch 5
FuncSeqInd{ P₁[ object ] } :

for p being Function-yielding FinSequence holds P₁[p]

provided

A1: P₁[ {} ] and
A2: for p being Function-yielding FinSequence st P₁[p] holds
for f being Function holds P₁[p ^ <*f*>]