let X be non empty set ; :: thesis: for S being SigmaField of X
for M being sigma_Measure of S
for f, g being PartFunc of X,ExtREAL st ex E1 being Element of S st
( E1 = dom f & f is E1 -measurable ) & ex E2 being Element of S st
( E2 = dom g & g is E2 -measurable ) holds
ex E being Element of S st
( E = dom (f + g) & f + g is E -measurable )
let S be SigmaField of X; :: thesis: for M being sigma_Measure of S
for f, g being PartFunc of X,ExtREAL st ex E1 being Element of S st
( E1 = dom f & f is E1 -measurable ) & ex E2 being Element of S st
( E2 = dom g & g is E2 -measurable ) holds
ex E being Element of S st
( E = dom (f + g) & f + g is E -measurable )
let M be sigma_Measure of S; :: thesis: for f, g being PartFunc of X,ExtREAL st ex E1 being Element of S st
( E1 = dom f & f is E1 -measurable ) & ex E2 being Element of S st
( E2 = dom g & g is E2 -measurable ) holds
ex E being Element of S st
( E = dom (f + g) & f + g is E -measurable )
let f, g be PartFunc of X,ExtREAL; :: thesis: ( ex E1 being Element of S st
( E1 = dom f & f is E1 -measurable ) & ex E2 being Element of S st
( E2 = dom g & g is E2 -measurable ) implies ex E being Element of S st
( E = dom (f + g) & f + g is E -measurable ) )
assume that
A1: ex E1 being Element of S st
( E1 = dom f & f is E1 -measurable ) and
A2: ex E2 being Element of S st
( E2 = dom g & g is E2 -measurable ) ; :: thesis: ex E being Element of S st
( E = dom (f + g) & f + g is E -measurable )
consider E1 being Element of S such that
A3: E1 = dom f and
A4: f is E1 -measurable by A1;
consider E2 being Element of S such that
A5: E2 = dom g and
A6: g is E2 -measurable by A2;
set E3 = E1 /\ E2;
set g1 = g | (E1 /\ E2);
A7: (g | (E1 /\ E2)) " {-infty} = (E1 /\ E2) /\ (g " {-infty}) by FUNCT_1:70;
set f1 = f | (E1 /\ E2);
dom (f | (E1 /\ E2)) = (dom f) /\ (E1 /\ E2) by RELAT_1:61;
then A8: dom (f | (E1 /\ E2)) = E1 /\ E2 by A3, XBOOLE_1:17, XBOOLE_1:28;
g is E1 /\ E2 -measurable by A6, MESFUNC1:30, XBOOLE_1:17;
then A9: g | (E1 /\ E2) is E1 /\ E2 -measurable by Lm6;
A10: (g | (E1 /\ E2)) " {+infty} = (E1 /\ E2) /\ (g " {+infty}) by FUNCT_1:70;
dom (g | (E1 /\ E2)) = (dom g) /\ (E1 /\ E2) by RELAT_1:61;
then A11: dom (g | (E1 /\ E2)) = E1 /\ E2 by A5, XBOOLE_1:17, XBOOLE_1:28;
(f | (E1 /\ E2)) " {+infty} = (E1 /\ E2) /\ (f " {+infty}) by FUNCT_1:70;
then A12: ((f | (E1 /\ E2)) " {+infty}) /\ ((g | (E1 /\ E2)) " {-infty}) = (f " {+infty}) /\ ((E1 /\ E2) /\ ((E1 /\ E2) /\ (g " {-infty}))) by A7, XBOOLE_1:16
.= (f " {+infty}) /\ (((E1 /\ E2) /\ (E1 /\ E2)) /\ (g " {-infty})) by XBOOLE_1:16
.= ((f " {+infty}) /\ (g " {-infty})) /\ (E1 /\ E2) by XBOOLE_1:16 ;
A13: dom ((f | (E1 /\ E2)) + (g | (E1 /\ E2))) = ((dom (f | (E1 /\ E2))) /\ (dom (g | (E1 /\ E2)))) \ ((((f | (E1 /\ E2)) " {-infty}) /\ ((g | (E1 /\ E2)) " {+infty})) \/ (((f | (E1 /\ E2)) " {+infty}) /\ ((g | (E1 /\ E2)) " {-infty}))) by MESFUNC1:def 3;
f is E1 /\ E2 -measurable by A4, MESFUNC1:30, XBOOLE_1:17;
then f | (E1 /\ E2) is E1 /\ E2 -measurable by Lm6;
then consider E being Element of S such that
A14: E = dom ((f | (E1 /\ E2)) + (g | (E1 /\ E2))) and
A15: (f | (E1 /\ E2)) + (g | (E1 /\ E2)) is E -measurable by A9, A8, A11, Lm7;
take E ; :: thesis: ( E = dom (f + g) & f + g is E -measurable )
A16: dom ((f + g) | E) = (dom (f + g)) /\ E by RELAT_1:61;
(f | (E1 /\ E2)) " {-infty} = (E1 /\ E2) /\ (f " {-infty}) by FUNCT_1:70;
then ((f | (E1 /\ E2)) " {-infty}) /\ ((g | (E1 /\ E2)) " {+infty}) = (f " {-infty}) /\ ((E1 /\ E2) /\ ((E1 /\ E2) /\ (g " {+infty}))) by A10, XBOOLE_1:16
.= (f " {-infty}) /\ (((E1 /\ E2) /\ (E1 /\ E2)) /\ (g " {+infty})) by XBOOLE_1:16
.= ((f " {-infty}) /\ (g " {+infty})) /\ (E1 /\ E2) by XBOOLE_1:16 ;
then A17: (((f | (E1 /\ E2)) " {-infty}) /\ ((g | (E1 /\ E2)) " {+infty})) \/ (((f | (E1 /\ E2)) " {+infty}) /\ ((g | (E1 /\ E2)) " {-infty})) = (E1 /\ E2) /\ (((f " {-infty}) /\ (g " {+infty})) \/ ((f " {+infty}) /\ (g " {-infty}))) by A12, XBOOLE_1:23;
A18: dom (f + g) = ((dom f) /\ (dom g)) \ (((f " {-infty}) /\ (g " {+infty})) \/ ((f " {+infty}) /\ (g " {-infty}))) by MESFUNC1:def 3;
then A19: dom (f + g) = E by A3, A5, A8, A11, A14, A13, A17, XBOOLE_1:47;

now :: thesis: for v being Element of X st v in dom ((f + g) | E) holds
((f + g) | E) . v = ((f | (E1 /\ E2)) + (g | (E1 /\ E2))) . v

let v be Element of X; :: thesis: ( v in dom ((f + g) | E) implies ((f + g) | E) . v = ((f | (E1 /\ E2)) + (g | (E1 /\ E2))) . v )
assume A20: v in dom ((f + g) | E) ; :: thesis: ((f + g) | E) . v = ((f | (E1 /\ E2)) + (g | (E1 /\ E2))) . v
then A21: v in (dom (f + g)) /\ E by RELAT_1:61;
then A22: v in dom (f + g) by XBOOLE_0:def 4;
A23: ((f + g) | E) . v = (f + g) . v by A20, FUNCT_1:47
.= (f . v) + (g . v) by A22, MESFUNC1:def 3 ;
A24: v in E by A21, XBOOLE_0:def 4;
A25: E c= E1 /\ E2 by A8, A11, A14, A13, XBOOLE_1:36;
((f | (E1 /\ E2)) + (g | (E1 /\ E2))) . v = ((f | (E1 /\ E2)) . v) + ((g | (E1 /\ E2)) . v) by A14, A19, A16, A20, MESFUNC1:def 3
.= (f . v) + ((g | (E1 /\ E2)) . v) by A8, A24, A25, FUNCT_1:47 ;
hence ((f + g) | E) . v = ((f | (E1 /\ E2)) + (g | (E1 /\ E2))) . v by A11, A24, A25, A23, FUNCT_1:47; :: thesis: verum

end;

then (f + g) | E = (f | (E1 /\ E2)) + (g | (E1 /\ E2)) by A14, A19, A16, PARTFUN1:5;
hence ( E = dom (f + g) & f + g is E -measurable ) by A3, A5, A8, A11, A14, A15, A13, A17, A18, Lm6, XBOOLE_1:47; :: thesis: verum