scheme :: AFINSQ_1:sch 3
IndXSeq{ P₁[ XFinSequence] } :

for p being XFinSequence holds P₁[p]

provided

A1: P₁[ {} ] and
A2: for p being XFinSequence
for x being object st P₁[p] holds
P₁[p ^ <%x%>]