set SS = AllSymbolsOf S;
set II = U -InterpretersOf S;
set Strings = ((AllSymbolsOf S) *) \ {{}};
set D = [:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):];
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 );
let IT1, IT2 be PartFunc of [:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],BOOLEAN; :: thesis: ( ( for x being Element of U -InterpretersOf S
for y being Element of ((AllSymbolsOf S) *) \ {{}} holds
( [x,y] in dom IT1 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 IT1 holds
IT1 . (x,y) = g -NorFunctor (x,y) ) & ( for x being Element of U -InterpretersOf S
for y being Element of ((AllSymbolsOf S) *) \ {{}} holds
( [x,y] in dom IT2 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 IT2 holds
IT2 . (x,y) = g -NorFunctor (x,y) ) implies IT1 = IT2 )
assume that
A3: for x being Element of U -InterpretersOf S
for y being Element of ((AllSymbolsOf S) *) \ {{}} holds
( [x,y] in dom IT1 iff S₁[x,y] ) and
A4: for x being Element of U -InterpretersOf S
for y being Element of ((AllSymbolsOf S) *) \ {{}} st [x,y] in dom IT1 holds
IT1 . (x,y) = H₁(x,y) ; :: thesis: ( ex x being Element of U -InterpretersOf S ex y being Element of ((AllSymbolsOf S) *) \ {{}} st
( ( [x,y] in dom IT2 implies ex phi1, phi2 being Element of ((AllSymbolsOf S) *) \ {{}} st
( y = (<*(TheNorSymbOf S)*> ^ phi1) ^ phi2 & [x,phi1] in dom g & [x,phi2] in dom g ) ) implies ( ex phi1, phi2 being Element of ((AllSymbolsOf S) *) \ {{}} st
( y = (<*(TheNorSymbOf S)*> ^ phi1) ^ phi2 & [x,phi1] in dom g & [x,phi2] in dom g ) & not [x,y] in dom IT2 ) ) or ex x being Element of U -InterpretersOf S ex y being Element of ((AllSymbolsOf S) *) \ {{}} st
( [x,y] in dom IT2 & not IT2 . (x,y) = g -NorFunctor (x,y) ) or IT1 = IT2 )
assume that
A5: for x being Element of U -InterpretersOf S
for y being Element of ((AllSymbolsOf S) *) \ {{}} holds
( [x,y] in dom IT2 iff S₁[x,y] ) and
A6: for x being Element of U -InterpretersOf S
for y being Element of ((AllSymbolsOf S) *) \ {{}} st [x,y] in dom IT2 holds
IT2 . (x,y) = H₁(x,y) ; :: thesis: IT1 = IT2

now :: thesis: for x being set st x in dom IT1 holds
x in dom IT2

let x be set ; :: thesis: ( x in dom IT1 implies x in dom IT2 )
assume A7: x in dom IT1 ; :: thesis: x in dom IT2
then reconsider xx = x as Element of [:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):] ;
consider x1, x2 being set such that
A8: ( x1 in U -InterpretersOf S & x2 in ((AllSymbolsOf S) *) \ {{}} & xx = [x1,x2] ) by ZFMISC_1:def 2;
reconsider I = x1 as Element of U -InterpretersOf S by A8;
reconsider phi = x2 as Element of ((AllSymbolsOf S) *) \ {{}} by A8;
S₁[I,phi] by A3, A7, A8;
hence x in dom IT2 by A5, A8; :: thesis: verum

end;

then A9: dom IT1 c= dom IT2 by TARSKI:def 3;

now :: thesis: for x being set st x in dom IT2 holds
x in dom IT1

let x be set ; :: thesis: ( x in dom IT2 implies x in dom IT1 )
assume A10: x in dom IT2 ; :: thesis: x in dom IT1
then reconsider xx = x as Element of [:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):] ;
consider x1, x2 being set such that
A11: ( x1 in U -InterpretersOf S & x2 in ((AllSymbolsOf S) *) \ {{}} & xx = [x1,x2] ) by ZFMISC_1:def 2;
reconsider I = x1 as Element of U -InterpretersOf S by A11;
reconsider phi = x2 as Element of ((AllSymbolsOf S) *) \ {{}} by A11;
S₁[I,phi] by A5, A10, A11;
hence x in dom IT1 by A3, A11; :: thesis: verum

end;

then dom IT2 c= dom IT1 by TARSKI:def 3;
then A12: dom IT2 = dom IT1 by A9, XBOOLE_0:def 10;

now :: thesis: for x being set st x in dom IT1 holds
IT1 . x = IT2 . x

let x be set ; :: thesis: ( x in dom IT1 implies IT1 . x = IT2 . x )
assume A13: x in dom IT1 ; :: thesis: IT1 . x = IT2 . x
then reconsider xx = x as Element of [:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):] ;
consider x1, x2 being set such that
A14: ( x1 in U -InterpretersOf S & x2 in ((AllSymbolsOf S) *) \ {{}} & xx = [x1,x2] ) by ZFMISC_1:def 2;
reconsider I = x1 as Element of U -InterpretersOf S by A14;
reconsider phi = x2 as Element of ((AllSymbolsOf S) *) \ {{}} by A14;
IT1 . x = IT1 . (I,phi) by A14
.= H₁(I,phi) by A4, A14, A13
.= IT2 . (I,phi) by A6, A14, A13, A9
.= IT2 . x by A14 ;
hence IT1 . x = IT2 . x ; :: thesis: verum

end;

hence IT1 = IT2 by A12, FUNCT_1:2; :: thesis: verum