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 f is_integrable_on M & g is_integrable_on M 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 f is_integrable_on M & g is_integrable_on M holds

dom (f + g) in S

let M be sigma_Measure of S; :: thesis: for f, g being PartFunc of X,ExtREAL st f is_integrable_on M & g is_integrable_on M holds

dom (f + g) in S

let f, g be PartFunc of X,ExtREAL; :: thesis: ( f is_integrable_on M & g is_integrable_on M implies dom (f + g) in S )

assume that

A1: f is_integrable_on M and

A2: g is_integrable_on M ; :: thesis: dom (f + g) in S

A3: f " {-infty} in S by A1, Th105;

A4: ex E2 being Element of S st

( E2 = dom g & g is E2 -measurable ) by A2;

A5: ex E1 being Element of S st

( E1 = dom f & f is E1 -measurable ) by A1;

A6: g " {-infty} in S by A2, Th105;

A7: g " {+infty} in S by A2, Th105;

f " {+infty} in S by A1, Th105;

hence dom (f + g) in S by A3, A7, A6, A5, A4, Th46; :: thesis: verum

for M being sigma_Measure of S

for f, g being PartFunc of X,ExtREAL st f is_integrable_on M & g is_integrable_on M 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 f is_integrable_on M & g is_integrable_on M holds

dom (f + g) in S

let M be sigma_Measure of S; :: thesis: for f, g being PartFunc of X,ExtREAL st f is_integrable_on M & g is_integrable_on M holds

dom (f + g) in S

let f, g be PartFunc of X,ExtREAL; :: thesis: ( f is_integrable_on M & g is_integrable_on M implies dom (f + g) in S )

assume that

A1: f is_integrable_on M and

A2: g is_integrable_on M ; :: thesis: dom (f + g) in S

A3: f " {-infty} in S by A1, Th105;

A4: ex E2 being Element of S st

( E2 = dom g & g is E2 -measurable ) by A2;

A5: ex E1 being Element of S st

( E1 = dom f & f is E1 -measurable ) by A1;

A6: g " {-infty} in S by A2, Th105;

A7: g " {+infty} in S by A2, Th105;

f " {+infty} in S by A1, Th105;

hence dom (f + g) in S by A3, A7, A6, A5, A4, Th46; :: thesis: verum