defpred S₁[ FinSequence] means ( $1 is Function-yielding implies P₁[$1] );
A3: S₁[ {} ] by A1;
A4: 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
A5: ( p is Function-yielding implies P₁[p] ) and
A6: p ^ <*x*> is Function-yielding ; :: thesis: P₁[p ^ <*x*>]
A7: ( <*x*> . 1 = x & dom <*x*> = {1} ) by FINSEQ_1:4, FINSEQ_1:55, FINSEQ_1:57;
then ( p is Function-yielding & <*x*> is Function-yielding & 1 in dom <*x*> ) by A6, Th25, TARSKI:def 1;
hence P₁[p ^ <*x*>] by A2, A5, A7; :: thesis: verum

end;

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