let m be Nat; 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; 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 ; 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; 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; 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;
hence
dom ((I1,m) -TruthEval) c= dom ((I2,m) -TruthEval)
by A2; verum