set SS = AllSymbolsOf S;
set II = U -InterpretersOf S;
set Strings = ((AllSymbolsOf S) *) \ {{}};
reconsider g = g as PartFunc of [:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],BOOLEAN ;
deffunc H₁( Element of U -InterpretersOf S, Element of ((AllSymbolsOf S) *) \ {{}}) -> Element of BOOLEAN = g -NorFunctor ($1,$2);
defpred S₁[ Element of U -InterpretersOf S, Element of ((AllSymbolsOf S) *) \ {{}}] means ex phi1, phi2 being Element of ((AllSymbolsOf S) *) \ {{}} st
( $2 = (<*(TheNorSymbOf S)*> ^ phi1) ^ phi2 & [$1,phi1] in dom g & [$1,phi2] in dom g );
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 phi1, phi2 being Element of ((AllSymbolsOf S) *) \ {{}} st
( y = (<*(TheNorSymbOf S)*> ^ phi1) ^ phi2 & [x,phi1] in dom g & [x,phi2] in dom g ) ) ) & ( 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 -NorFunctor (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 phi1, phi2 being Element of ((AllSymbolsOf S) *) \ {{}} st
( y = (<*(TheNorSymbOf S)*> ^ phi1) ^ phi2 & [x,phi1] in dom g & [x,phi2] in dom g ) ) ) & ( 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 -NorFunctor (x,y) ) ) by A2; :: thesis: verum