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_measurable_on E1 ) & ex E2 being Element of S st
( E2 = dom g & g is_measurable_on E2 ) holds
ex E being Element of S st
( E = dom (f + g) & f + g is_measurable_on E )
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_measurable_on E1 ) & ex E2 being Element of S st
( E2 = dom g & g is_measurable_on E2 ) holds
ex E being Element of S st
( E = dom (f + g) & f + g is_measurable_on E )
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_measurable_on E1 ) & ex E2 being Element of S st
( E2 = dom g & g is_measurable_on E2 ) holds
ex E being Element of S st
( E = dom (f + g) & f + g is_measurable_on E )
let f, g be PartFunc of X,ExtREAL; :: thesis: ( ex E1 being Element of S st
( E1 = dom f & f is_measurable_on E1 ) & ex E2 being Element of S st
( E2 = dom g & g is_measurable_on E2 ) implies ex E being Element of S st
( E = dom (f + g) & f + g is_measurable_on E ) )
assume that
A1: ex E1 being Element of S st
( E1 = dom f & f is_measurable_on E1 ) and
A2: ex E2 being Element of S st
( E2 = dom g & g is_measurable_on E2 ) ; :: thesis: ex E being Element of S st
( E = dom (f + g) & f + g is_measurable_on E )
consider E1 being Element of S such that
A3: E1 = dom f and
A4: f is_measurable_on E1 by A1;
consider E2 being Element of S such that
A5: E2 = dom g and
A6: g is_measurable_on E2 by A2;
set E3 = E1 /\ E2;
set g1 = g | (E1 /\ E2);
A7: (g | (E1 /\ E2)) " {-infty} = (E1 /\ E2) /\ (g " {-infty}) by FUNCT_1:139;
set f1 = f | (E1 /\ E2);
dom (f | (E1 /\ E2)) = (dom f) /\ (E1 /\ E2) by RELAT_1:90;
then A8: dom (f | (E1 /\ E2)) = E1 /\ E2 by A3, XBOOLE_1:17, XBOOLE_1:28;
g is_measurable_on E1 /\ E2 by A6, MESFUNC1:34, XBOOLE_1:17;
then A9: g | (E1 /\ E2) is_measurable_on E1 /\ E2 by Lm6;
A10: (g | (E1 /\ E2)) " {+infty} = (E1 /\ E2) /\ (g " {+infty}) by FUNCT_1:139;
dom (g | (E1 /\ E2)) = (dom g) /\ (E1 /\ E2) by RELAT_1:90;
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:139;
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_measurable_on E1 /\ E2 by A4, MESFUNC1:34, XBOOLE_1:17;
then f | (E1 /\ E2) is_measurable_on E1 /\ E2 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_measurable_on E by A9, A8, A11, Lm7;
take E ; :: thesis: ( E = dom (f + g) & f + g is_measurable_on E )
A16: dom ((f + g) | E) = (dom (f + g)) /\ E by RELAT_1:90;
(f | (E1 /\ E2)) " {-infty} = (E1 /\ E2) /\ (f " {-infty}) by FUNCT_1:139;
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

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:90;
then A22: v in dom (f + g) by XBOOLE_0:def 4;
A23: ((f + g) | E) . v = (f + g) . v by A20, FUNCT_1:70
.= (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:70 ;
hence ((f + g) | E) . v = ((f | (E1 /\ E2)) + (g | (E1 /\ E2))) . v by A11, A24, A25, A23, FUNCT_1:70; :: thesis: verum

end;

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