set SS = AllSymbolsOf S;
set II = U -InterpretersOf S;
set Strings = ((AllSymbolsOf S) *) \ {{}};
deffunc H₁( Element of U -InterpretersOf S, Element of ((AllSymbolsOf S) *) \ {{}}) -> Element of BOOLEAN = g -ExFunctor ($1,$2);
defpred S₁[ Element of U -InterpretersOf S, Element of ((AllSymbolsOf S) *) \ {{}}] 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 ((AllSymbolsOf S) *) \ {{}} st S₁[x,y] holds
H₁(x,y) in BOOLEAN ;
consider f being PartFunc of [:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],BOOLEAN such that
A2: ( ( for x being Element of U -InterpretersOf S
for y being Element of ((AllSymbolsOf S) *) \ {{}} holds
( [x,y] in dom f iff S₁[x,y] ) ) & ( for x being Element of U -InterpretersOf S
for y being Element of ((AllSymbolsOf S) *) \ {{}} st [x,y] in dom f holds
f . (x,y) = H₁(x,y) ) ) from BINOP_1:sch 8(A1);
take f ; :: thesis: ( ( for x being Element of U -InterpretersOf S
for y being Element of ((AllSymbolsOf S) *) \ {{}} 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 ((AllSymbolsOf S) *) \ {{}} 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 ((AllSymbolsOf S) *) \ {{}} 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 ((AllSymbolsOf S) *) \ {{}} st [x,y] in dom f holds
f . (x,y) = g -ExFunctor (x,y) ) ) by A2; :: thesis: verum