scheme :: BSPACE:sch 1
IndSeqS{ F1() -> 1-sorted , P1[ set ] } :
for p being FinSequence of F1() holds P1[p]
provided
A1: P1[ <*> F1()] and
A2: for p being FinSequence of F1()
for x being Element of F1() st P1[p] holds
P1[p ^ <*x*>]