let m, n be Nat; 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; 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 ; 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; (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 ;
( 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)
;
( 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;
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; verum