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 Lm11;
A1: ( (I,m) -TruthEval = F . I & (I,(m + n)) -TruthEval = G . I & dom F = U -InterpretersOf S ) by FUNCT_2:def 1;
A2: 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 A3: x in dom ((I,m) -TruthEval) ; :: thesis: ( x in dom ((I,(m + n)) -TruthEval) & ((I,m) -TruthEval) . x = ((I,(m + n)) -TruthEval) . x )
then A4: [I,x] in dom ((S,U) -TruthEval m) by A1, FUNCT_5:31;
then A5: ( [I,x] in dom ((S,U) -TruthEval (m + n)) & ((S,U) -TruthEval (m + n)) . [I,x] = ((S,U) -TruthEval m) . [I,x] ) by Lm7;
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 A4, Lm7
.= ((I,m) -TruthEval) . x by A3, FUNCT_5:31, A1 ;
hence ( x in dom ((I,(m + n)) -TruthEval) & ((I,m) -TruthEval) . x = ((I,(m + n)) -TruthEval) . x ) by A5, FUNCT_5:20; :: thesis: verum

end;

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