set R = Polish-expression-set (P,A);
set Q = (Polish-expression-set (P,A)) ^^ n;
defpred S1[ 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 * & S1[a,b] )
proof
let a be
object ;
( a in (Polish-expression-set (P,A)) ^^ n implies ex b being object st
( b in P * & S1[a,b] ) )
assume A11:
a in (Polish-expression-set (P,A)) ^^ n
;
ex b being object st
( b in P * & S1[a,b] )
then reconsider a =
a as
FinSequence ;
take b =
t ^ a;
( b in P * & S1[a,b] )
A12:
(Polish-expression-set (P,A)) ^^ n c= P *
by Th15;
t in P *
by A0, Th10, TARSKI:def 3;
hence
(
b in P * &
S1[
a,
b] )
by A11, A12, Th13;
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
S1[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
take
f
; 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; verum