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

let p be FinSequence; :: thesis:
let x be object ; :: thesis:
assume A4: S₁[p] ; :: thesis:
assume A5: p ^ <*x*> in F₁() ; :: thesis:
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:

end;