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, Th111;
A4: ex E2 being Element of S st
( E2 = dom g & g is_measurable_on E2 ) by A2, Def17;
A5: ex E1 being Element of S st
( E1 = dom f & f is_measurable_on E1 ) by A1, Def17;
A6: g " {-infty } in S by A2, Th111;
A7: g " {+infty } in S by A2, Th111;
f " {+infty } in S by A1, Th111;
hence dom (f + g) in S by A3, A7, A6, A5, A4, Th52; :: thesis: verum