set R = Polish-expression-set (P,A);
set Q = (Polish-expression-set (P,A)) ^^ n;
defpred S₁[ object , object ] means ex p being FinSequence st
( p = $1 & $2 = t ^ p );
A10: for a being object st a in (Polish-expression-set (P,A)) ^^ n holds
ex b being object st
( b in P * & S₁[a,b] )

proof

let a be object ; :: thesis: ( a in (Polish-expression-set (P,A)) ^^ n implies ex b being object st
( b in P * & S₁[a,b] ) )
assume A11: a in (Polish-expression-set (P,A)) ^^ n ; :: thesis: ex b being object st
( b in P * & S₁[a,b] )
then reconsider a = a as FinSequence ;
take b = t ^ a; :: thesis: ( b in P * & S₁[a,b] )
A12: (Polish-expression-set (P,A)) ^^ n c= P * by Th14;
t in P * by A0, Th9, TARSKI:def 3;
hence ( b in P * & S₁[a,b] ) by A11, A12, Th12; :: thesis: verum

end;

consider f being Function of ((Polish-expression-set (P,A)) ^^ n),(P *) such that
A22: for a being object st a in (Polish-expression-set (P,A)) ^^ n holds
S₁[a,f . a] from FUNCT_2:sch 1(A10);
A23: for q being FinSequence st q in (Polish-expression-set (P,A)) ^^ n holds
f . q = t ^ q

proof

let q be FinSequence; :: thesis: ( q in (Polish-expression-set (P,A)) ^^ n implies f . q = t ^ q )
assume q in (Polish-expression-set (P,A)) ^^ n ; :: thesis: f . q = t ^ q
then S₁[q,f . q] by A22;
hence f . q = t ^ q ; :: thesis: verum

end;

take f ; :: thesis: for q being FinSequence st q in dom f holds
f . q = t ^ q
dom f = (Polish-expression-set (P,A)) ^^ n by FUNCT_2:def 1;
hence for q being FinSequence st q in dom f holds
f . q = t ^ q by A23; :: thesis: verum