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 & f is_measurable_on E1 ) by A1;
consider E2 being Element of S such that
A4: ( E2 = dom g & g is_measurable_on E2 ) by A2;
set E3 = E1 /\ E2;
set f1 = f | (E1 /\ E2);
set g1 = g | (E1 /\ E2);
( f is_measurable_on E1 /\ E2 & g is_measurable_on E1 /\ E2 ) by A3, A4, MESFUNC1:34, XBOOLE_1:17;
then A5: ( f | (E1 /\ E2) is_measurable_on E1 /\ E2 & g | (E1 /\ E2) is_measurable_on E1 /\ E2 ) by Lm7;
( dom (f | (E1 /\ E2)) = (dom f) /\ (E1 /\ E2) & dom (g | (E1 /\ E2)) = (dom g) /\ (E1 /\ E2) ) by RELAT_1:90;
then A6: ( dom (f | (E1 /\ E2)) = E1 /\ E2 & dom (g | (E1 /\ E2)) = E1 /\ E2 ) by A3, A4, XBOOLE_1:17, XBOOLE_1:28;
then consider E being Element of S such that
A7: ( E = dom ((f | (E1 /\ E2)) + (g | (E1 /\ E2))) & (f | (E1 /\ E2)) + (g | (E1 /\ E2)) is_measurable_on E ) by A5, Lm8;
A8: 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;
A9: ( (f | (E1 /\ E2)) " {-infty } = (E1 /\ E2) /\ (f " {-infty }) & (f | (E1 /\ E2)) " {+infty } = (E1 /\ E2) /\ (f " {+infty }) & (g | (E1 /\ E2)) " {-infty } = (E1 /\ E2) /\ (g " {-infty }) & (g | (E1 /\ E2)) " {+infty } = (E1 /\ E2) /\ (g " {+infty }) ) by FUNCT_1:139;
then A10: ((f | (E1 /\ E2)) " {-infty }) /\ ((g | (E1 /\ E2)) " {+infty }) = (f " {-infty }) /\ ((E1 /\ E2) /\ ((E1 /\ E2) /\ (g " {+infty }))) by 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 ;
((f | (E1 /\ E2)) " {+infty }) /\ ((g | (E1 /\ E2)) " {-infty }) = (f " {+infty }) /\ ((E1 /\ E2) /\ ((E1 /\ E2) /\ (g " {-infty }))) by A9, 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 A11: (((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 A10, XBOOLE_1:23;
A12: dom (f + g) = ((dom f) /\ (dom g)) \ (((f " {-infty }) /\ (g " {+infty })) \/ ((f " {+infty }) /\ (g " {-infty }))) by MESFUNC1:def 3;
then A13: dom (f + g) = E by A3, A4, A6, A7, A8, A11, XBOOLE_1:47;
take E ; :: thesis: ( E = dom (f + g) & f + g is_measurable_on E )
A14: dom ((f + g) | E) = (dom (f + g)) /\ E by RELAT_1:90;

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 A15: v in dom ((f + g) | E) ; :: thesis: ((f + g) | E) . v = ((f | (E1 /\ E2)) + (g | (E1 /\ E2))) . v
then v in (dom (f + g)) /\ E by RELAT_1:90;
then A16: ( v in dom (f + g) & v in E ) by XBOOLE_0:def 4;
A17: E c= E1 /\ E2 by A6, A7, A8, XBOOLE_1:36;
A18: ((f + g) | E) . v = (f + g) . v by A15, FUNCT_1:70
.= (f . v) + (g . v) by A16, MESFUNC1:def 3 ;
((f | (E1 /\ E2)) + (g | (E1 /\ E2))) . v = ((f | (E1 /\ E2)) . v) + ((g | (E1 /\ E2)) . v) by A7, A13, A14, A15, MESFUNC1:def 3
.= (f . v) + ((g | (E1 /\ E2)) . v) by A6, A16, A17, FUNCT_1:70 ;
hence ((f + g) | E) . v = ((f | (E1 /\ E2)) + (g | (E1 /\ E2))) . v by A6, A16, A17, A18, FUNCT_1:70; :: thesis: verum

end;

then (f + g) | E = (f | (E1 /\ E2)) + (g | (E1 /\ E2)) by A7, A13, A14, PARTFUN1:34;
hence ( E = dom (f + g) & f + g is_measurable_on E ) by A3, A4, A6, A7, A8, A11, A12, Lm7, XBOOLE_1:47; :: thesis: verum