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 B0: ( 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 B5: (I1 -TermEval) | (((rng phi1) /\ (OwnSymbolsOf S1)) *) = (I2 -TermEval) | (((rng phi1) /\ (OwnSymbolsOf S1)) *) by Th11;
then B4: 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 B1: (((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 = abs (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 C3: r1 in rng phi1 by FOMODEL0:6;
( r1 in {(TheEqSymbOf S1)} or not r1 in (RelSymbolsOf S1) \ (OwnSymbolsOf S1) ) by FOMODEL1:1;
then CC4: ( 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 C3, FOMODEL1:def 17, XBOOLE_0:def 4;
then B6: r1 in ((rng phi1) /\ (OwnSymbolsOf S1)) \/ {(TheEqSymbOf S1)} by XBOOLE_0:def 3;
reconsider t1 = SubTerms phi1 as (abs (ar r1)) + 0 -element FinSequence of AllTermsOf S1 by FOMODEL0:26;
t1 is TS1 * -valued ;
then ( t1 in (abs (ar r1)) -tuples_on ((OwnSymbolsOf S1) *) & t1 in (abs (ar r1)) -tuples_on ((rng phi1) *) ) by FOMODEL0:16;
then t1 in ((abs (ar r1)) -tuples_on ((rng phi1) *)) /\ ((abs (ar r1)) -tuples_on ((OwnSymbolsOf S1) *)) by XBOOLE_0:def 4;
then t1 in (abs (ar r1)) -tuples_on (((rng phi1) *) /\ ((OwnSymbolsOf S1) *)) by FOMODEL0:3;
then t1 in (abs (ar r1)) -tuples_on (((rng phi1) /\ (OwnSymbolsOf S1)) *) by FOMODEL0:55;
then ( t1 is ((rng phi1) /\ (OwnSymbolsOf S1)) * -valued & rng t1 c= AllTermsOf S1 ) by FOMODEL0:12, RELAT_1:def 19;
then Z2: ( rng t1 c= ((rng phi1) /\ (OwnSymbolsOf S1)) * & rng t1 c= AllTermsOf S1 ) by RELAT_1:def 19;
then B2: rng t1 c= (((rng phi1) /\ (OwnSymbolsOf S1)) *) /\ (AllTermsOf S1) by XBOOLE_1:19;
B3: rng t1 c= (((rng phi1) /\ (OwnSymbolsOf S1)) *) /\ (AllTermsOf S2) by Z2, B1, XBOOLE_1:19;
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 B2;
t1 is X2 -valued abs (ar r1) -element FinSequence by B3, RELAT_1:def 19;
then reconsider t2 = t1 as abs (ar r1) -element FinSequence of X2 by FOMODEL0:26;
t2 is Element of X2 * by FINSEQ_1:def 11;
then reconsider tt2 = t2 as abs (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;
C5: ( dom ( the adicity of S1 | EE1) = EE1 & dom ( the adicity of S2 | EE2) = EE2 ) by PARTFUN1:def 2;

let x be set ; :: thesis:
assume D0: 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 C5, FUNCT_1:47, TARSKI:def 1;
then ( ( the adicity of S1 | EE1) . x = - 2 & the adicity of S2 . x = - 2 ) by B0, FOMODEL1:def 23;
hence ( the adicity of S1 | EE1) . x = ( the adicity of S2 | EE2) . x by C5, B0, D0, FUNCT_1:47; :: thesis:

end;

then the adicity of S1 | EE1 = the adicity of S2 | EE2 by C5, B0, FUNCT_1: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 B0, FUNCT_4:78;
then C2: ( ((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 B0, FUNCT_4:78;
C0: ar r1 = ( the adicity of S1 | (((rng phi1) /\ (OwnSymbolsOf S1)) \/ EE1)) . r1 by B6, FUNCT_1:49
.= the adicity of S2 . r1 by B6, C2, 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;
C1: ar r1 = ar r2 by C0;
then reconsider r2 = r2 as relational Element of S2 ;
reconsider phi2 = r2 -compound tt2 as 0wff string of S2 by C1;
take phi2 ; :: thesis:
thus phi1 = <*r1*> ^ ((S1 -multiCat) . t1) by FOMODEL1:def 38
.= phi2 by FOMODEL0:52 ; :: thesis:
B11: (S2 -firstChar) . phi2 = phi2 . 1 by FOMODEL0:6
.= r2 by FINSEQ_1:41 ;
then reconsider tt22 = tt2 as abs (ar ((S2 -firstChar) . phi2)) -element Element of (AllTermsOf S2) * by C0;
B12: tt22 = SubTerms phi2 by B11, FOMODEL1:def 38;
B15: (I1 -TermEval) * t1 = ((I1 -TermEval) | (((rng phi1) /\ (OwnSymbolsOf S1)) *)) * t1 by Z2, B1, B4, RELAT_1:165, XBOOLE_1:19
.= (I2 -TermEval) * (SubTerms phi2) by B12, B5, Z2, B1, B4, RELAT_1:165, XBOOLE_1:19 ;

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

then D0: r1 in (rng phi1) /\ (OwnSymbolsOf S1) by CC4, C3, FOMODEL1:def 17, TARSKI:def 1, XBOOLE_0:def 4;
then I1 . r1 = (I1 | ((rng phi1) /\ (OwnSymbolsOf S1))) . r1 by FUNCT_1:49
.= I2 . r2 by B0, D0, FUNCT_1:49 ;
then ( I1 -AtomicEval phi1 = (I1 . r1) . ((I1 -TermEval) * t1) & I2 -AtomicEval phi2 = (I1 . r1) . ((I2 -TermEval) * (SubTerms phi2)) ) by B0, D1, B11, FOMODEL2:14;
hence I1 -AtomicEval phi1 = I2 -AtomicEval phi2 by B15; :: 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 B0, B11, FOMODEL2:14;
hence I1 -AtomicEval phi1 = I2 -AtomicEval phi2 by B15; :: thesis:

end;

end;