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 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 ) and
A3: f " {+infty } in S and
A4: f " {-infty } in S and
A5: g " {+infty } in S and
A6: g " {-infty } in S ; :: thesis: dom (f + g) in S
A7: (f " {+infty }) /\ (g " {-infty }) in S by A3, A6, MEASURE1:66;
(f " {-infty }) /\ (g " {+infty }) in S by A4, A5, MEASURE1:66;
then ((f " {-infty }) /\ (g " {+infty })) \/ ((f " {+infty }) /\ (g " {-infty })) in S by A7, MEASURE1:66;
then A8: X \ (((f " {-infty }) /\ (g " {+infty })) \/ ((f " {+infty }) /\ (g " {-infty }))) in S by MEASURE1:66;
consider E2 being Element of S such that
A9: E2 = dom g and
g is_measurable_on E2 by A2;
consider E1 being Element of S such that
A10: E1 = dom f and
f is_measurable_on E1 by A1;
A11: (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 ;
dom (f + g) = (E1 /\ E2) \ (((f " {-infty }) /\ (g " {+infty })) \/ ((f " {+infty }) /\ (g " {-infty }))) by A10, A9, MESFUNC1:def 3;
hence dom (f + g) in S by A8, A11, MEASURE1:66; :: thesis: verum