set SS = AllSymbolsOf S;
set II = U -InterpretersOf S;
set Strings = (() *) \ ;
set D = [:(),((() *) \ ):];
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 );
let IT1, IT2 be PartFunc of [:(),((() *) \ ):],BOOLEAN; :: thesis: ( ( for x being Element of U -InterpretersOf S
for y being Element of (() *) \ holds
( [x,y] in dom IT1 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 IT1 holds
IT1 . (x,y) = g -NorFunctor (x,y) ) & ( for x being Element of U -InterpretersOf S
for y being Element of (() *) \ holds
( [x,y] in dom IT2 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 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 (() *) \ holds
( [x,y] in dom IT1 iff S1[x,y] ) and
A4: for x being Element of U -InterpretersOf S
for y being Element of (() *) \ st [x,y] in dom IT1 holds
IT1 . (x,y) = H1(x,y) ; :: thesis: ( ex x being Element of U -InterpretersOf S ex y being Element of (() *) \ st
( ( [x,y] in dom IT2 implies ex phi1, phi2 being Element of (() *) \ st
( y = (<*()*> ^ phi1) ^ phi2 & [x,phi1] in dom g & [x,phi2] in dom g ) ) implies ( ex phi1, phi2 being Element of (() *) \ st
( y = (<*()*> ^ 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 (() *) \ 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 (() *) \ holds
( [x,y] in dom IT2 iff S1[x,y] ) and
A6: for x being Element of U -InterpretersOf S
for y being Element of (() *) \ st [x,y] in dom IT2 holds
IT2 . (x,y) = H1(x,y) ; :: thesis: IT1 = IT2
A7: now :: thesis: for x being object st x in dom IT1 holds
x in dom IT2
let x be object ; :: thesis: ( x in dom IT1 implies x in dom IT2 )
assume A8: x in dom IT1 ; :: thesis: x in dom IT2
then reconsider xx = x as Element of [:(),((() *) \ ):] ;
consider x1, x2 being object such that
A9: ( x1 in U -InterpretersOf S & x2 in (() *) \ & xx = [x1,x2] ) by ZFMISC_1:def 2;
reconsider I = x1 as Element of U -InterpretersOf S by A9;
reconsider phi = x2 as Element of (() *) \ by A9;
S1[I,phi] by A3, A8, A9;
hence x in dom IT2 by A5, A9; :: thesis: verum
end;
then A10: dom IT1 c= dom IT2 ;
now :: thesis: for x being object st x in dom IT2 holds
x in dom IT1
let x be object ; :: thesis: ( x in dom IT2 implies x in dom IT1 )
assume A11: x in dom IT2 ; :: thesis: x in dom IT1
then reconsider xx = x as Element of [:(),((() *) \ ):] ;
consider x1, x2 being object such that
A12: ( x1 in U -InterpretersOf S & x2 in (() *) \ & xx = [x1,x2] ) by ZFMISC_1:def 2;
reconsider I = x1 as Element of U -InterpretersOf S by A12;
reconsider phi = x2 as Element of (() *) \ by A12;
S1[I,phi] by A5, A11, A12;
hence x in dom IT1 by ; :: thesis: verum
end;
then A13: dom IT2 c= dom IT1 ;
now :: thesis: for x being object st x in dom IT1 holds
IT1 . x = IT2 . x
let x be object ; :: thesis: ( x in dom IT1 implies IT1 . x = IT2 . x )
assume A14: x in dom IT1 ; :: thesis: IT1 . x = IT2 . x
then reconsider xx = x as Element of [:(),((() *) \ ):] ;
consider x1, x2 being object such that
A15: ( x1 in U -InterpretersOf S & x2 in (() *) \ & xx = [x1,x2] ) by ZFMISC_1:def 2;
reconsider I = x1 as Element of U -InterpretersOf S by A15;
reconsider phi = x2 as Element of (() *) \ by A15;
IT1 . x = IT1 . (I,phi) by A15
.= H1(I,phi) by A4, A15, A14
.= IT2 . (I,phi) by A6, A15, A14, A7
.= IT2 . x by A15 ;
hence IT1 . x = IT2 . x ; :: thesis: verum
end;
hence IT1 = IT2 by ; :: thesis: verum