let m, n be Nat; :: thesis: for S being Language
for U being non empty set
for I being Element of U -InterpretersOf S holds (I,m) -TruthEval c= (I,(m + n)) -TruthEval
let S be Language; :: thesis: for U being non empty set
for I being Element of U -InterpretersOf S holds (I,m) -TruthEval c= (I,(m + n)) -TruthEval
let U be non empty set ; :: thesis: for I being Element of U -InterpretersOf S holds (I,m) -TruthEval c= (I,(m + n)) -TruthEval
set UI = U -InterpretersOf S;
set SS = AllSymbolsOf S;
let I be Element of U -InterpretersOf S; :: thesis: (I,m) -TruthEval c= (I,(m + n)) -TruthEval
set IT1 = (I,m) -TruthEval ;
set IT2 = (I,(m + n)) -TruthEval ;
set f = (S,U) -TruthEval m;
set g = (S,U) -TruthEval (m + n);
reconsider F = curry ((S,U) -TruthEval m), G = curry ((S,U) -TruthEval (m + n)) as Function of (U -InterpretersOf S),(PFuncs ((((AllSymbolsOf S) *) \ {{}}),BOOLEAN)) by Lm28;
Z0: ( (I,m) -TruthEval = F . I & (I,(m + n)) -TruthEval = G . I & dom F = U -InterpretersOf S ) by FUNCT_2:def 1;
B2: for x being set st x in dom ((I,m) -TruthEval) holds
( x in dom ((I,(m + n)) -TruthEval) & ((I,m) -TruthEval) . x = ((I,(m + n)) -TruthEval) . x )

proof

let x be set ; :: thesis: ( x in dom ((I,m) -TruthEval) implies ( x in dom ((I,(m + n)) -TruthEval) & ((I,m) -TruthEval) . x = ((I,(m + n)) -TruthEval) . x ) )
assume Z1: x in dom ((I,m) -TruthEval) ; :: thesis: ( x in dom ((I,(m + n)) -TruthEval) & ((I,m) -TruthEval) . x = ((I,(m + n)) -TruthEval) . x )
then D2: [I,x] in dom ((S,U) -TruthEval m) by Z0, FUNCT_5:31;
then D1: ( [I,x] in dom ((S,U) -TruthEval (m + n)) & ((S,U) -TruthEval (m + n)) . [I,x] = ((S,U) -TruthEval m) . [I,x] ) by Lm26;
then ( x in dom ((I,(m + n)) -TruthEval) & ((I,(m + n)) -TruthEval) . x = ((S,U) -TruthEval (m + n)) . (I,x) ) by FUNCT_5:20;
then ((I,(m + n)) -TruthEval) . x = ((S,U) -TruthEval m) . (I,x) by D2, Lm26
.= ((I,m) -TruthEval) . x by Z1, Z0, FUNCT_5:31 ;
hence ( x in dom ((I,(m + n)) -TruthEval) & ((I,m) -TruthEval) . x = ((I,(m + n)) -TruthEval) . x ) by D1, FUNCT_5:20; :: thesis: verum

end;

B3: ( ( for x being set st x in dom ((I,m) -TruthEval) holds
x in dom ((I,(m + n)) -TruthEval) ) & ( for x being set st x in dom ((I,m) -TruthEval) holds
((I,m) -TruthEval) . x = ((I,(m + n)) -TruthEval) . x ) ) by B2;
then dom ((I,m) -TruthEval) c= dom ((I,(m + n)) -TruthEval) by TARSKI:def 3;
hence (I,m) -TruthEval c= (I,(m + n)) -TruthEval by B3, GRFUNC_1:2; :: thesis: verum