defpred S₁[ FinSequence] means ( $1 in F₁() implies P₁[$1] );
A3: for p being FinSequence
for x being set st S₁[p] holds
S₁[p ^ <*x*>]

proof

let p be FinSequence; :: thesis: for x being set st S₁[p] holds
S₁[p ^ <*x*>]
let x be set ; :: thesis: ( S₁[p] implies S₁[p ^ <*x*>] )
assume A4: S₁[p] ; :: thesis: S₁[p ^ <*x*>]
assume A5: p ^ <*x*> in F₁() ; :: thesis: P₁[p ^ <*x*>]
then reconsider h = p ^ <*x*> as FinSequence of NAT by TREES_1:19;
consider g being FinSequence of NAT , n being Element of NAT such that
A6: h = g ^ <*n*> by Th4;
A7: g = p by A6, FINSEQ_2:17;
reconsider g = g as Element of F₁() by A5, A6, TREES_1:21;
P₁[g] by A4, A7;
hence P₁[p ^ <*x*>] by A2, A5, A6; :: thesis: verum

end;

A8: S₁[ {} ] by A1;
for p being FinSequence holds S₁[p] from FINSEQ_1:sch 3(A8, A3);
hence for f being Element of F₁() holds P₁[f] ; :: thesis: verum