let U be non empty set ; :: thesis:
let S1, S2 be Language; :: thesis:
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:
let I1 be Element of U -InterpretersOf S1; :: thesis:
let I2 be Element of U -InterpretersOf S2; :: thesis:
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:
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;

let x be object ; :: thesis:
assume A12: x in dom ( the adicity of S1 | EE1) ; :: thesis:
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:

end;

then the adicity of S1 | EE1 = the adicity of S2 | EE2 by FUNCT_1:2, A11, A1;
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:
thus phi1 = <*r1*> ^ ((S1 -multiCat) . t1) by FOMODEL1:def 38
.= phi2 by FOMODEL0:52 ; :: thesis:
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 ;

suppose A19: r1 <> TheEqSymbOf S1 ; :: thesis:

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:

end;

suppose r1 = TheEqSymbOf S1 ; :: thesis:

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:

end;

end;