scheme :: AFINSQ_2:sch 2
Sch5{ F₁() -> set , P₁[ set ] } :

for F being XFinSequence of F₁() holds P₁[F]

provided

A1: P₁[ <%> F₁()] and
A2: for F being XFinSequence of F₁()
for d being Element of F₁() st P₁[F] holds
P₁[F ^ <%d%>]