set SS = AllSymbolsOf S;

set II = U -InterpretersOf S;

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

set D = [:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):];

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

defpred S_{1}[ 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_{1}[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_{1}(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_{1}[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_{1}(x,y)
; :: thesis: IT1 = IT2

set II = U -InterpretersOf S;

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

set D = [:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):];

deffunc H

defpred S

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

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] 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

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

A7: now :: thesis: for x being object st x in dom IT1 holds

x in dom IT2

then A10:
dom IT1 c= dom IT2
;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 [:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):] ;

consider x1, x2 being object such that

A9: ( 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 A9;

reconsider phi = x2 as Element of ((AllSymbolsOf S) *) \ {{}} by A9;

S_{1}[I,phi]
by A3, A8, A9;

hence x in dom IT2 by A5, A9; :: thesis: verum

end;assume A8: 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 object such that

A9: ( 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 A9;

reconsider phi = x2 as Element of ((AllSymbolsOf S) *) \ {{}} by A9;

S

hence x in dom IT2 by A5, A9; :: thesis: verum

now :: thesis: for x being object st x in dom IT2 holds

x in dom IT1

then A13:
dom IT2 c= dom IT1
;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 [:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):] ;

consider x1, x2 being object such that

A12: ( 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 A12;

reconsider phi = x2 as Element of ((AllSymbolsOf S) *) \ {{}} by A12;

S_{1}[I,phi]
by A5, A11, A12;

hence x in dom IT1 by A3, A12; :: thesis: verum

end;assume A11: 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 object such that

A12: ( 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 A12;

reconsider phi = x2 as Element of ((AllSymbolsOf S) *) \ {{}} by A12;

S

hence x in dom IT1 by A3, A12; :: thesis: verum

now :: thesis: for x being object st x in dom IT1 holds

IT1 . x = IT2 . x

hence
IT1 = IT2
by FUNCT_1:2, A10, XBOOLE_0:def 10, A13; :: thesis: verumIT1 . 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 [:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):] ;

consider x1, x2 being object such that

A15: ( 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 A15;

reconsider phi = x2 as Element of ((AllSymbolsOf S) *) \ {{}} by A15;

IT1 . x = IT1 . (I,phi) by A15

.= H_{1}(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;assume A14: 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 object such that

A15: ( 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 A15;

reconsider phi = x2 as Element of ((AllSymbolsOf S) *) \ {{}} by A15;

IT1 . x = IT1 . (I,phi) by A15

.= H

.= IT2 . (I,phi) by A6, A15, A14, A7

.= IT2 . x by A15 ;

hence IT1 . x = IT2 . x ; :: thesis: verum