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 Th61;
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;

consider f being sequence of ({a} *) such that
A2: for x being Element of NAT holds S₁[x,f . x] from FUNCT_2:sch 3(A1);
take f ; :: thesis: for n being Nat holds f . n = n |-> a
let n be Nat; :: thesis: f . n = n |-> a
reconsider nn = n as Element of NAT by ORDINAL1:def 12;
S₁[nn,f . nn] by A2;
hence f . n = n |-> a ; :: thesis: verum