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)
A1: ( ((S,U1) -TruthEval) . mm = (S,U1) -TruthEval mm & ((S,U2) -TruthEval) . mm = (S,U2) -TruthEval mm ) by Def20;
set F1 = (I1,m) -TruthEval ;
set F2 = (I2,m) -TruthEval ;
A2: ( (curry (((S,U1) -TruthEval) . mm)) . I1 = (I1,m) -TruthEval & (curry (((S,U2) -TruthEval) . mm)) . I2 = (I2,m) -TruthEval ) by Def20;
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 Lm10;
A3: 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 A4: uncurry F = ((S,U1) -TruthEval) . mm by FUNCT_5:50;
now :: thesis: for ww being object st ww in dom f1 holds
ww in dom f2
let ww be object ; :: thesis: ( ww in dom f1 implies ww in dom f2 )
assume A5: 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 A3, FUNCT_2:def 1, A5;
then [I1,w] in dom ((S,U1) -TruthEval mm) by A1, A4, FUNCT_5:38;
then [I2,ww] in dom (((S,U2) -TruthEval) . mm) by A1, Lm9;
hence ww in dom f2 by FUNCT_5:20; :: thesis: verum
end;
hence dom ((I1,m) -TruthEval) c= dom ((I2,m) -TruthEval) by A2; :: thesis: verum