scheme :: FINSEQ_1:sch 3
IndSeq{ P1[ FinSequence] } :
for p being FinSequence holds P1[p]
provided
A1: P1[ {} ] and
A2: for p being FinSequence
for x being object st P1[p] holds
P1[p ^ <*x*>]