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 *) )
B3:
( 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 Z2:
I1 | X = I2 | X
; ( not the adicity of S1 | X = the adicity of S2 | X or (I1 -TermEval) | (X *) c= (I2 -TermEval) | (X *) )
then B2:
( dom (I1 -TermEval) = AllTermsOf S1 & dom (I2 -TermEval) = AllTermsOf S2 & I1 | X = I2 | X )
by FUNCT_2:def 1;
BB4: X /\ (dom I1) =
dom (I2 | X)
by Z2, RELAT_1:61
.=
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 } ;
B0:
S1[ 0 ]
proof
Z3:
(
(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 Z3, XBOOLE_1:1;
reconsider D2 =
(X *) /\ ((S2 -termsOfMaxDepth) . 0) as
Subset of
(AllTermsOf S2) by Z3, XBOOLE_1:1;
set f1 =
(I1 -TermEval) | D1;
set f2 =
(I2 -TermEval) | D2;
C1:
(
dom ((I1 -TermEval) | D1) = D1 &
dom ((I2 -TermEval) | D2) = D2 )
by PARTFUN1:def 2;
now 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 Z7:
x in dom ((I1 -TermEval) | D1)
;
( x in dom ((I2 -TermEval) | D2) & ((I2 -TermEval) | D2) . x = ((I1 -TermEval) | D1) . x )then C7:
x in (X *) /\ (AtomicTermsOf S1)
by C1, FOMODEL1:def 30;
then C6:
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 Z7, C1;
x in H1(
Y1)
by C6, FINSEQ_2:96;
then consider y1 being
Element of
Y1 such that C0:
x = <*y1*>
;
y1 in Y1
;
then reconsider l1 =
y1 as
literal Element of
S1 ;
(
l1 in X &
l1 in OwnSymbolsOf S1 )
by FOMODEL1:def 19, XBOOLE_0:def 4;
then
l1 in X /\ (OwnSymbolsOf S2)
by BB4, B3, 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 Z2, FUNCT_2:def 1
.=
(abs (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 C7;
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 Z7;
reconsider x1 =
t1 as
Element of
D11 by Z7, PARTFUN1:def 2;
CC8:
(
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 CC8, XBOOLE_0:def 4;
<*ll2*> in H1(
Y2)
;
then
<*ll2*> in 1
-tuples_on Y2
by FINSEQ_2:96;
then CC11:
x in (X *) /\ (AtomicTermsOf S2)
by C0, FOMODEL0:2;
reconsider D22 =
D2 as non
empty Subset of
(AllTermsOf S2) by CC11, FOMODEL1:def 30;
reconsider x2 =
x as
Element of
D22 by CC11, FOMODEL1:def 30;
C10:
t1 . 1
= y1
by C0, 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 C12:
(
(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 C10, Z2, C12, FOMODEL0:6
.=
(I2 . (<*l2*> . 1)) . {}
by FINSEQ_1:40
.=
(I2 . ((S2 -firstChar) . <*l2*>)) . ((I2 -TermEval) * (SubTerms <*l2*>))
by FOMODEL0:6
.=
((I2 -TermEval) | D2) . x
by C0, C12, FOMODEL2:21
;
hence
(
x in dom ((I2 -TermEval) | D2) &
((I2 -TermEval) | D2) . x = ((I1 -TermEval) | D1) . x )
by C1, CC11, FOMODEL1:def 30;
verum end;
hence
S1[
0 ]
by FOMODEL0:51;
verum
end;
assume B5:
the adicity of S1 | X = the adicity of S2 | X
; (I1 -TermEval) | (X *) c= (I2 -TermEval) | (X *)
B1:
for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be
Nat;
( S1[n] implies S1[n + 1] )
assume C0:
S1[
n]
;
S1[n + 1]
reconsider nn =
n,
NN =
n + 1 as
Element of
NAT by ORDINAL1:def 12;
Z3:
(
(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 Z3, XBOOLE_1:1;
reconsider D2 =
(X *) /\ ((S2 -termsOfMaxDepth) . NN),
d2 =
(X *) /\ ((S2 -termsOfMaxDepth) . nn) as
Subset of
(AllTermsOf S2) by Z3, XBOOLE_1:1;
set f1 =
(I1 -TermEval) | D1;
set f2 =
(I2 -TermEval) | D2;
C1:
(
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 C2:
d1 c= d2
by C0, GRFUNC_1:2;
reconsider d12 =
d1 as
Subset of
d2 by C0, C1, GRFUNC_1:2;
reconsider d21 =
d12 as
Subset of
(AllTermsOf S2) by XBOOLE_1:1;
now 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 D20:
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 D20, PARTFUN1:def 2;
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 =
abs (ar o1);
D9:
(
t1 in X * & not
t1 is
empty )
by TARSKI:def 3;
then reconsider XX =
X as non
empty set ;
DD1:
y1 in XX *
by TARSKI:def 3;
{(t1 . 1)} \ XX = {}
by DD1;
then DD3:
(
t1 . 1
in XX &
o1 = t1 . 1 )
by FOMODEL0:6, ZFMISC_1:60;
then
(
o1 in XX &
o1 in OwnSymbolsOf S1 )
by FOMODEL1:def 19;
then
o1 in XX /\ (OwnSymbolsOf S2)
by BB4, B3, 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 DD3;
(
( the adicity of S1 . ox) \+\ (( the adicity of S1 | XX) . ox) = {} &
( the adicity of S2 . ox) \+\ (( the adicity of S2 | XX) . ox) = {} )
;
then D19:
( 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 D19, B5;
then
not
o22 is
relational
;
then reconsider o2 =
o2 as
termal Element of
S2 ;
set m2 =
abs (ar o2);
D14:
(
(I1 . ox) \+\ ((I1 | XX) . ox) = {} &
(I2 . ox) \+\ ((I2 | XX) . ox) = {} )
;
then D17:
I1 . ox =
(I1 | XX) . o1
by FOMODEL0:29
.=
I2 . ox
by D14, Z2, FOMODEL0:29
;
set st1 =
SubTerms t1;
reconsider B =
rng t1 as non
empty Subset of
XX by DD1, RELAT_1:def 19;
(
rng (SubTerms t1) c= (rng t1) * &
B * c= XX * )
by RELAT_1:def 19;
then D2:
rng (SubTerms t1) c= XX *
by XBOOLE_1:1;
DD10:
rng (SubTerms t1) c= (S1 -termsOfMaxDepth) . n
by RELAT_1:def 19;
then
rng (SubTerms t1) c= d1
by D2, XBOOLE_1:19;
then D7:
(
rng (SubTerms t1) c= ((AllSymbolsOf S1) *) \ {{}} &
rng (SubTerms t1) c= d2 )
by C2, XBOOLE_1:1;
then
(
rng (SubTerms t1) c= ((AllSymbolsOf S1) *) \ {{}} &
rng (SubTerms t1) c= ((AllSymbolsOf S2) *) \ {{}} )
by XBOOLE_1:1;
then DD6:
(
rng (SubTerms t1) c= (AllSymbolsOf S1) * &
rng (SubTerms t1) c= (AllSymbolsOf S2) * )
by XBOOLE_1:1;
rng (SubTerms t1) c= (S2 -termsOfMaxDepth) . nn
by D7, XBOOLE_1:1;
then
SubTerms t1 is
(S2 -termsOfMaxDepth) . nn -valued
by RELAT_1:def 19;
then
SubTerms t1 is
abs (ar o2) -element FinSequence of
(S2 -termsOfMaxDepth) . nn
by B5, D19, FOMODEL0:26;
then reconsider st2 =
SubTerms t1 as
abs (ar o2) -element Element of
((S2 -termsOfMaxDepth) . nn) * by FINSEQ_1:def 11;
reconsider T2n =
(S2 -termsOfMaxDepth) . nn as non
empty Subset of
(AllTermsOf S2) by FOMODEL1:2;
st2 in T2n *
;
then reconsider st22 =
st2 as
abs (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 ;
EE2:
(
t11 in X * &
t11 in (S1 -termsOfMaxDepth) . 0 )
by FOMODEL1:def 33, TARSKI:def 3;
then E2:
t11 in (XX *) /\ ((S1 -termsOfMaxDepth) . 0)
by XBOOLE_0:def 4;
EE3:
(
(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 EE3, XBOOLE_1:1;
reconsider A2 =
(X *) /\ ((S2 -termsOfMaxDepth) . 0) as
Subset of
(AllTermsOf S2) by EE3, XBOOLE_1:1;
set g1 =
(I1 -TermEval) | A1;
set g2 =
(I2 -TermEval) | A2;
E1:
(
dom ((I1 -TermEval) | A1) = A1 &
dom ((I2 -TermEval) | A2) = A2 )
by PARTFUN1:def 2;
then EE4:
A1 c= A2
by B0, GRFUNC_1:2;
then
(
t11 in A2 &
t11 in A1 )
by E2;
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 EE6:
(
t2 in XX * &
t2 in (S2 -termsOfMaxDepth) . NN )
by FOMODEL1:def 33, TARSKI:def 3;
thus
y in dom ((I2 -TermEval) | D2)
by C1, EE6, XBOOLE_0:def 4;
((I1 -TermEval) | D1) . y = ((I2 -TermEval) | D2) . yreconsider D22 =
D2 as non
empty set by EE6, XBOOLE_0:def 4;
reconsider A11 =
A1,
A22 =
A2 as non
empty set by E1, B0, EE2, XBOOLE_0:def 4;
reconsider t111 =
t11 as
Element of
A11 by EE2, XBOOLE_0:def 4;
reconsider t02 =
t11 as
Element of
A22 by EE4, E2;
reconsider t20 =
t2 as
Element of
D22 by EE6, 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 E5:
(
((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 E5, B0, E1, E2, GRFUNC_1:2;
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 E0:
abs (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 E0;
E1:
not
st11 is
{} * -valued
;
st11 is
(AllSymbolsOf S2) * -valued
by DD6, RELAT_1:def 19;
then
(S2 -multiCat) . st11 <> {}
by E1, FOMODEL0:52;
then E3:
(S1 -multiCat) . (SubTerms t1) = (S2 -multiCat) . (SubTerms t1)
by FOMODEL0:52;
E4:
t1 = t2
by E3, FOMODEL1:def 37;
then
(
t1 in X * &
t1 in (S2 -termsOfMaxDepth) . NN )
by FOMODEL1:def 33, TARSKI:def 3;
hence
y in dom ((I2 -TermEval) | D2)
by C1, XBOOLE_0:def 4;
((I1 -TermEval) | D1) . y = ((I2 -TermEval) | D2) . yDD15:
(
t2 in (S2 -termsOfMaxDepth) . NN &
t2 in X * )
by E3, D9, FOMODEL1:def 33, FOMODEL1:def 37;
reconsider D22 =
D2 as non
empty set by DD15, XBOOLE_0:def 4;
reconsider tt2 =
t2 as
Element of
D22 by DD15, XBOOLE_0:def 4;
D12:
(S2 -firstChar) . t2 =
t2 . 1
by FOMODEL0:6
.=
o2
by FINSEQ_1:41
;
then D13:
st22 = SubTerms t2
by FOMODEL1:def 37;
D25:
(I1 -TermEval) | d1 =
((I2 -TermEval) | d2) | d1
by C0, C1, GRFUNC_1:34
.=
(I2 -TermEval) | (d12 null d2)
by RELAT_1:71
;
(
(((I1 -TermEval) | D11) . y1) \+\ ((I1 -TermEval) . y1) = {} &
(((I2 -TermEval) | D22) . tt2) \+\ ((I2 -TermEval) . tt2) = {} )
;
then D16:
(
((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 C1, DD10, D2, RELAT_1:165, XBOOLE_1:19
.=
(I1 . o1) . ((I2 -TermEval) * (SubTerms t1))
by C1, DD10, D2, D25, RELAT_1:165, XBOOLE_1:19
.=
((I2 -TermEval) | D2) . y
by E4, D16, D12, D13, D17, FOMODEL2:21
;
verum end; end;
hence
S1[
n + 1]
by FOMODEL0:51;
verum
end;
B6:
for n being Nat holds S1[n]
from NAT_1:sch 2(B0, B1);
now set g1 =
(I1 -TermEval) | (X *);
set g2 =
(I2 -TermEval) | (X *);
C4:
(
dom ((I1 -TermEval) | (X *)) = (X *) /\ (AllTermsOf S1) &
dom ((I2 -TermEval) | (X *)) = (X *) /\ (AllTermsOf S2) )
by B2, RELAT_1:61;
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 C2:
x in dom ((I1 -TermEval) | (X *))
;
( x in dom ((I2 -TermEval) | (X *)) & ((I1 -TermEval) | (X *)) . x = ((I2 -TermEval) | (X *)) . x )then C0:
x in (X *) /\ (AllTermsOf S1)
by B2, RELAT_1:61;
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;
C6:
(
t11 in (S1 -termsOfMaxDepth) . (Depth t1) &
x in X * )
by C0, FOMODEL1:def 33;
then C1:
(
x in (X *) /\ ((S1 -termsOfMaxDepth) . (Depth t1)) &
(S1 -termsOfMaxDepth) . mm1 c= AllTermsOf S1 &
(S2 -termsOfMaxDepth) . mm1 c= AllTermsOf S2 )
by FOMODEL1:2, XBOOLE_0:def 4;
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 C1, XBOOLE_1:1;
reconsider t111 =
t1 as
Element of
D1 by C6, XBOOLE_0:def 4;
set f1 =
(I1 -TermEval) | D1;
set f2 =
(I2 -TermEval) | D2;
C5:
(
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 B6, C1, PARTFUN1:def 2;
then C3:
(
x in dom ((I2 -TermEval) | D2) &
((I1 -TermEval) | D1) . x = ((I2 -TermEval) | D2) . x )
by FOMODEL0:51;
then C9:
(
x in (X *) /\ (AllTermsOf S2) &
x in D2 )
by C5, XBOOLE_0:def 4;
hence
x in dom ((I2 -TermEval) | (X *))
by B2, RELAT_1:61;
((I1 -TermEval) | (X *)) . x = ((I2 -TermEval) | (X *)) . xthus ((I1 -TermEval) | (X *)) . x =
(I1 -TermEval) . t111
by C2, FUNCT_1:47
.=
((I1 -TermEval) | D1) . t111
by C5, FUNCT_1:47
.=
(I2 -TermEval) . t111
by C3, C5, FUNCT_1:49
.=
((I2 -TermEval) | (X *)) . x
by C9, C4, FUNCT_1:47
;
verum end;
hence
(I1 -TermEval) | (X *) c= (I2 -TermEval) | (X *)
by FOMODEL0:51; verum