let X be set ; :: thesis: for U being non empty set

for S1, S2 being Language

for I1 being Element of U -InterpretersOf S1

for I2 being Element of U -InterpretersOf S2 st I1 | X = I2 | X & the adicity of S1 | X = the adicity of S2 | X holds

(I1 -TermEval) | (X *) c= (I2 -TermEval) | (X *)

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

for I1 being Element of U -InterpretersOf S1

for I2 being Element of U -InterpretersOf S2 st I1 | X = I2 | X & the adicity of S1 | X = the adicity of S2 | X holds

(I1 -TermEval) | (X *) c= (I2 -TermEval) | (X *)

let S1, S2 be Language; :: thesis: for I1 being Element of U -InterpretersOf S1

for I2 being Element of U -InterpretersOf S2 st I1 | X = I2 | X & the adicity of S1 | X = the adicity of S2 | X holds

(I1 -TermEval) | (X *) c= (I2 -TermEval) | (X *)

set T1 = S1 -termsOfMaxDepth ;

set O1 = OwnSymbolsOf S1;

set TT1 = AllTermsOf S1;

set SS1 = AllSymbolsOf S1;

set L1 = LettersOf S1;

set F1 = S1 -firstChar ;

set C1 = S1 -multiCat ;

set AT1 = AtomicTermsOf S1;

set II1 = U -InterpretersOf S1;

set a1 = the adicity of S1;

set strings1 = ((AllSymbolsOf S1) *) \ {{}};

set T2 = S2 -termsOfMaxDepth ;

set O2 = OwnSymbolsOf S2;

set TT2 = AllTermsOf S2;

set SS2 = AllSymbolsOf S2;

set L2 = LettersOf S2;

set F2 = S2 -firstChar ;

set C2 = S2 -multiCat ;

set AT2 = AtomicTermsOf S2;

set II2 = U -InterpretersOf S2;

set a2 = the adicity of S2;

set strings2 = ((AllSymbolsOf S2) *) \ {{}};

let I1 be Element of U -InterpretersOf S1; :: thesis: for I2 being Element of U -InterpretersOf S2 st I1 | X = I2 | X & the adicity of S1 | X = the adicity of S2 | X holds

(I1 -TermEval) | (X *) c= (I2 -TermEval) | (X *)

let I2 be Element of U -InterpretersOf S2; :: thesis: ( I1 | X = I2 | X & the adicity of S1 | X = the adicity of S2 | X implies (I1 -TermEval) | (X *) c= (I2 -TermEval) | (X *) )

A1: ( dom I1 = OwnSymbolsOf S1 & dom I2 = OwnSymbolsOf S2 ) by PARTFUN1:def 2;

set E1 = I1 -TermEval ;

set E2 = I2 -TermEval ;

set I11 = I1 | X;

set I22 = I2 | X;

assume A2: I1 | X = I2 | X ; :: thesis: ( not the adicity of S1 | X = the adicity of S2 | X or (I1 -TermEval) | (X *) c= (I2 -TermEval) | (X *) )

then A3: ( dom (I1 -TermEval) = AllTermsOf S1 & dom (I2 -TermEval) = AllTermsOf S2 & I1 | X = I2 | X ) by FUNCT_2:def 1;

A4: X /\ (dom I1) = dom (I2 | X) by RELAT_1:61, A2

.= X /\ (dom I2) by RELAT_1:61 ;

defpred S_{1}[ Nat] means (I1 -TermEval) | ((X *) /\ ((S1 -termsOfMaxDepth) . $1)) c= (I2 -TermEval) | ((X *) /\ ((S2 -termsOfMaxDepth) . $1));

deffunc H_{1}( set ) -> set = { <*x*> where x is Element of $1 : verum } ;

A5: S_{1}[ 0 ]

A17: for n being Nat st S_{1}[n] holds

S_{1}[n + 1]
_{1}[n]
from NAT_1:sch 2(A5, A17);

for S1, S2 being Language

for I1 being Element of U -InterpretersOf S1

for I2 being Element of U -InterpretersOf S2 st I1 | X = I2 | X & the adicity of S1 | X = the adicity of S2 | X holds

(I1 -TermEval) | (X *) c= (I2 -TermEval) | (X *)

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

for I1 being Element of U -InterpretersOf S1

for I2 being Element of U -InterpretersOf S2 st I1 | X = I2 | X & the adicity of S1 | X = the adicity of S2 | X holds

(I1 -TermEval) | (X *) c= (I2 -TermEval) | (X *)

let S1, S2 be Language; :: thesis: for I1 being Element of U -InterpretersOf S1

for I2 being Element of U -InterpretersOf S2 st I1 | X = I2 | X & the adicity of S1 | X = the adicity of S2 | X holds

(I1 -TermEval) | (X *) c= (I2 -TermEval) | (X *)

set T1 = S1 -termsOfMaxDepth ;

set O1 = OwnSymbolsOf S1;

set TT1 = AllTermsOf S1;

set SS1 = AllSymbolsOf S1;

set L1 = LettersOf S1;

set F1 = S1 -firstChar ;

set C1 = S1 -multiCat ;

set AT1 = AtomicTermsOf S1;

set II1 = U -InterpretersOf S1;

set a1 = the adicity of S1;

set strings1 = ((AllSymbolsOf S1) *) \ {{}};

set T2 = S2 -termsOfMaxDepth ;

set O2 = OwnSymbolsOf S2;

set TT2 = AllTermsOf S2;

set SS2 = AllSymbolsOf S2;

set L2 = LettersOf S2;

set F2 = S2 -firstChar ;

set C2 = S2 -multiCat ;

set AT2 = AtomicTermsOf S2;

set II2 = U -InterpretersOf S2;

set a2 = the adicity of S2;

set strings2 = ((AllSymbolsOf S2) *) \ {{}};

let I1 be Element of U -InterpretersOf S1; :: thesis: for I2 being Element of U -InterpretersOf S2 st I1 | X = I2 | X & the adicity of S1 | X = the adicity of S2 | X holds

(I1 -TermEval) | (X *) c= (I2 -TermEval) | (X *)

let I2 be Element of U -InterpretersOf S2; :: thesis: ( I1 | X = I2 | X & the adicity of S1 | X = the adicity of S2 | X implies (I1 -TermEval) | (X *) c= (I2 -TermEval) | (X *) )

A1: ( dom I1 = OwnSymbolsOf S1 & dom I2 = OwnSymbolsOf S2 ) by PARTFUN1:def 2;

set E1 = I1 -TermEval ;

set E2 = I2 -TermEval ;

set I11 = I1 | X;

set I22 = I2 | X;

assume A2: I1 | X = I2 | X ; :: thesis: ( not the adicity of S1 | X = the adicity of S2 | X or (I1 -TermEval) | (X *) c= (I2 -TermEval) | (X *) )

then A3: ( dom (I1 -TermEval) = AllTermsOf S1 & dom (I2 -TermEval) = AllTermsOf S2 & I1 | X = I2 | X ) by FUNCT_2:def 1;

A4: X /\ (dom I1) = dom (I2 | X) by RELAT_1:61, A2

.= X /\ (dom I2) by RELAT_1:61 ;

defpred S

deffunc H

A5: S

proof

assume A16:
the adicity of S1 | X = the adicity of S2 | X
; :: thesis: (I1 -TermEval) | (X *) c= (I2 -TermEval) | (X *)
A6:
( (S2 -termsOfMaxDepth) . 0 c= AllTermsOf S2 & (S1 -termsOfMaxDepth) . 0 c= AllTermsOf S1 )
by FOMODEL1:2;

reconsider D1 = (X *) /\ ((S1 -termsOfMaxDepth) . 0) as Subset of (AllTermsOf S1) by A6, XBOOLE_1:1;

reconsider D2 = (X *) /\ ((S2 -termsOfMaxDepth) . 0) as Subset of (AllTermsOf S2) by A6, XBOOLE_1:1;

set f1 = (I1 -TermEval) | D1;

set f2 = (I2 -TermEval) | D2;

A7: ( dom ((I1 -TermEval) | D1) = D1 & dom ((I2 -TermEval) | D2) = D2 ) by PARTFUN1:def 2;

_{1}[ 0 ]
by FOMODEL0:51; :: thesis: verum

end;reconsider D1 = (X *) /\ ((S1 -termsOfMaxDepth) . 0) as Subset of (AllTermsOf S1) by A6, XBOOLE_1:1;

reconsider D2 = (X *) /\ ((S2 -termsOfMaxDepth) . 0) as Subset of (AllTermsOf S2) by A6, XBOOLE_1:1;

set f1 = (I1 -TermEval) | D1;

set f2 = (I2 -TermEval) | D2;

A7: ( dom ((I1 -TermEval) | D1) = D1 & dom ((I2 -TermEval) | D2) = D2 ) by PARTFUN1:def 2;

now :: thesis: for x being set st x in dom ((I1 -TermEval) | D1) holds

( x in dom ((I2 -TermEval) | D2) & ((I2 -TermEval) | D2) . x = ((I1 -TermEval) | D1) . x )

hence
S( x in dom ((I2 -TermEval) | D2) & ((I2 -TermEval) | D2) . x = ((I1 -TermEval) | D1) . x )

let x be set ; :: thesis: ( x in dom ((I1 -TermEval) | D1) implies ( x in dom ((I2 -TermEval) | D2) & ((I2 -TermEval) | D2) . x = ((I1 -TermEval) | D1) . x ) )

assume A8: x in dom ((I1 -TermEval) | D1) ; :: thesis: ( x in dom ((I2 -TermEval) | D2) & ((I2 -TermEval) | D2) . x = ((I1 -TermEval) | D1) . x )

then A9: x in (X *) /\ (AtomicTermsOf S1) by A7, FOMODEL1:def 30;

then A10: x in 1 -tuples_on (X /\ (LettersOf S1)) by FOMODEL0:2;

then reconsider Y1 = X /\ (LettersOf S1) as non empty set ;

Y1 <> {} ;

then reconsider XX = X as non empty set ;

reconsider xx = x as Element of X * by A8, A7;

x in H_{1}(Y1)
by FINSEQ_2:96, A10;

then consider y1 being Element of Y1 such that

A11: x = <*y1*> ;

y1 in Y1 ;

then reconsider l1 = y1 as literal Element of S1 ;

( l1 in X & l1 in OwnSymbolsOf S1 ) by XBOOLE_0:def 4, FOMODEL1:def 19;

then l1 in X /\ (OwnSymbolsOf S2) by A4, A1, XBOOLE_0:def 4;

then reconsider s2 = l1 as own Element of S2 ;

reconsider s22 = s2, l11 = l1 as Element of XX by XBOOLE_0:def 4;

( ((I2 | XX) . s22) \+\ (I2 . s22) = {} & ((I1 | XX) . l11) \+\ (I1 . l11) = {} ) ;

then ( (I2 | X) . s2 = I2 . s2 & (I1 | X) . l1 = I1 . l1 ) by FOMODEL0:29;

then 0 -tuples_on U = dom (I2 . s2) by A2, FUNCT_2:def 1

.= |.(ar s2).| -tuples_on U by FUNCT_2:def 1 ;

then ( not s2 is relational & not s2 is operational ) ;

then reconsider l2 = s2 as literal Element of S2 ;

x in AtomicTermsOf S1 by A9;

then x in (S1 -termsOfMaxDepth) . 0 by FOMODEL1:def 30;

then reconsider t1 = x as 0 -termal string of S1 by FOMODEL1:def 33;

reconsider D11 = D1 as non empty Subset of (AllTermsOf S1) by A8;

reconsider x1 = t1 as Element of D11 by A8;

A12: ( l11 in XX & l2 in LettersOf S2 ) by FOMODEL1:def 14;

then reconsider Y2 = XX /\ (LettersOf S2) as non empty set by XBOOLE_0:def 4;

reconsider ll2 = l2 as Element of Y2 by A12, XBOOLE_0:def 4;

<*ll2*> in H_{1}(Y2)
;

then <*ll2*> in 1 -tuples_on Y2 by FINSEQ_2:96;

then A13: x in (X *) /\ (AtomicTermsOf S2) by FOMODEL0:2, A11;

reconsider D22 = D2 as non empty Subset of (AllTermsOf S2) by FOMODEL1:def 30, A13;

reconsider x2 = x as Element of D22 by A13, FOMODEL1:def 30;

A14: t1 . 1 = y1 by A11, FINSEQ_1:40;

then reconsider y11 = t1 . 1 as Element of XX by XBOOLE_0:def 4;

( ((I1 | XX) . y11) \+\ (I1 . y11) = {} & ((I2 | XX) . y11) \+\ (I2 . y11) = {} & (((I2 -TermEval) | D22) . x2) \+\ ((I2 -TermEval) . x2) = {} ) ;

then A15: ( (I1 | X) . y11 = I1 . y11 & (I2 | X) . y11 = I2 . y11 & (I2 -TermEval) . x2 = ((I2 -TermEval) | D22) . x2 ) by FOMODEL0:29;

(((I1 -TermEval) | D11) . x1) \+\ ((I1 -TermEval) . x1) = {} ;

then ((I1 -TermEval) | D1) . x = (I1 -TermEval) . t1 by FOMODEL0:29

.= (I1 . ((S1 -firstChar) . t1)) . ((I1 -TermEval) * (SubTerms t1)) by FOMODEL2:21

.= (I2 . l2) . {} by FOMODEL0:6, A14, A2, A15

.= (I2 . (<*l2*> . 1)) . {} by FINSEQ_1:40

.= (I2 . ((S2 -firstChar) . <*l2*>)) . ((I2 -TermEval) * (SubTerms <*l2*>)) by FOMODEL0:6

.= ((I2 -TermEval) | D2) . x by FOMODEL2:21, A11, A15 ;

hence ( x in dom ((I2 -TermEval) | D2) & ((I2 -TermEval) | D2) . x = ((I1 -TermEval) | D1) . x ) by A7, A13, FOMODEL1:def 30; :: thesis: verum

end;assume A8: x in dom ((I1 -TermEval) | D1) ; :: thesis: ( x in dom ((I2 -TermEval) | D2) & ((I2 -TermEval) | D2) . x = ((I1 -TermEval) | D1) . x )

then A9: x in (X *) /\ (AtomicTermsOf S1) by A7, FOMODEL1:def 30;

then A10: x in 1 -tuples_on (X /\ (LettersOf S1)) by FOMODEL0:2;

then reconsider Y1 = X /\ (LettersOf S1) as non empty set ;

Y1 <> {} ;

then reconsider XX = X as non empty set ;

reconsider xx = x as Element of X * by A8, A7;

x in H

then consider y1 being Element of Y1 such that

A11: x = <*y1*> ;

y1 in Y1 ;

then reconsider l1 = y1 as literal Element of S1 ;

( l1 in X & l1 in OwnSymbolsOf S1 ) by XBOOLE_0:def 4, FOMODEL1:def 19;

then l1 in X /\ (OwnSymbolsOf S2) by A4, A1, XBOOLE_0:def 4;

then reconsider s2 = l1 as own Element of S2 ;

reconsider s22 = s2, l11 = l1 as Element of XX by XBOOLE_0:def 4;

( ((I2 | XX) . s22) \+\ (I2 . s22) = {} & ((I1 | XX) . l11) \+\ (I1 . l11) = {} ) ;

then ( (I2 | X) . s2 = I2 . s2 & (I1 | X) . l1 = I1 . l1 ) by FOMODEL0:29;

then 0 -tuples_on U = dom (I2 . s2) by A2, FUNCT_2:def 1

.= |.(ar s2).| -tuples_on U by FUNCT_2:def 1 ;

then ( not s2 is relational & not s2 is operational ) ;

then reconsider l2 = s2 as literal Element of S2 ;

x in AtomicTermsOf S1 by A9;

then x in (S1 -termsOfMaxDepth) . 0 by FOMODEL1:def 30;

then reconsider t1 = x as 0 -termal string of S1 by FOMODEL1:def 33;

reconsider D11 = D1 as non empty Subset of (AllTermsOf S1) by A8;

reconsider x1 = t1 as Element of D11 by A8;

A12: ( l11 in XX & l2 in LettersOf S2 ) by FOMODEL1:def 14;

then reconsider Y2 = XX /\ (LettersOf S2) as non empty set by XBOOLE_0:def 4;

reconsider ll2 = l2 as Element of Y2 by A12, XBOOLE_0:def 4;

<*ll2*> in H

then <*ll2*> in 1 -tuples_on Y2 by FINSEQ_2:96;

then A13: x in (X *) /\ (AtomicTermsOf S2) by FOMODEL0:2, A11;

reconsider D22 = D2 as non empty Subset of (AllTermsOf S2) by FOMODEL1:def 30, A13;

reconsider x2 = x as Element of D22 by A13, FOMODEL1:def 30;

A14: t1 . 1 = y1 by A11, FINSEQ_1:40;

then reconsider y11 = t1 . 1 as Element of XX by XBOOLE_0:def 4;

( ((I1 | XX) . y11) \+\ (I1 . y11) = {} & ((I2 | XX) . y11) \+\ (I2 . y11) = {} & (((I2 -TermEval) | D22) . x2) \+\ ((I2 -TermEval) . x2) = {} ) ;

then A15: ( (I1 | X) . y11 = I1 . y11 & (I2 | X) . y11 = I2 . y11 & (I2 -TermEval) . x2 = ((I2 -TermEval) | D22) . x2 ) by FOMODEL0:29;

(((I1 -TermEval) | D11) . x1) \+\ ((I1 -TermEval) . x1) = {} ;

then ((I1 -TermEval) | D1) . x = (I1 -TermEval) . t1 by FOMODEL0:29

.= (I1 . ((S1 -firstChar) . t1)) . ((I1 -TermEval) * (SubTerms t1)) by FOMODEL2:21

.= (I2 . l2) . {} by FOMODEL0:6, A14, A2, A15

.= (I2 . (<*l2*> . 1)) . {} by FINSEQ_1:40

.= (I2 . ((S2 -firstChar) . <*l2*>)) . ((I2 -TermEval) * (SubTerms <*l2*>)) by FOMODEL0:6

.= ((I2 -TermEval) | D2) . x by FOMODEL2:21, A11, A15 ;

hence ( x in dom ((I2 -TermEval) | D2) & ((I2 -TermEval) | D2) . x = ((I1 -TermEval) | D1) . x ) by A7, A13, FOMODEL1:def 30; :: thesis: verum

A17: for n being Nat st S

S

proof

A49:
for n being Nat holds S
let n be Nat; :: thesis: ( S_{1}[n] implies S_{1}[n + 1] )

assume A18: S_{1}[n]
; :: thesis: S_{1}[n + 1]

reconsider nn = n, NN = n + 1 as Element of NAT by ORDINAL1:def 12;

A19: ( (S2 -termsOfMaxDepth) . NN c= AllTermsOf S2 & (S1 -termsOfMaxDepth) . NN c= AllTermsOf S1 & (S1 -termsOfMaxDepth) . nn c= AllTermsOf S1 & (S2 -termsOfMaxDepth) . nn c= AllTermsOf S2 ) by FOMODEL1:2;

reconsider D1 = (X *) /\ ((S1 -termsOfMaxDepth) . NN), d1 = (X *) /\ ((S1 -termsOfMaxDepth) . nn) as Subset of (AllTermsOf S1) by A19, XBOOLE_1:1;

reconsider D2 = (X *) /\ ((S2 -termsOfMaxDepth) . NN), d2 = (X *) /\ ((S2 -termsOfMaxDepth) . nn) as Subset of (AllTermsOf S2) by A19, XBOOLE_1:1;

set f1 = (I1 -TermEval) | D1;

set f2 = (I2 -TermEval) | D2;

A20: ( dom ((I1 -TermEval) | D1) = D1 & dom ((I2 -TermEval) | D2) = D2 & dom ((I1 -TermEval) | d1) = d1 & dom ((I2 -TermEval) | d2) = d2 ) by PARTFUN1:def 2;

then A21: d1 c= d2 by A18, GRFUNC_1:2;

reconsider d12 = d1 as Subset of d2 by A18, GRFUNC_1:2, A20;

reconsider d21 = d12 as Subset of (AllTermsOf S2) by XBOOLE_1:1;

_{1}[n + 1]
by FOMODEL0:51; :: thesis: verum

end;assume A18: S

reconsider nn = n, NN = n + 1 as Element of NAT by ORDINAL1:def 12;

A19: ( (S2 -termsOfMaxDepth) . NN c= AllTermsOf S2 & (S1 -termsOfMaxDepth) . NN c= AllTermsOf S1 & (S1 -termsOfMaxDepth) . nn c= AllTermsOf S1 & (S2 -termsOfMaxDepth) . nn c= AllTermsOf S2 ) by FOMODEL1:2;

reconsider D1 = (X *) /\ ((S1 -termsOfMaxDepth) . NN), d1 = (X *) /\ ((S1 -termsOfMaxDepth) . nn) as Subset of (AllTermsOf S1) by A19, XBOOLE_1:1;

reconsider D2 = (X *) /\ ((S2 -termsOfMaxDepth) . NN), d2 = (X *) /\ ((S2 -termsOfMaxDepth) . nn) as Subset of (AllTermsOf S2) by A19, XBOOLE_1:1;

set f1 = (I1 -TermEval) | D1;

set f2 = (I2 -TermEval) | D2;

A20: ( dom ((I1 -TermEval) | D1) = D1 & dom ((I2 -TermEval) | D2) = D2 & dom ((I1 -TermEval) | d1) = d1 & dom ((I2 -TermEval) | d2) = d2 ) by PARTFUN1:def 2;

then A21: d1 c= d2 by A18, GRFUNC_1:2;

reconsider d12 = d1 as Subset of d2 by A18, GRFUNC_1:2, A20;

reconsider d21 = d12 as Subset of (AllTermsOf S2) by XBOOLE_1:1;

now :: thesis: for y being set st y in dom ((I1 -TermEval) | D1) holds

( y in dom ((I2 -TermEval) | D2) & ((I1 -TermEval) | D1) . y = ((I2 -TermEval) | D2) . y )

hence
S( y in dom ((I2 -TermEval) | D2) & ((I1 -TermEval) | D1) . y = ((I2 -TermEval) | D2) . y )

let y be set ; :: thesis: ( y in dom ((I1 -TermEval) | D1) implies ( b_{1} in dom ((I2 -TermEval) | D2) & ((I1 -TermEval) | D1) . b_{1} = ((I2 -TermEval) | D2) . b_{1} ) )

assume A22: y in dom ((I1 -TermEval) | D1) ; :: thesis: ( b_{1} in dom ((I2 -TermEval) | D2) & ((I1 -TermEval) | D1) . b_{1} = ((I2 -TermEval) | D2) . b_{1} )

then reconsider D11 = D1 as non empty set ;

reconsider y1 = y as Element of D11 by A22;

y1 in (S1 -termsOfMaxDepth) . NN by XBOOLE_0:def 4;

then reconsider t1 = y1 as nn + 1 -termal string of S1 by FOMODEL1:def 33;

reconsider o1 = (S1 -firstChar) . t1 as termal Element of S1 ;

set m1 = |.(ar o1).|;

A23: ( t1 in X * & not t1 is empty ) by TARSKI:def 3;

then reconsider XX = X as non empty set ;

A24: y1 in XX * by TARSKI:def 3;

{(t1 . 1)} \ XX = {} by A24;

then A25: ( t1 . 1 in XX & o1 = t1 . 1 ) by ZFMISC_1:60, FOMODEL0:6;

then ( o1 in XX & o1 in OwnSymbolsOf S1 ) by FOMODEL1:def 19;

then o1 in XX /\ (OwnSymbolsOf S2) by A4, A1, XBOOLE_0:def 4;

then reconsider o2 = o1 as own Element of S2 ;

reconsider o22 = o2 as ofAtomicFormula Element of S2 ;

reconsider ox = o1 as Element of XX by A25;

( ( the adicity of S1 . ox) \+\ (( the adicity of S1 | XX) . ox) = {} & ( the adicity of S2 . ox) \+\ (( the adicity of S2 | XX) . ox) = {} ) ;

then A26: ( the adicity of S1 . o1 = ( the adicity of S1 | X) . o1 & the adicity of S2 . o2 = ( the adicity of S2 | X) . o2 ) by FOMODEL0:29;

ar o1 = ar o22 by A26, A16;

then not o22 is relational ;

then reconsider o2 = o2 as termal Element of S2 ;

set m2 = |.(ar o2).|;

A27: ( (I1 . ox) \+\ ((I1 | XX) . ox) = {} & (I2 . ox) \+\ ((I2 | XX) . ox) = {} ) ;

then A28: I1 . ox = (I1 | XX) . o1 by FOMODEL0:29

.= I2 . ox by A27, FOMODEL0:29, A2 ;

set st1 = SubTerms t1;

reconsider B = rng t1 as non empty Subset of XX by A24, RELAT_1:def 19;

( rng (SubTerms t1) c= (rng t1) * & B * c= XX * ) by RELAT_1:def 19;

then A29: rng (SubTerms t1) c= XX * by XBOOLE_1:1;

A30: rng (SubTerms t1) c= (S1 -termsOfMaxDepth) . n by RELAT_1:def 19;

then rng (SubTerms t1) c= d1 by A29, XBOOLE_1:19;

then A31: ( rng (SubTerms t1) c= ((AllSymbolsOf S1) *) \ {{}} & rng (SubTerms t1) c= d2 ) by XBOOLE_1:1, A21;

then A32: ( rng (SubTerms t1) c= ((AllSymbolsOf S1) *) \ {{}} & rng (SubTerms t1) c= ((AllSymbolsOf S2) *) \ {{}} ) by XBOOLE_1:1;

SubTerms t1 is (S2 -termsOfMaxDepth) . nn -valued by A31, XBOOLE_1:1, RELAT_1:def 19;

then SubTerms t1 is |.(ar o2).| -element FinSequence of (S2 -termsOfMaxDepth) . nn by FOMODEL0:26, A16, A26;

then reconsider st2 = SubTerms t1 as |.(ar o2).| -element Element of ((S2 -termsOfMaxDepth) . nn) * ;

reconsider T2n = (S2 -termsOfMaxDepth) . nn as non empty Subset of (AllTermsOf S2) by FOMODEL1:2;

st2 in T2n * ;

then reconsider st22 = st2 as |.(ar o2).| -element Element of (AllTermsOf S2) * ;

reconsider t2 = o2 -compound st2 as nn + 1 -termal string of S2 ;

end;assume A22: y in dom ((I1 -TermEval) | D1) ; :: thesis: ( b

then reconsider D11 = D1 as non empty set ;

reconsider y1 = y as Element of D11 by A22;

y1 in (S1 -termsOfMaxDepth) . NN by XBOOLE_0:def 4;

then reconsider t1 = y1 as nn + 1 -termal string of S1 by FOMODEL1:def 33;

reconsider o1 = (S1 -firstChar) . t1 as termal Element of S1 ;

set m1 = |.(ar o1).|;

A23: ( t1 in X * & not t1 is empty ) by TARSKI:def 3;

then reconsider XX = X as non empty set ;

A24: y1 in XX * by TARSKI:def 3;

{(t1 . 1)} \ XX = {} by A24;

then A25: ( t1 . 1 in XX & o1 = t1 . 1 ) by ZFMISC_1:60, FOMODEL0:6;

then ( o1 in XX & o1 in OwnSymbolsOf S1 ) by FOMODEL1:def 19;

then o1 in XX /\ (OwnSymbolsOf S2) by A4, A1, XBOOLE_0:def 4;

then reconsider o2 = o1 as own Element of S2 ;

reconsider o22 = o2 as ofAtomicFormula Element of S2 ;

reconsider ox = o1 as Element of XX by A25;

( ( the adicity of S1 . ox) \+\ (( the adicity of S1 | XX) . ox) = {} & ( the adicity of S2 . ox) \+\ (( the adicity of S2 | XX) . ox) = {} ) ;

then A26: ( the adicity of S1 . o1 = ( the adicity of S1 | X) . o1 & the adicity of S2 . o2 = ( the adicity of S2 | X) . o2 ) by FOMODEL0:29;

ar o1 = ar o22 by A26, A16;

then not o22 is relational ;

then reconsider o2 = o2 as termal Element of S2 ;

set m2 = |.(ar o2).|;

A27: ( (I1 . ox) \+\ ((I1 | XX) . ox) = {} & (I2 . ox) \+\ ((I2 | XX) . ox) = {} ) ;

then A28: I1 . ox = (I1 | XX) . o1 by FOMODEL0:29

.= I2 . ox by A27, FOMODEL0:29, A2 ;

set st1 = SubTerms t1;

reconsider B = rng t1 as non empty Subset of XX by A24, RELAT_1:def 19;

( rng (SubTerms t1) c= (rng t1) * & B * c= XX * ) by RELAT_1:def 19;

then A29: rng (SubTerms t1) c= XX * by XBOOLE_1:1;

A30: rng (SubTerms t1) c= (S1 -termsOfMaxDepth) . n by RELAT_1:def 19;

then rng (SubTerms t1) c= d1 by A29, XBOOLE_1:19;

then A31: ( rng (SubTerms t1) c= ((AllSymbolsOf S1) *) \ {{}} & rng (SubTerms t1) c= d2 ) by XBOOLE_1:1, A21;

then A32: ( rng (SubTerms t1) c= ((AllSymbolsOf S1) *) \ {{}} & rng (SubTerms t1) c= ((AllSymbolsOf S2) *) \ {{}} ) by XBOOLE_1:1;

SubTerms t1 is (S2 -termsOfMaxDepth) . nn -valued by A31, XBOOLE_1:1, RELAT_1:def 19;

then SubTerms t1 is |.(ar o2).| -element FinSequence of (S2 -termsOfMaxDepth) . nn by FOMODEL0:26, A16, A26;

then reconsider st2 = SubTerms t1 as |.(ar o2).| -element Element of ((S2 -termsOfMaxDepth) . nn) * ;

reconsider T2n = (S2 -termsOfMaxDepth) . nn as non empty Subset of (AllTermsOf S2) by FOMODEL1:2;

st2 in T2n * ;

then reconsider st22 = st2 as |.(ar o2).| -element Element of (AllTermsOf S2) * ;

reconsider t2 = o2 -compound st2 as nn + 1 -termal string of S2 ;

per cases
( t1 is 0 -termal or not t1 is 0 -termal )
;

end;

suppose
t1 is 0 -termal
; :: thesis: ( b_{1} in dom ((I2 -TermEval) | D2) & ((I1 -TermEval) | D1) . b_{1} = ((I2 -TermEval) | D2) . b_{1} )

then reconsider t11 = t1 as 0 -termal string of S1 ;

A33: ( t11 in X * & t11 in (S1 -termsOfMaxDepth) . 0 ) by FOMODEL1:def 33, TARSKI:def 3;

then A34: t11 in (XX *) /\ ((S1 -termsOfMaxDepth) . 0) by XBOOLE_0:def 4;

A35: ( (S2 -termsOfMaxDepth) . 0 c= AllTermsOf S2 & (S1 -termsOfMaxDepth) . 0 c= AllTermsOf S1 ) by FOMODEL1:2;

reconsider A1 = (X *) /\ ((S1 -termsOfMaxDepth) . 0) as Subset of (AllTermsOf S1) by A35, XBOOLE_1:1;

reconsider A2 = (X *) /\ ((S2 -termsOfMaxDepth) . 0) as Subset of (AllTermsOf S2) by A35, XBOOLE_1:1;

set g1 = (I1 -TermEval) | A1;

set g2 = (I2 -TermEval) | A2;

A36: ( dom ((I1 -TermEval) | A1) = A1 & dom ((I2 -TermEval) | A2) = A2 ) by PARTFUN1:def 2;

then A37: A1 c= A2 by A5, GRFUNC_1:2;

then ( t11 in A2 & t11 in A1 ) by A34;

then reconsider t2 = t11 as 0 -termal string of S2 by FOMODEL1:def 33;

t2 is 0 + (0 * NN) -termal ;

then t2 is 0 + NN -termal ;

then A38: ( t2 in XX * & t2 in (S2 -termsOfMaxDepth) . NN ) by TARSKI:def 3;

thus y in dom ((I2 -TermEval) | D2) by A20, XBOOLE_0:def 4, A38; :: thesis: ((I1 -TermEval) | D1) . y = ((I2 -TermEval) | D2) . y

reconsider D22 = D2 as non empty set by XBOOLE_0:def 4, A38;

reconsider A11 = A1, A22 = A2 as non empty set by A36, A5, A33, XBOOLE_0:def 4;

reconsider t111 = t11 as Element of A11 by A33, XBOOLE_0:def 4;

reconsider t02 = t11 as Element of A22 by A37, A34;

reconsider t20 = t2 as Element of D22 by A38, XBOOLE_0:def 4;

( (((I1 -TermEval) | D11) . y1) \+\ ((I1 -TermEval) . y1) = {} & (((I1 -TermEval) | ((X *) /\ ((S1 -termsOfMaxDepth) . 0))) . t111) \+\ ((I1 -TermEval) . t111) = {} & (((I2 -TermEval) | A2) . t02) \+\ ((I2 -TermEval) . t02) = {} & (((I2 -TermEval) | D22) . t20) \+\ ((I2 -TermEval) . t20) = {} ) ;

then A39: ( ((I1 -TermEval) | D1) . y = (I1 -TermEval) . y & ((I1 -TermEval) | ((X *) /\ ((S1 -termsOfMaxDepth) . 0))) . y = (I1 -TermEval) . y & ((I2 -TermEval) | ((X *) /\ ((S2 -termsOfMaxDepth) . 0))) . y = (I2 -TermEval) . y & ((I2 -TermEval) | D2) . y = (I2 -TermEval) . y ) by FOMODEL0:29;

thus ((I1 -TermEval) | D1) . y = ((I2 -TermEval) | D2) . y by A39, A5, A36, GRFUNC_1:2, A34; :: thesis: verum

end;A33: ( t11 in X * & t11 in (S1 -termsOfMaxDepth) . 0 ) by FOMODEL1:def 33, TARSKI:def 3;

then A34: t11 in (XX *) /\ ((S1 -termsOfMaxDepth) . 0) by XBOOLE_0:def 4;

A35: ( (S2 -termsOfMaxDepth) . 0 c= AllTermsOf S2 & (S1 -termsOfMaxDepth) . 0 c= AllTermsOf S1 ) by FOMODEL1:2;

reconsider A1 = (X *) /\ ((S1 -termsOfMaxDepth) . 0) as Subset of (AllTermsOf S1) by A35, XBOOLE_1:1;

reconsider A2 = (X *) /\ ((S2 -termsOfMaxDepth) . 0) as Subset of (AllTermsOf S2) by A35, XBOOLE_1:1;

set g1 = (I1 -TermEval) | A1;

set g2 = (I2 -TermEval) | A2;

A36: ( dom ((I1 -TermEval) | A1) = A1 & dom ((I2 -TermEval) | A2) = A2 ) by PARTFUN1:def 2;

then A37: A1 c= A2 by A5, GRFUNC_1:2;

then ( t11 in A2 & t11 in A1 ) by A34;

then reconsider t2 = t11 as 0 -termal string of S2 by FOMODEL1:def 33;

t2 is 0 + (0 * NN) -termal ;

then t2 is 0 + NN -termal ;

then A38: ( t2 in XX * & t2 in (S2 -termsOfMaxDepth) . NN ) by TARSKI:def 3;

thus y in dom ((I2 -TermEval) | D2) by A20, XBOOLE_0:def 4, A38; :: thesis: ((I1 -TermEval) | D1) . y = ((I2 -TermEval) | D2) . y

reconsider D22 = D2 as non empty set by XBOOLE_0:def 4, A38;

reconsider A11 = A1, A22 = A2 as non empty set by A36, A5, A33, XBOOLE_0:def 4;

reconsider t111 = t11 as Element of A11 by A33, XBOOLE_0:def 4;

reconsider t02 = t11 as Element of A22 by A37, A34;

reconsider t20 = t2 as Element of D22 by A38, XBOOLE_0:def 4;

( (((I1 -TermEval) | D11) . y1) \+\ ((I1 -TermEval) . y1) = {} & (((I1 -TermEval) | ((X *) /\ ((S1 -termsOfMaxDepth) . 0))) . t111) \+\ ((I1 -TermEval) . t111) = {} & (((I2 -TermEval) | A2) . t02) \+\ ((I2 -TermEval) . t02) = {} & (((I2 -TermEval) | D22) . t20) \+\ ((I2 -TermEval) . t20) = {} ) ;

then A39: ( ((I1 -TermEval) | D1) . y = (I1 -TermEval) . y & ((I1 -TermEval) | ((X *) /\ ((S1 -termsOfMaxDepth) . 0))) . y = (I1 -TermEval) . y & ((I2 -TermEval) | ((X *) /\ ((S2 -termsOfMaxDepth) . 0))) . y = (I2 -TermEval) . y & ((I2 -TermEval) | D2) . y = (I2 -TermEval) . y ) by FOMODEL0:29;

thus ((I1 -TermEval) | D1) . y = ((I2 -TermEval) | D2) . y by A39, A5, A36, GRFUNC_1:2, A34; :: thesis: verum

suppose
not t1 is 0 -termal
; :: thesis: ( b_{1} in dom ((I2 -TermEval) | D2) & ((I1 -TermEval) | D1) . b_{1} = ((I2 -TermEval) | D2) . b_{1} )

then
o1 is operational
by FOMODEL1:16;

then consider n1 being Nat such that

A40: |.(ar o1).| = n1 + 1 by NAT_1:6;

reconsider nn1 = n1 as Element of NAT by ORDINAL1:def 12;

reconsider st11 = SubTerms t1 as nn1 + 1 -element Element of (AllTermsOf S1) * by A40;

A41: not st11 is {} * -valued ;

st11 is (AllSymbolsOf S2) * -valued by XBOOLE_1:1, A32, RELAT_1:def 19;

then (S2 -multiCat) . st11 <> {} by FOMODEL0:52, A41;

then A42: (S1 -multiCat) . (SubTerms t1) = (S2 -multiCat) . (SubTerms t1) by FOMODEL0:52;

A43: t1 = t2 by FOMODEL1:def 37, A42;

then ( t1 in X * & t1 in (S2 -termsOfMaxDepth) . NN ) by FOMODEL1:def 33, TARSKI:def 3;

hence y in dom ((I2 -TermEval) | D2) by A20, XBOOLE_0:def 4; :: thesis: ((I1 -TermEval) | D1) . y = ((I2 -TermEval) | D2) . y

A44: ( t2 in (S2 -termsOfMaxDepth) . NN & t2 in X * ) by FOMODEL1:def 37, A42, A23, FOMODEL1:def 33;

reconsider D22 = D2 as non empty set by A44, XBOOLE_0:def 4;

reconsider tt2 = t2 as Element of D22 by A44, XBOOLE_0:def 4;

A45: (S2 -firstChar) . t2 = t2 . 1 by FOMODEL0:6

.= o2 by FINSEQ_1:41 ;

then A46: st22 = SubTerms t2 by FOMODEL1:def 37;

A47: (I1 -TermEval) | d1 = ((I2 -TermEval) | d2) | d1 by A18, GRFUNC_1:34, A20

.= (I2 -TermEval) | (d12 null d2) by RELAT_1:71 ;

( (((I1 -TermEval) | D11) . y1) \+\ ((I1 -TermEval) . y1) = {} & (((I2 -TermEval) | D22) . tt2) \+\ ((I2 -TermEval) . tt2) = {} ) ;

then A48: ( ((I1 -TermEval) | D1) . y1 = (I1 -TermEval) . y1 & ((I2 -TermEval) | D2) . t2 = (I2 -TermEval) . t2 ) by FOMODEL0:29;

hence ((I1 -TermEval) | D1) . y = (I1 . o1) . ((I1 -TermEval) * (SubTerms t1)) by FOMODEL2:21

.= (I1 . o1) . (((I1 -TermEval) | d1) * (SubTerms t1)) by RELAT_1:165, A20, A30, A29, XBOOLE_1:19

.= (I1 . o1) . ((I2 -TermEval) * (SubTerms t1)) by RELAT_1:165, A20, A30, A29, XBOOLE_1:19, A47

.= ((I2 -TermEval) | D2) . y by A43, A48, FOMODEL2:21, A45, A46, A28 ;

:: thesis: verum

end;then consider n1 being Nat such that

A40: |.(ar o1).| = n1 + 1 by NAT_1:6;

reconsider nn1 = n1 as Element of NAT by ORDINAL1:def 12;

reconsider st11 = SubTerms t1 as nn1 + 1 -element Element of (AllTermsOf S1) * by A40;

A41: not st11 is {} * -valued ;

st11 is (AllSymbolsOf S2) * -valued by XBOOLE_1:1, A32, RELAT_1:def 19;

then (S2 -multiCat) . st11 <> {} by FOMODEL0:52, A41;

then A42: (S1 -multiCat) . (SubTerms t1) = (S2 -multiCat) . (SubTerms t1) by FOMODEL0:52;

A43: t1 = t2 by FOMODEL1:def 37, A42;

then ( t1 in X * & t1 in (S2 -termsOfMaxDepth) . NN ) by FOMODEL1:def 33, TARSKI:def 3;

hence y in dom ((I2 -TermEval) | D2) by A20, XBOOLE_0:def 4; :: thesis: ((I1 -TermEval) | D1) . y = ((I2 -TermEval) | D2) . y

A44: ( t2 in (S2 -termsOfMaxDepth) . NN & t2 in X * ) by FOMODEL1:def 37, A42, A23, FOMODEL1:def 33;

reconsider D22 = D2 as non empty set by A44, XBOOLE_0:def 4;

reconsider tt2 = t2 as Element of D22 by A44, XBOOLE_0:def 4;

A45: (S2 -firstChar) . t2 = t2 . 1 by FOMODEL0:6

.= o2 by FINSEQ_1:41 ;

then A46: st22 = SubTerms t2 by FOMODEL1:def 37;

A47: (I1 -TermEval) | d1 = ((I2 -TermEval) | d2) | d1 by A18, GRFUNC_1:34, A20

.= (I2 -TermEval) | (d12 null d2) by RELAT_1:71 ;

( (((I1 -TermEval) | D11) . y1) \+\ ((I1 -TermEval) . y1) = {} & (((I2 -TermEval) | D22) . tt2) \+\ ((I2 -TermEval) . tt2) = {} ) ;

then A48: ( ((I1 -TermEval) | D1) . y1 = (I1 -TermEval) . y1 & ((I2 -TermEval) | D2) . t2 = (I2 -TermEval) . t2 ) by FOMODEL0:29;

hence ((I1 -TermEval) | D1) . y = (I1 . o1) . ((I1 -TermEval) * (SubTerms t1)) by FOMODEL2:21

.= (I1 . o1) . (((I1 -TermEval) | d1) * (SubTerms t1)) by RELAT_1:165, A20, A30, A29, XBOOLE_1:19

.= (I1 . o1) . ((I2 -TermEval) * (SubTerms t1)) by RELAT_1:165, A20, A30, A29, XBOOLE_1:19, A47

.= ((I2 -TermEval) | D2) . y by A43, A48, FOMODEL2:21, A45, A46, A28 ;

:: thesis: verum

now :: thesis: for x being set st x in dom ((I1 -TermEval) | (X *)) holds

( x in dom ((I2 -TermEval) | (X *)) & ((I1 -TermEval) | (X *)) . x = ((I2 -TermEval) | (X *)) . x )

hence
(I1 -TermEval) | (X *) c= (I2 -TermEval) | (X *)
by FOMODEL0:51; :: thesis: verum( x in dom ((I2 -TermEval) | (X *)) & ((I1 -TermEval) | (X *)) . x = ((I2 -TermEval) | (X *)) . x )

set g1 = (I1 -TermEval) | (X *);

set g2 = (I2 -TermEval) | (X *);

A50: ( dom ((I1 -TermEval) | (X *)) = (X *) /\ (AllTermsOf S1) & dom ((I2 -TermEval) | (X *)) = (X *) /\ (AllTermsOf S2) ) by RELAT_1:61, A3;

let x be set ; :: thesis: ( x in dom ((I1 -TermEval) | (X *)) implies ( x in dom ((I2 -TermEval) | (X *)) & ((I1 -TermEval) | (X *)) . x = ((I2 -TermEval) | (X *)) . x ) )

assume A51: x in dom ((I1 -TermEval) | (X *)) ; :: thesis: ( x in dom ((I2 -TermEval) | (X *)) & ((I1 -TermEval) | (X *)) . x = ((I2 -TermEval) | (X *)) . x )

then x in (X *) /\ (AllTermsOf S1) by RELAT_1:61, A3;

then reconsider t1 = x as termal string of S1 ;

set m1 = Depth t1;

reconsider mm1 = Depth t1 as Element of NAT by ORDINAL1:def 12;

reconsider t11 = t1 as Depth t1 -termal string of S1 by FOMODEL1:def 40;

A52: ( t11 in (S1 -termsOfMaxDepth) . (Depth t1) & x in X * ) by A51, FOMODEL1:def 33;

then A53: ( x in (X *) /\ ((S1 -termsOfMaxDepth) . (Depth t1)) & (S1 -termsOfMaxDepth) . mm1 c= AllTermsOf S1 & (S2 -termsOfMaxDepth) . mm1 c= AllTermsOf S2 ) by XBOOLE_0:def 4, FOMODEL1:2;

then reconsider D1 = (X *) /\ ((S1 -termsOfMaxDepth) . (Depth t1)) as non empty Subset of (AllTermsOf S1) by XBOOLE_1:1;

reconsider D2 = (X *) /\ ((S2 -termsOfMaxDepth) . (Depth t1)) as Subset of (AllTermsOf S2) by XBOOLE_1:1, A53;

reconsider t111 = t1 as Element of D1 by A52, XBOOLE_0:def 4;

set f1 = (I1 -TermEval) | D1;

set f2 = (I2 -TermEval) | D2;

A54: ( dom ((I1 -TermEval) | D1) = D1 & dom ((I2 -TermEval) | D2) = D2 ) by PARTFUN1:def 2;

( x in dom ((I1 -TermEval) | D1) & (I1 -TermEval) | D1 c= (I2 -TermEval) | D2 ) by A49, A53, PARTFUN1:def 2;

then A55: ( x in dom ((I2 -TermEval) | D2) & ((I1 -TermEval) | D1) . x = ((I2 -TermEval) | D2) . x ) by FOMODEL0:51;

then A56: ( x in (X *) /\ (AllTermsOf S2) & x in D2 ) by XBOOLE_0:def 4, A54;

hence x in dom ((I2 -TermEval) | (X *)) by RELAT_1:61, A3; :: thesis: ((I1 -TermEval) | (X *)) . x = ((I2 -TermEval) | (X *)) . x

thus ((I1 -TermEval) | (X *)) . x = (I1 -TermEval) . t111 by A51, FUNCT_1:47

.= ((I1 -TermEval) | D1) . t111 by A54, FUNCT_1:47

.= (I2 -TermEval) . t111 by A55, FUNCT_1:49

.= ((I2 -TermEval) | (X *)) . x by A56, A50, FUNCT_1:47 ; :: thesis: verum

end;set g2 = (I2 -TermEval) | (X *);

A50: ( dom ((I1 -TermEval) | (X *)) = (X *) /\ (AllTermsOf S1) & dom ((I2 -TermEval) | (X *)) = (X *) /\ (AllTermsOf S2) ) by RELAT_1:61, A3;

let x be set ; :: thesis: ( x in dom ((I1 -TermEval) | (X *)) implies ( x in dom ((I2 -TermEval) | (X *)) & ((I1 -TermEval) | (X *)) . x = ((I2 -TermEval) | (X *)) . x ) )

assume A51: x in dom ((I1 -TermEval) | (X *)) ; :: thesis: ( x in dom ((I2 -TermEval) | (X *)) & ((I1 -TermEval) | (X *)) . x = ((I2 -TermEval) | (X *)) . x )

then x in (X *) /\ (AllTermsOf S1) by RELAT_1:61, A3;

then reconsider t1 = x as termal string of S1 ;

set m1 = Depth t1;

reconsider mm1 = Depth t1 as Element of NAT by ORDINAL1:def 12;

reconsider t11 = t1 as Depth t1 -termal string of S1 by FOMODEL1:def 40;

A52: ( t11 in (S1 -termsOfMaxDepth) . (Depth t1) & x in X * ) by A51, FOMODEL1:def 33;

then A53: ( x in (X *) /\ ((S1 -termsOfMaxDepth) . (Depth t1)) & (S1 -termsOfMaxDepth) . mm1 c= AllTermsOf S1 & (S2 -termsOfMaxDepth) . mm1 c= AllTermsOf S2 ) by XBOOLE_0:def 4, FOMODEL1:2;

then reconsider D1 = (X *) /\ ((S1 -termsOfMaxDepth) . (Depth t1)) as non empty Subset of (AllTermsOf S1) by XBOOLE_1:1;

reconsider D2 = (X *) /\ ((S2 -termsOfMaxDepth) . (Depth t1)) as Subset of (AllTermsOf S2) by XBOOLE_1:1, A53;

reconsider t111 = t1 as Element of D1 by A52, XBOOLE_0:def 4;

set f1 = (I1 -TermEval) | D1;

set f2 = (I2 -TermEval) | D2;

A54: ( dom ((I1 -TermEval) | D1) = D1 & dom ((I2 -TermEval) | D2) = D2 ) by PARTFUN1:def 2;

( x in dom ((I1 -TermEval) | D1) & (I1 -TermEval) | D1 c= (I2 -TermEval) | D2 ) by A49, A53, PARTFUN1:def 2;

then A55: ( x in dom ((I2 -TermEval) | D2) & ((I1 -TermEval) | D1) . x = ((I2 -TermEval) | D2) . x ) by FOMODEL0:51;

then A56: ( x in (X *) /\ (AllTermsOf S2) & x in D2 ) by XBOOLE_0:def 4, A54;

hence x in dom ((I2 -TermEval) | (X *)) by RELAT_1:61, A3; :: thesis: ((I1 -TermEval) | (X *)) . x = ((I2 -TermEval) | (X *)) . x

thus ((I1 -TermEval) | (X *)) . x = (I1 -TermEval) . t111 by A51, FUNCT_1:47

.= ((I1 -TermEval) | D1) . t111 by A54, FUNCT_1:47

.= (I2 -TermEval) . t111 by A55, FUNCT_1:49

.= ((I2 -TermEval) | (X *)) . x by A56, A50, FUNCT_1:47 ; :: thesis: verum