let m be Nat; :: thesis: for S being Language
for U1, U2 being non empty set
for I1 being Element of U1 -InterpretersOf S
for I2 being Element of U2 -InterpretersOf S holds dom ((I1,m) -TruthEval) c= dom ((I2,m) -TruthEval)
let S be Language; :: thesis: for U1, U2 being non empty set
for I1 being Element of U1 -InterpretersOf S
for I2 being Element of U2 -InterpretersOf S holds dom ((I1,m) -TruthEval) c= dom ((I2,m) -TruthEval)
let U1, U2 be non empty set ; :: thesis: for I1 being Element of U1 -InterpretersOf S
for I2 being Element of U2 -InterpretersOf S holds dom ((I1,m) -TruthEval) c= dom ((I2,m) -TruthEval)
reconsider mm = m as Element of NAT by ORDINAL1:def 12;
set II1 = U1 -InterpretersOf S;
set II2 = U2 -InterpretersOf S;
set f = ((S,U1) -TruthEval) . mm;
set SS = AllSymbolsOf S;
set ff1 = (S,U1) -TruthEval mm;
set ff2 = (S,U2) -TruthEval mm;
set g = ((S,U2) -TruthEval) . mm;
let I1 be Element of U1 -InterpretersOf S; :: thesis: for I2 being Element of U2 -InterpretersOf S holds dom ((I1,m) -TruthEval) c= dom ((I2,m) -TruthEval)
let I2 be Element of U2 -InterpretersOf S; :: thesis: dom ((I1,m) -TruthEval) c= dom ((I2,m) -TruthEval)
B0: ( ((S,U1) -TruthEval) . mm = (S,U1) -TruthEval mm & ((S,U2) -TruthEval) . mm = (S,U2) -TruthEval mm ) by DefTruth2;
set F1 = (I1,m) -TruthEval ;
set F2 = (I2,m) -TruthEval ;
B10: ( (curry (((S,U1) -TruthEval) . mm)) . I1 = (I1,m) -TruthEval & (curry (((S,U2) -TruthEval) . mm)) . I2 = (I2,m) -TruthEval ) by DefTruth2;
then reconsider f1 = (curry (((S,U1) -TruthEval) . mm)) . I1, f2 = (curry (((S,U2) -TruthEval) . mm)) . I2 as Element of PFuncs ((((AllSymbolsOf S) *) \ {{}}),BOOLEAN) ;
reconsider F = curry (((S,U1) -TruthEval) . mm) as Function of (U1 -InterpretersOf S),(PFuncs ((((AllSymbolsOf S) *) \ {{}}),BOOLEAN)) by Lm22;
Z1: I1 in U1 -InterpretersOf S ;
((S,U1) -TruthEval) . mm is Element of PFuncs ([:(U1 -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],BOOLEAN) ;
then dom (((S,U1) -TruthEval) . mm) c= [:(U1 -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):] by RELAT_1:def 18;
then B3: uncurry F = ((S,U1) -TruthEval) . mm by FUNCT_5:50;

now

let ww be set ; :: thesis: ( ww in dom f1 implies ww in dom f2 )
assume C1: ww in dom f1 ; :: thesis: ww in dom f2
then reconsider w = ww as Element of ((AllSymbolsOf S) *) \ {{}} ;
( I1 in dom F & f1 = F . I1 & ww in dom f1 ) by Z1, C1, FUNCT_2:def 1;
then [I1,w] in dom ((S,U1) -TruthEval mm) by B0, B3, FUNCT_5:38;
then [I2,ww] in dom (((S,U2) -TruthEval) . mm) by B0, Lm23;
hence ww in dom f2 by FUNCT_5:20; :: thesis: verum

end;

hence dom ((I1,m) -TruthEval) c= dom ((I2,m) -TruthEval) by B10, TARSKI:def 3; :: thesis: verum