let U be non empty set ; :: thesis: for S1, S2 being Language

for phi1 being 0wff string of S1

for I1 being Element of U -InterpretersOf S1

for I2 being Element of U -InterpretersOf S2 st I1 | ((rng phi1) /\ (OwnSymbolsOf S1)) = I2 | ((rng phi1) /\ (OwnSymbolsOf S1)) & the adicity of S1 | ((rng phi1) /\ (OwnSymbolsOf S1)) = the adicity of S2 | ((rng phi1) /\ (OwnSymbolsOf S1)) & TheEqSymbOf S1 = TheEqSymbOf S2 holds

ex phi2 being 0wff string of S2 st

( phi2 = phi1 & I2 -AtomicEval phi2 = I1 -AtomicEval phi1 )

let S1, S2 be Language; :: thesis: for phi1 being 0wff string of S1

for I1 being Element of U -InterpretersOf S1

for I2 being Element of U -InterpretersOf S2 st I1 | ((rng phi1) /\ (OwnSymbolsOf S1)) = I2 | ((rng phi1) /\ (OwnSymbolsOf S1)) & the adicity of S1 | ((rng phi1) /\ (OwnSymbolsOf S1)) = the adicity of S2 | ((rng phi1) /\ (OwnSymbolsOf S1)) & TheEqSymbOf S1 = TheEqSymbOf S2 holds

ex phi2 being 0wff string of S2 st

( phi2 = phi1 & I2 -AtomicEval phi2 = I1 -AtomicEval phi1 )

set II1 = U -InterpretersOf S1;

set II2 = U -InterpretersOf S2;

set a2 = the adicity of S2;

set F2 = S2 -firstChar ;

set E1 = TheEqSymbOf S1;

set E2 = TheEqSymbOf S2;

set TT1 = AllTermsOf S1;

set TT2 = AllTermsOf S2;

set O1 = OwnSymbolsOf S1;

set O2 = OwnSymbolsOf S2;

set C2 = S2 -multiCat ;

set F1 = S1 -firstChar ;

set TS1 = TermSymbolsOf S1;

set TS2 = TermSymbolsOf S2;

set a1 = the adicity of S1;

set C1 = S1 -multiCat ;

set AS1 = AtomicFormulaSymbolsOf S1;

set AS2 = AtomicFormulaSymbolsOf S2;

set d = U -deltaInterpreter ;

set RR1 = RelSymbolsOf S1;

reconsider TS1 = TermSymbolsOf S1 as non empty Subset of (OwnSymbolsOf S1) by FOMODEL1:1;

reconsider TS2 = TermSymbolsOf S2 as non empty Subset of (OwnSymbolsOf S2) by FOMODEL1:1;

let phi1 be 0wff string of S1; :: thesis: for I1 being Element of U -InterpretersOf S1

for I2 being Element of U -InterpretersOf S2 st I1 | ((rng phi1) /\ (OwnSymbolsOf S1)) = I2 | ((rng phi1) /\ (OwnSymbolsOf S1)) & the adicity of S1 | ((rng phi1) /\ (OwnSymbolsOf S1)) = the adicity of S2 | ((rng phi1) /\ (OwnSymbolsOf S1)) & TheEqSymbOf S1 = TheEqSymbOf S2 holds

ex phi2 being 0wff string of S2 st

( phi2 = phi1 & I2 -AtomicEval phi2 = I1 -AtomicEval phi1 )

let I1 be Element of U -InterpretersOf S1; :: thesis: for I2 being Element of U -InterpretersOf S2 st I1 | ((rng phi1) /\ (OwnSymbolsOf S1)) = I2 | ((rng phi1) /\ (OwnSymbolsOf S1)) & the adicity of S1 | ((rng phi1) /\ (OwnSymbolsOf S1)) = the adicity of S2 | ((rng phi1) /\ (OwnSymbolsOf S1)) & TheEqSymbOf S1 = TheEqSymbOf S2 holds

ex phi2 being 0wff string of S2 st

( phi2 = phi1 & I2 -AtomicEval phi2 = I1 -AtomicEval phi1 )

let I2 be Element of U -InterpretersOf S2; :: thesis: ( I1 | ((rng phi1) /\ (OwnSymbolsOf S1)) = I2 | ((rng phi1) /\ (OwnSymbolsOf S1)) & the adicity of S1 | ((rng phi1) /\ (OwnSymbolsOf S1)) = the adicity of S2 | ((rng phi1) /\ (OwnSymbolsOf S1)) & TheEqSymbOf S1 = TheEqSymbOf S2 implies ex phi2 being 0wff string of S2 st

( phi2 = phi1 & I2 -AtomicEval phi2 = I1 -AtomicEval phi1 ) )

set TE1 = I1 -TermEval ;

set TE2 = I2 -TermEval ;

set X = (rng phi1) /\ (OwnSymbolsOf S1);

assume A1: ( I1 | ((rng phi1) /\ (OwnSymbolsOf S1)) = I2 | ((rng phi1) /\ (OwnSymbolsOf S1)) & the adicity of S1 | ((rng phi1) /\ (OwnSymbolsOf S1)) = the adicity of S2 | ((rng phi1) /\ (OwnSymbolsOf S1)) & TheEqSymbOf S1 = TheEqSymbOf S2 ) ; :: thesis: ex phi2 being 0wff string of S2 st

( phi2 = phi1 & I2 -AtomicEval phi2 = I1 -AtomicEval phi1 )

then A2: (I1 -TermEval) | (((rng phi1) /\ (OwnSymbolsOf S1)) *) = (I2 -TermEval) | (((rng phi1) /\ (OwnSymbolsOf S1)) *) by Th11;

then A3: dom ((I1 -TermEval) | (((rng phi1) /\ (OwnSymbolsOf S1)) *)) = (((rng phi1) /\ (OwnSymbolsOf S1)) *) /\ (dom (I2 -TermEval)) by RELAT_1:61

.= (((rng phi1) /\ (OwnSymbolsOf S1)) *) /\ (AllTermsOf S2) by FUNCT_2:def 1 ;

then A4: (((rng phi1) /\ (OwnSymbolsOf S1)) *) /\ (AllTermsOf S2) = (((rng phi1) /\ (OwnSymbolsOf S1)) *) /\ (dom (I1 -TermEval)) by RELAT_1:61

.= (((rng phi1) /\ (OwnSymbolsOf S1)) *) /\ (AllTermsOf S1) by FUNCT_2:def 1 ;

reconsider r1 = (S1 -firstChar) . phi1 as relational Element of S1 ;

set m = |.(ar r1).|;

set Y1 = ((rng phi1) /\ (OwnSymbolsOf S1)) \/ {(TheEqSymbOf S1)};

set Y2 = ((rng phi1) /\ (OwnSymbolsOf S1)) \/ {(TheEqSymbOf S2)};

{((phi1 null {}) . 1)} \ ((rng phi1) \/ {}) = {} ;

then phi1 . 1 in rng phi1 by ZFMISC_1:60;

then A5: r1 in rng phi1 by FOMODEL0:6;

( r1 in {(TheEqSymbOf S1)} or not r1 in (RelSymbolsOf S1) \ (OwnSymbolsOf S1) ) by FOMODEL1:1;

then A6: ( r1 in {(TheEqSymbOf S1)} or not r1 in RelSymbolsOf S1 or r1 in OwnSymbolsOf S1 ) by XBOOLE_0:def 5;

then ( r1 in {(TheEqSymbOf S1)} or r1 in (rng phi1) /\ (OwnSymbolsOf S1) ) by A5, FOMODEL1:def 17, XBOOLE_0:def 4;

then A7: r1 in ((rng phi1) /\ (OwnSymbolsOf S1)) \/ {(TheEqSymbOf S1)} by XBOOLE_0:def 3;

reconsider t1 = SubTerms phi1 as |.(ar r1).| + 0 -element FinSequence of AllTermsOf S1 by FOMODEL0:26;

t1 is TS1 * -valued ;

then ( t1 in |.(ar r1).| -tuples_on ((OwnSymbolsOf S1) *) & t1 in |.(ar r1).| -tuples_on ((rng phi1) *) ) by FOMODEL0:16;

then t1 in (|.(ar r1).| -tuples_on ((rng phi1) *)) /\ (|.(ar r1).| -tuples_on ((OwnSymbolsOf S1) *)) by XBOOLE_0:def 4;

then t1 in |.(ar r1).| -tuples_on (((rng phi1) *) /\ ((OwnSymbolsOf S1) *)) by FOMODEL0:3;

then t1 in |.(ar r1).| -tuples_on (((rng phi1) /\ (OwnSymbolsOf S1)) *) by FOMODEL0:55;

then A8: ( t1 is ((rng phi1) /\ (OwnSymbolsOf S1)) * -valued & rng t1 c= AllTermsOf S1 ) by FOMODEL0:12, RELAT_1:def 19;

then A9: ( rng t1 c= ((rng phi1) /\ (OwnSymbolsOf S1)) * & rng t1 c= AllTermsOf S1 ) by RELAT_1:def 19;

then A10: rng t1 c= (((rng phi1) /\ (OwnSymbolsOf S1)) *) /\ (AllTermsOf S1) by XBOOLE_1:19;

rng t1 c= (((rng phi1) /\ (OwnSymbolsOf S1)) *) /\ (AllTermsOf S2) by XBOOLE_1:19, A9, A4;

then reconsider X2 = (((rng phi1) /\ (OwnSymbolsOf S1)) *) /\ (AllTermsOf S2) as non empty Subset of (AllTermsOf S2) ;

reconsider X1 = (((rng phi1) /\ (OwnSymbolsOf S1)) *) /\ (AllTermsOf S1) as non empty Subset of (AllTermsOf S1) by A10;

t1 is X2 -valued |.(ar r1).| -element FinSequence by RELAT_1:def 19, A9, A4, XBOOLE_1:19;

then reconsider t2 = t1 as |.(ar r1).| -element FinSequence of X2 by FOMODEL0:26;

t2 is Element of X2 * ;

then reconsider tt2 = t2 as |.(ar r1).| -element Element of (AllTermsOf S2) * ;

reconsider E11 = TheEqSymbOf S1 as Element of AtomicFormulaSymbolsOf S1 by FOMODEL1:def 20;

reconsider EE1 = {E11} as non empty Subset of (AtomicFormulaSymbolsOf S1) ;

reconsider E22 = TheEqSymbOf S2 as Element of AtomicFormulaSymbolsOf S2 by FOMODEL1:def 20;

reconsider EE2 = {E22} as non empty Subset of (AtomicFormulaSymbolsOf S2) ;

set Y1 = ((rng phi1) /\ (OwnSymbolsOf S1)) \/ EE1;

set Y2 = ((rng phi1) /\ (OwnSymbolsOf S1)) \/ EE2;

set f1 = the adicity of S1 | EE1;

set f2 = the adicity of S2 | EE2;

A11: ( dom ( the adicity of S1 | EE1) = EE1 & dom ( the adicity of S2 | EE2) = EE2 ) by PARTFUN1:def 2;

then ( the adicity of S2 | ((rng phi1) /\ (OwnSymbolsOf S1))) +* ( the adicity of S2 | EE2) = the adicity of S1 | (((rng phi1) /\ (OwnSymbolsOf S1)) \/ EE1) by A1, FUNCT_4:78;

then A13: ( ((rng phi1) /\ (OwnSymbolsOf S1)) \/ EE1 = ((rng phi1) /\ (OwnSymbolsOf S1)) \/ EE2 & the adicity of S1 | (((rng phi1) /\ (OwnSymbolsOf S1)) \/ EE1) = the adicity of S2 | (((rng phi1) /\ (OwnSymbolsOf S1)) \/ EE2) ) by FUNCT_4:78, A1;

A14: ar r1 = ( the adicity of S1 | (((rng phi1) /\ (OwnSymbolsOf S1)) \/ EE1)) . r1 by FUNCT_1:49, A7

.= the adicity of S2 . r1 by A7, A13, FUNCT_1:49 ;

then r1 in dom the adicity of S2 by FUNCT_1:def 2;

then r1 in AtomicFormulaSymbolsOf S2 ;

then reconsider r2 = r1 as ofAtomicFormula Element of S2 by FOMODEL1:def 20;

A15: ar r1 = ar r2 by A14;

then reconsider r2 = r2 as relational Element of S2 ;

reconsider phi2 = r2 -compound tt2 as 0wff string of S2 by A15;

take phi2 ; :: thesis: ( phi2 = phi1 & I2 -AtomicEval phi2 = I1 -AtomicEval phi1 )

thus phi1 = <*r1*> ^ ((S1 -multiCat) . t1) by FOMODEL1:def 38

.= phi2 by FOMODEL0:52 ; :: thesis: I2 -AtomicEval phi2 = I1 -AtomicEval phi1

A16: (S2 -firstChar) . phi2 = phi2 . 1 by FOMODEL0:6

.= r2 by FINSEQ_1:41 ;

then reconsider tt22 = tt2 as |.(ar ((S2 -firstChar) . phi2)).| -element Element of (AllTermsOf S2) * by A14;

A17: tt22 = SubTerms phi2 by FOMODEL1:def 38, A16;

A18: (I1 -TermEval) * t1 = ((I1 -TermEval) | (((rng phi1) /\ (OwnSymbolsOf S1)) *)) * t1 by RELAT_1:165, XBOOLE_1:19, A9, A4, A3

.= (I2 -TermEval) * (SubTerms phi2) by A17, A2, A8, RELAT_1:def 19, A3, RELAT_1:165 ;

for phi1 being 0wff string of S1

for I1 being Element of U -InterpretersOf S1

for I2 being Element of U -InterpretersOf S2 st I1 | ((rng phi1) /\ (OwnSymbolsOf S1)) = I2 | ((rng phi1) /\ (OwnSymbolsOf S1)) & the adicity of S1 | ((rng phi1) /\ (OwnSymbolsOf S1)) = the adicity of S2 | ((rng phi1) /\ (OwnSymbolsOf S1)) & TheEqSymbOf S1 = TheEqSymbOf S2 holds

ex phi2 being 0wff string of S2 st

( phi2 = phi1 & I2 -AtomicEval phi2 = I1 -AtomicEval phi1 )

let S1, S2 be Language; :: thesis: for phi1 being 0wff string of S1

for I1 being Element of U -InterpretersOf S1

for I2 being Element of U -InterpretersOf S2 st I1 | ((rng phi1) /\ (OwnSymbolsOf S1)) = I2 | ((rng phi1) /\ (OwnSymbolsOf S1)) & the adicity of S1 | ((rng phi1) /\ (OwnSymbolsOf S1)) = the adicity of S2 | ((rng phi1) /\ (OwnSymbolsOf S1)) & TheEqSymbOf S1 = TheEqSymbOf S2 holds

ex phi2 being 0wff string of S2 st

( phi2 = phi1 & I2 -AtomicEval phi2 = I1 -AtomicEval phi1 )

set II1 = U -InterpretersOf S1;

set II2 = U -InterpretersOf S2;

set a2 = the adicity of S2;

set F2 = S2 -firstChar ;

set E1 = TheEqSymbOf S1;

set E2 = TheEqSymbOf S2;

set TT1 = AllTermsOf S1;

set TT2 = AllTermsOf S2;

set O1 = OwnSymbolsOf S1;

set O2 = OwnSymbolsOf S2;

set C2 = S2 -multiCat ;

set F1 = S1 -firstChar ;

set TS1 = TermSymbolsOf S1;

set TS2 = TermSymbolsOf S2;

set a1 = the adicity of S1;

set C1 = S1 -multiCat ;

set AS1 = AtomicFormulaSymbolsOf S1;

set AS2 = AtomicFormulaSymbolsOf S2;

set d = U -deltaInterpreter ;

set RR1 = RelSymbolsOf S1;

reconsider TS1 = TermSymbolsOf S1 as non empty Subset of (OwnSymbolsOf S1) by FOMODEL1:1;

reconsider TS2 = TermSymbolsOf S2 as non empty Subset of (OwnSymbolsOf S2) by FOMODEL1:1;

let phi1 be 0wff string of S1; :: thesis: for I1 being Element of U -InterpretersOf S1

for I2 being Element of U -InterpretersOf S2 st I1 | ((rng phi1) /\ (OwnSymbolsOf S1)) = I2 | ((rng phi1) /\ (OwnSymbolsOf S1)) & the adicity of S1 | ((rng phi1) /\ (OwnSymbolsOf S1)) = the adicity of S2 | ((rng phi1) /\ (OwnSymbolsOf S1)) & TheEqSymbOf S1 = TheEqSymbOf S2 holds

ex phi2 being 0wff string of S2 st

( phi2 = phi1 & I2 -AtomicEval phi2 = I1 -AtomicEval phi1 )

let I1 be Element of U -InterpretersOf S1; :: thesis: for I2 being Element of U -InterpretersOf S2 st I1 | ((rng phi1) /\ (OwnSymbolsOf S1)) = I2 | ((rng phi1) /\ (OwnSymbolsOf S1)) & the adicity of S1 | ((rng phi1) /\ (OwnSymbolsOf S1)) = the adicity of S2 | ((rng phi1) /\ (OwnSymbolsOf S1)) & TheEqSymbOf S1 = TheEqSymbOf S2 holds

ex phi2 being 0wff string of S2 st

( phi2 = phi1 & I2 -AtomicEval phi2 = I1 -AtomicEval phi1 )

let I2 be Element of U -InterpretersOf S2; :: thesis: ( I1 | ((rng phi1) /\ (OwnSymbolsOf S1)) = I2 | ((rng phi1) /\ (OwnSymbolsOf S1)) & the adicity of S1 | ((rng phi1) /\ (OwnSymbolsOf S1)) = the adicity of S2 | ((rng phi1) /\ (OwnSymbolsOf S1)) & TheEqSymbOf S1 = TheEqSymbOf S2 implies ex phi2 being 0wff string of S2 st

( phi2 = phi1 & I2 -AtomicEval phi2 = I1 -AtomicEval phi1 ) )

set TE1 = I1 -TermEval ;

set TE2 = I2 -TermEval ;

set X = (rng phi1) /\ (OwnSymbolsOf S1);

assume A1: ( I1 | ((rng phi1) /\ (OwnSymbolsOf S1)) = I2 | ((rng phi1) /\ (OwnSymbolsOf S1)) & the adicity of S1 | ((rng phi1) /\ (OwnSymbolsOf S1)) = the adicity of S2 | ((rng phi1) /\ (OwnSymbolsOf S1)) & TheEqSymbOf S1 = TheEqSymbOf S2 ) ; :: thesis: ex phi2 being 0wff string of S2 st

( phi2 = phi1 & I2 -AtomicEval phi2 = I1 -AtomicEval phi1 )

then A2: (I1 -TermEval) | (((rng phi1) /\ (OwnSymbolsOf S1)) *) = (I2 -TermEval) | (((rng phi1) /\ (OwnSymbolsOf S1)) *) by Th11;

then A3: dom ((I1 -TermEval) | (((rng phi1) /\ (OwnSymbolsOf S1)) *)) = (((rng phi1) /\ (OwnSymbolsOf S1)) *) /\ (dom (I2 -TermEval)) by RELAT_1:61

.= (((rng phi1) /\ (OwnSymbolsOf S1)) *) /\ (AllTermsOf S2) by FUNCT_2:def 1 ;

then A4: (((rng phi1) /\ (OwnSymbolsOf S1)) *) /\ (AllTermsOf S2) = (((rng phi1) /\ (OwnSymbolsOf S1)) *) /\ (dom (I1 -TermEval)) by RELAT_1:61

.= (((rng phi1) /\ (OwnSymbolsOf S1)) *) /\ (AllTermsOf S1) by FUNCT_2:def 1 ;

reconsider r1 = (S1 -firstChar) . phi1 as relational Element of S1 ;

set m = |.(ar r1).|;

set Y1 = ((rng phi1) /\ (OwnSymbolsOf S1)) \/ {(TheEqSymbOf S1)};

set Y2 = ((rng phi1) /\ (OwnSymbolsOf S1)) \/ {(TheEqSymbOf S2)};

{((phi1 null {}) . 1)} \ ((rng phi1) \/ {}) = {} ;

then phi1 . 1 in rng phi1 by ZFMISC_1:60;

then A5: r1 in rng phi1 by FOMODEL0:6;

( r1 in {(TheEqSymbOf S1)} or not r1 in (RelSymbolsOf S1) \ (OwnSymbolsOf S1) ) by FOMODEL1:1;

then A6: ( r1 in {(TheEqSymbOf S1)} or not r1 in RelSymbolsOf S1 or r1 in OwnSymbolsOf S1 ) by XBOOLE_0:def 5;

then ( r1 in {(TheEqSymbOf S1)} or r1 in (rng phi1) /\ (OwnSymbolsOf S1) ) by A5, FOMODEL1:def 17, XBOOLE_0:def 4;

then A7: r1 in ((rng phi1) /\ (OwnSymbolsOf S1)) \/ {(TheEqSymbOf S1)} by XBOOLE_0:def 3;

reconsider t1 = SubTerms phi1 as |.(ar r1).| + 0 -element FinSequence of AllTermsOf S1 by FOMODEL0:26;

t1 is TS1 * -valued ;

then ( t1 in |.(ar r1).| -tuples_on ((OwnSymbolsOf S1) *) & t1 in |.(ar r1).| -tuples_on ((rng phi1) *) ) by FOMODEL0:16;

then t1 in (|.(ar r1).| -tuples_on ((rng phi1) *)) /\ (|.(ar r1).| -tuples_on ((OwnSymbolsOf S1) *)) by XBOOLE_0:def 4;

then t1 in |.(ar r1).| -tuples_on (((rng phi1) *) /\ ((OwnSymbolsOf S1) *)) by FOMODEL0:3;

then t1 in |.(ar r1).| -tuples_on (((rng phi1) /\ (OwnSymbolsOf S1)) *) by FOMODEL0:55;

then A8: ( t1 is ((rng phi1) /\ (OwnSymbolsOf S1)) * -valued & rng t1 c= AllTermsOf S1 ) by FOMODEL0:12, RELAT_1:def 19;

then A9: ( rng t1 c= ((rng phi1) /\ (OwnSymbolsOf S1)) * & rng t1 c= AllTermsOf S1 ) by RELAT_1:def 19;

then A10: rng t1 c= (((rng phi1) /\ (OwnSymbolsOf S1)) *) /\ (AllTermsOf S1) by XBOOLE_1:19;

rng t1 c= (((rng phi1) /\ (OwnSymbolsOf S1)) *) /\ (AllTermsOf S2) by XBOOLE_1:19, A9, A4;

then reconsider X2 = (((rng phi1) /\ (OwnSymbolsOf S1)) *) /\ (AllTermsOf S2) as non empty Subset of (AllTermsOf S2) ;

reconsider X1 = (((rng phi1) /\ (OwnSymbolsOf S1)) *) /\ (AllTermsOf S1) as non empty Subset of (AllTermsOf S1) by A10;

t1 is X2 -valued |.(ar r1).| -element FinSequence by RELAT_1:def 19, A9, A4, XBOOLE_1:19;

then reconsider t2 = t1 as |.(ar r1).| -element FinSequence of X2 by FOMODEL0:26;

t2 is Element of X2 * ;

then reconsider tt2 = t2 as |.(ar r1).| -element Element of (AllTermsOf S2) * ;

reconsider E11 = TheEqSymbOf S1 as Element of AtomicFormulaSymbolsOf S1 by FOMODEL1:def 20;

reconsider EE1 = {E11} as non empty Subset of (AtomicFormulaSymbolsOf S1) ;

reconsider E22 = TheEqSymbOf S2 as Element of AtomicFormulaSymbolsOf S2 by FOMODEL1:def 20;

reconsider EE2 = {E22} as non empty Subset of (AtomicFormulaSymbolsOf S2) ;

set Y1 = ((rng phi1) /\ (OwnSymbolsOf S1)) \/ EE1;

set Y2 = ((rng phi1) /\ (OwnSymbolsOf S1)) \/ EE2;

set f1 = the adicity of S1 | EE1;

set f2 = the adicity of S2 | EE2;

A11: ( dom ( the adicity of S1 | EE1) = EE1 & dom ( the adicity of S2 | EE2) = EE2 ) by PARTFUN1:def 2;

now :: thesis: for x being object st x in dom ( the adicity of S1 | EE1) holds

( the adicity of S1 | EE1) . x = ( the adicity of S2 | EE2) . x

then
the adicity of S1 | EE1 = the adicity of S2 | EE2
by FUNCT_1:2, A11, A1;( the adicity of S1 | EE1) . x = ( the adicity of S2 | EE2) . x

let x be object ; :: thesis: ( x in dom ( the adicity of S1 | EE1) implies ( the adicity of S1 | EE1) . x = ( the adicity of S2 | EE2) . x )

assume A12: x in dom ( the adicity of S1 | EE1) ; :: thesis: ( the adicity of S1 | EE1) . x = ( the adicity of S2 | EE2) . x

then ( x = TheEqSymbOf S1 & ( the adicity of S1 | EE1) . x = the adicity of S1 . x ) by FUNCT_1:47, TARSKI:def 1;

then ( ( the adicity of S1 | EE1) . x = - 2 & the adicity of S2 . x = - 2 ) by FOMODEL1:def 23, A1;

hence ( the adicity of S1 | EE1) . x = ( the adicity of S2 | EE2) . x by A11, A1, A12, FUNCT_1:47; :: thesis: verum

end;assume A12: x in dom ( the adicity of S1 | EE1) ; :: thesis: ( the adicity of S1 | EE1) . x = ( the adicity of S2 | EE2) . x

then ( x = TheEqSymbOf S1 & ( the adicity of S1 | EE1) . x = the adicity of S1 . x ) by FUNCT_1:47, TARSKI:def 1;

then ( ( the adicity of S1 | EE1) . x = - 2 & the adicity of S2 . x = - 2 ) by FOMODEL1:def 23, A1;

hence ( the adicity of S1 | EE1) . x = ( the adicity of S2 | EE2) . x by A11, A1, A12, FUNCT_1:47; :: thesis: verum

then ( the adicity of S2 | ((rng phi1) /\ (OwnSymbolsOf S1))) +* ( the adicity of S2 | EE2) = the adicity of S1 | (((rng phi1) /\ (OwnSymbolsOf S1)) \/ EE1) by A1, FUNCT_4:78;

then A13: ( ((rng phi1) /\ (OwnSymbolsOf S1)) \/ EE1 = ((rng phi1) /\ (OwnSymbolsOf S1)) \/ EE2 & the adicity of S1 | (((rng phi1) /\ (OwnSymbolsOf S1)) \/ EE1) = the adicity of S2 | (((rng phi1) /\ (OwnSymbolsOf S1)) \/ EE2) ) by FUNCT_4:78, A1;

A14: ar r1 = ( the adicity of S1 | (((rng phi1) /\ (OwnSymbolsOf S1)) \/ EE1)) . r1 by FUNCT_1:49, A7

.= the adicity of S2 . r1 by A7, A13, FUNCT_1:49 ;

then r1 in dom the adicity of S2 by FUNCT_1:def 2;

then r1 in AtomicFormulaSymbolsOf S2 ;

then reconsider r2 = r1 as ofAtomicFormula Element of S2 by FOMODEL1:def 20;

A15: ar r1 = ar r2 by A14;

then reconsider r2 = r2 as relational Element of S2 ;

reconsider phi2 = r2 -compound tt2 as 0wff string of S2 by A15;

take phi2 ; :: thesis: ( phi2 = phi1 & I2 -AtomicEval phi2 = I1 -AtomicEval phi1 )

thus phi1 = <*r1*> ^ ((S1 -multiCat) . t1) by FOMODEL1:def 38

.= phi2 by FOMODEL0:52 ; :: thesis: I2 -AtomicEval phi2 = I1 -AtomicEval phi1

A16: (S2 -firstChar) . phi2 = phi2 . 1 by FOMODEL0:6

.= r2 by FINSEQ_1:41 ;

then reconsider tt22 = tt2 as |.(ar ((S2 -firstChar) . phi2)).| -element Element of (AllTermsOf S2) * by A14;

A17: tt22 = SubTerms phi2 by FOMODEL1:def 38, A16;

A18: (I1 -TermEval) * t1 = ((I1 -TermEval) | (((rng phi1) /\ (OwnSymbolsOf S1)) *)) * t1 by RELAT_1:165, XBOOLE_1:19, A9, A4, A3

.= (I2 -TermEval) * (SubTerms phi2) by A17, A2, A8, RELAT_1:def 19, A3, RELAT_1:165 ;

per cases
( r1 <> TheEqSymbOf S1 or r1 = TheEqSymbOf S1 )
;

end;

suppose A19:
r1 <> TheEqSymbOf S1
; :: thesis: I2 -AtomicEval phi2 = I1 -AtomicEval phi1

then A20:
r1 in (rng phi1) /\ (OwnSymbolsOf S1)
by A6, A5, FOMODEL1:def 17, XBOOLE_0:def 4, TARSKI:def 1;

then I1 . r1 = (I1 | ((rng phi1) /\ (OwnSymbolsOf S1))) . r1 by FUNCT_1:49

.= I2 . r2 by FUNCT_1:49, A1, A20 ;

then ( I1 -AtomicEval phi1 = (I1 . r1) . ((I1 -TermEval) * t1) & I2 -AtomicEval phi2 = (I1 . r1) . ((I2 -TermEval) * (SubTerms phi2)) ) by A1, A19, A16, FOMODEL2:14;

hence I1 -AtomicEval phi1 = I2 -AtomicEval phi2 by A18; :: thesis: verum

end;then I1 . r1 = (I1 | ((rng phi1) /\ (OwnSymbolsOf S1))) . r1 by FUNCT_1:49

.= I2 . r2 by FUNCT_1:49, A1, A20 ;

then ( I1 -AtomicEval phi1 = (I1 . r1) . ((I1 -TermEval) * t1) & I2 -AtomicEval phi2 = (I1 . r1) . ((I2 -TermEval) * (SubTerms phi2)) ) by A1, A19, A16, FOMODEL2:14;

hence I1 -AtomicEval phi1 = I2 -AtomicEval phi2 by A18; :: thesis: verum

suppose
r1 = TheEqSymbOf S1
; :: thesis: I2 -AtomicEval phi2 = I1 -AtomicEval phi1

then
( I1 -AtomicEval phi1 = (U -deltaInterpreter) . ((I1 -TermEval) * t1) & I2 -AtomicEval phi2 = (U -deltaInterpreter) . ((I2 -TermEval) * (SubTerms phi2)) )
by A1, A16, FOMODEL2:14;

hence I1 -AtomicEval phi1 = I2 -AtomicEval phi2 by A18; :: thesis: verum

end;hence I1 -AtomicEval phi1 = I2 -AtomicEval phi2 by A18; :: thesis: verum