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

proof

let i be Nat; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume A4: 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 A5: len p = i + 1 ; :: thesis: P₁[p]
then consider q being FinSequence of F₁(), x being Element of F₁() such that
A6: p = q ^ <*x*> by Th17;
len p = (len q) + 1 by A6, Th14;
hence P₁[p] by A2, A4, A5, A6; :: thesis: verum

end;

let p be FinSequence of F₁(); :: thesis: P₁[p]
A7: len p = len p ;
A8: S₁[ 0 ]

proof

let p be FinSequence of F₁(); :: thesis: ( len p = 0 implies P₁[p] )
assume len p = 0 ; :: thesis: P₁[p]
then p = <*> F₁() ;
hence P₁[p] by A1; :: thesis: verum

end;

for i being Nat holds S₁[i] from NAT_1:sch 2(A8, A3);
hence P₁[p] by A7; :: thesis: verum