scheme :: FUNCT_7:sch 5
FuncSeqInd{ P1[ object ] } :
for p being Function-yielding FinSequence holds P1[p]
provided
A1: P1[ {} ] and
A2: for p being Function-yielding FinSequence st P1[p] holds
for f being Function holds P1[p ^ <*f*>]