set SS = AllSymbolsOf S;
set II = U -InterpretersOf S;
set Strings = (() *) \ ;
deffunc H1( Element of U -InterpretersOf S, Element of (() *) \ ) -> Element of BOOLEAN = g -ExFunctor (\$1,\$2);
defpred S1[ Element of U -InterpretersOf S, Element of (() *) \ ] means ex v being literal Element of S ex w being string of S st
( [\$1,w] in dom g & \$2 = <*v*> ^ w );
A1: for x being Element of U -InterpretersOf S
for y being Element of (() *) \ st S1[x,y] holds
H1(x,y) in BOOLEAN ;
consider f being PartFunc of [:(),((() *) \ ):],BOOLEAN such that
A2: ( ( for x being Element of U -InterpretersOf S
for y being Element of (() *) \ holds
( [x,y] in dom f iff S1[x,y] ) ) & ( for x being Element of U -InterpretersOf S
for y being Element of (() *) \ st [x,y] in dom f holds
f . (x,y) = H1(x,y) ) ) from take f ; :: thesis: ( ( for x being Element of U -InterpretersOf S
for y being Element of (() *) \ holds
( [x,y] in dom f iff ex v being literal Element of S ex w being string of S st
( [x,w] in dom g & y = <*v*> ^ w ) ) ) & ( for x being Element of U -InterpretersOf S
for y being Element of (() *) \ st [x,y] in dom f holds
f . (x,y) = g -ExFunctor (x,y) ) )

thus ( ( for x being Element of U -InterpretersOf S
for y being Element of (() *) \ holds
( [x,y] in dom f iff ex v being literal Element of S ex w being string of S st
( [x,w] in dom g & y = <*v*> ^ w ) ) ) & ( for x being Element of U -InterpretersOf S
for y being Element of (() *) \ st [x,y] in dom f holds
f . (x,y) = g -ExFunctor (x,y) ) ) by A2; :: thesis: verum