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 ) & f " {+infty } in S & f " {-infty } in S & g " {+infty } in S & g " {-infty } in S holds
dom (f + g) in S
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 ) & f " {+infty } in S & f " {-infty } in S & g " {+infty } in S & g " {-infty } in S holds
dom (f + g) in S
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 ) & f " {+infty } in S & f " {-infty } in S & g " {+infty } in S & g " {-infty } in S holds
dom (f + g) in S
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 ) & f " {+infty } in S & f " {-infty } in S & g " {+infty } in S & g " {-infty } in S implies dom (f + g) in S )
assume A1: ( 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 ) & f " {+infty } in S & f " {-infty } in S & g " {+infty } in S & g " {-infty } in S ) ; :: thesis: dom (f + g) in S
then consider E1 being Element of S such that
A2: ( E1 = dom f & f is_measurable_on E1 ) ;
consider E2 being Element of S such that
A3: ( E2 = dom g & g is_measurable_on E2 ) by A1;
A4: dom (f + g) = (E1 /\ E2) \ (((f " {-infty }) /\ (g " {+infty })) \/ ((f " {+infty }) /\ (g " {-infty }))) by A2, A3, MESFUNC1:def 3;
( (f " {-infty }) /\ (g " {+infty }) in S & (f " {+infty }) /\ (g " {-infty }) in S ) by A1, MEASURE1:66;
then ((f " {-infty }) /\ (g " {+infty })) \/ ((f " {+infty }) /\ (g " {-infty })) in S by MEASURE1:66;
then A5: X \ (((f " {-infty }) /\ (g " {+infty })) \/ ((f " {+infty }) /\ (g " {-infty }))) in S by MEASURE1:66;
(E1 /\ E2) /\ (X \ (((f " {-infty }) /\ (g " {+infty })) \/ ((f " {+infty }) /\ (g " {-infty })))) = ((E1 /\ E2) /\ X) \ (((f " {-infty }) /\ (g " {+infty })) \/ ((f " {+infty }) /\ (g " {-infty }))) by XBOOLE_1:49
.= (E1 /\ E2) \ (((f " {-infty }) /\ (g " {+infty })) \/ ((f " {+infty }) /\ (g " {-infty }))) by XBOOLE_1:28 ;
hence dom (f + g) in S by A4, A5, MEASURE1:66; :: thesis: verum