let X be set ; 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 ; 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; 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; 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; ( 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
; ( 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 S1[ Nat] means (I1 -TermEval) | ((X *) /\ ((S1 -termsOfMaxDepth) . $1)) c= (I2 -TermEval) | ((X *) /\ ((S2 -termsOfMaxDepth) . $1));
deffunc H1( set ) -> set = { <*x*> where x is Element of $1 : verum } ;
A5:
S1[ 0 ]
proof
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;
now 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 )let x be
set ;
( 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)
;
( 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 H1(
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 H1(
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;
verum end;
hence
S1[
0 ]
by FOMODEL0:51;
verum
end;
assume A16:
the adicity of S1 | X = the adicity of S2 | X
; (I1 -TermEval) | (X *) c= (I2 -TermEval) | (X *)
A17:
for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be
Nat;
( S1[n] implies S1[n + 1] )
assume A18:
S1[
n]
;
S1[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;
now 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 )let y be
set ;
( y in dom ((I1 -TermEval) | D1) implies ( b1 in dom ((I2 -TermEval) | D2) & ((I1 -TermEval) | D1) . b1 = ((I2 -TermEval) | D2) . b1 ) )assume A22:
y in dom ((I1 -TermEval) | D1)
;
( b1 in dom ((I2 -TermEval) | D2) & ((I1 -TermEval) | D1) . b1 = ((I2 -TermEval) | D2) . b1 )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 )
;
suppose
t1 is
0 -termal
;
( b1 in dom ((I2 -TermEval) | D2) & ((I1 -TermEval) | D1) . b1 = ((I2 -TermEval) | D2) . b1 )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;
((I1 -TermEval) | D1) . y = ((I2 -TermEval) | D2) . yreconsider 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;
verum end; suppose
not
t1 is
0 -termal
;
( b1 in dom ((I2 -TermEval) | D2) & ((I1 -TermEval) | D1) . b1 = ((I2 -TermEval) | D2) . b1 )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;
((I1 -TermEval) | D1) . y = ((I2 -TermEval) | D2) . yA44:
(
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
;
verum end; end;
hence
S1[
n + 1]
by FOMODEL0:51;
verum
end;
A49:
for n being Nat holds S1[n]
from NAT_1:sch 2(A5, A17);
now 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 )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 ;
( 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 *))
;
( 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;
((I1 -TermEval) | (X *)) . x = ((I2 -TermEval) | (X *)) . xthus ((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
;
verum end;
hence
(I1 -TermEval) | (X *) c= (I2 -TermEval) | (X *)
by FOMODEL0:51; verum