scheme :: AFINSQ_1:sch 3
IndXSeq{ P1[ XFinSequence] } :
for p being XFinSequence holds P1[p]
provided
A1: P1[ {} ] and
A2: for p being XFinSequence
for x being object st P1[p] holds
P1[p ^ <%x%>]