defpred S₁[ FinSequence] means ( $1 is Function-yielding 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 that
A4: ( p is Function-yielding implies P₁[p] ) and
A5: p ^ <*x*> is Function-yielding ; :: thesis: P₁[p ^ <*x*>]
A6: <*x*> . 1 = x by FINSEQ_1:40;
( p is Function-yielding & <*x*> is Function-yielding ) by A5, Th25;
hence P₁[p ^ <*x*>] by A2, A4, A6; :: thesis: verum

end;

A7: S₁[ {} ] by A1;
for p being FinSequence holds S₁[p] from FINSEQ_1:sch 3(A7, A3);
hence for p being Function-yielding FinSequence holds P₁[p] ; :: thesis: verum