defpred S₁[ Element of NAT , set ] means $2 = $1 |-> a;
A1: for x being Element of NAT ex y being Element of {a} * st S₁[x,y]

proof

let n be Element of NAT ; :: thesis: ex y being Element of {a} * st S₁[n,y]
a is Element of {a} by TARSKI:def 1;
then n |-> a is FinSequence of {a} by FINSEQ_2:77;
then reconsider u = n |-> a as Element of {a} * by FINSEQ_1:def 11;
take u ; :: thesis: S₁[n,u]
thus S₁[n,u] ; :: thesis: verum

end;

ex f being Function of NAT ,({a} * ) st
for x being Element of NAT holds S₁[x,f . x] from FUNCT_2:sch 3(A1);
hence ex b₁ being Function of NAT ,({a} * ) st
for n being Element of NAT holds b₁ . n = n |-> a ; :: thesis: verum