set SS = AllSymbolsOf S;
set II = U -InterpretersOf S;
set Strings = ((AllSymbolsOf S) *) \ {{}};
set D = [:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):];
deffunc H1( Element of U -InterpretersOf S, Element of ((AllSymbolsOf S) *) \ {{}}) -> Element of BOOLEAN = g -NorFunctor ($1,$2);
defpred S1[ 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; ( ( 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 S1[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) = H1(x,y)
; ( 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 S1[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) = H1(x,y)
; IT1 = IT2
then A10:
dom IT1 c= dom IT2
;
then A13:
dom IT2 c= dom IT1
;
now for x being object st x in dom IT1 holds
IT1 . x = IT2 . xlet x be
object ;
( x in dom IT1 implies IT1 . x = IT2 . x )assume A14:
x in dom IT1
;
IT1 . x = IT2 . xthen 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
.=
H1(
I,
phi)
by A4, A15, A14
.=
IT2 . (
I,
phi)
by A6, A15, A14, A7
.=
IT2 . x
by A15
;
hence
IT1 . x = IT2 . x
;
verum end;
hence
IT1 = IT2
by FUNCT_1:2, A10, XBOOLE_0:def 10, A13; verum