defpred S₁[ set ] means for p being FinSequence of F₁() st len p = $1 holds
P₁[p];
A3: S₁[ 0 ] by A1, FINSEQ_1:32;
A4: for i being Nat st S₁[i] holds
S₁[i + 1]

proof

let i be Nat; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume A5: for p being FinSequence of F₁() st len p = i holds
P₁[p] ; :: thesis: S₁[i + 1]
let p be FinSequence of F₁(); :: thesis: ( len p = i + 1 implies P₁[p] )
assume A6: len p = i + 1 ; :: thesis: P₁[p]
then consider q being FinSequence of F₁(), x being Element of F₁() such that
A7: p = q ^ <*x*> by Th22;
len p = (len q) + 1 by A7, Th19;
hence P₁[p] by A2, A5, A6, A7; :: thesis: verum

end;

A8: for i being Nat holds S₁[i] from NAT_1:sch 2(A3, A4);
let p be FinSequence of F₁(); :: thesis: P₁[p]
len p = len p ;
hence P₁[p] by A8; :: thesis: verum