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

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