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