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 ) & 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 E1 -measurable ) & ex E2 being Element of S st
( E2 = dom g & g is E2 -measurable ) & 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 E1 -measurable ) & ex E2 being Element of S st
( E2 = dom g & g is E2 -measurable ) & 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 E1 -measurable ) & ex E2 being Element of S st
( E2 = dom g & g is E2 -measurable ) & 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 E1 -measurable ) and
A2: ex E2 being Element of S st
( E2 = dom g & g is E2 -measurable ) 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:34;
(f " {-infty}) /\ (g " {+infty}) in S by A4, A5, MEASURE1:34;
then ((f " {-infty}) /\ (g " {+infty})) \/ ((f " {+infty}) /\ (g " {-infty})) in S by A7, MEASURE1:34;
then A8: X \ (((f " {-infty}) /\ (g " {+infty})) \/ ((f " {+infty}) /\ (g " {-infty}))) in S by MEASURE1:34;
consider E2 being Element of S such that
A9: E2 = dom g and
g is E2 -measurable by A2;
consider E1 being Element of S such that
A10: E1 = dom f and
f is E1 -measurable 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:34; :: thesis: verum