set SS = AllSymbolsOf S;

set II = U -InterpretersOf S;

set Strings = ((AllSymbolsOf S) *) \ {{}};

deffunc H_{1}( Element of U -InterpretersOf S, Element of ((AllSymbolsOf S) *) \ {{}}) -> Element of BOOLEAN = g -ExFunctor ($1,$2);

defpred S_{1}[ 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_{1}[x,y] holds

H_{1}(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_{1}[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_{1}(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

set II = U -InterpretersOf S;

set Strings = ((AllSymbolsOf S) *) \ {{}};

deffunc H

defpred S

( [$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

H

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

for y being Element of ((AllSymbolsOf S) *) \ {{}} st [x,y] in dom f holds

f . (x,y) = H

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