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

dom (f + g) in S

let f, g be PartFunc of X,COMPLEX; :: 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: Re g is_integrable_on M by A2;

A4: Im g is_integrable_on M by A2;

Im f is_integrable_on M by A1;

then dom ((Im f) + (Im g)) in S by A4, MESFUNC6:99;

then A5: dom (Im (f + g)) in S by Th5;

Re f is_integrable_on M by A1;

then dom ((Re f) + (Re g)) in S by A3, MESFUNC6:99;

then A6: dom (Re (f + g)) in S by Th5;

dom (<i> (#) (Im (f + g))) = dom (Im (f + g)) by VALUED_1:def 5;

then dom ((Re (f + g)) + (<i> (#) (Im (f + g)))) = (dom (Re (f + g))) /\ (dom (Im (f + g))) by VALUED_1:def 1;

then dom ((Re (f + g)) + (<i> (#) (Im (f + g)))) in S by A6, A5, FINSUB_1:def 2;

hence dom (f + g) in S by Th8; :: thesis: verum

for M being sigma_Measure of S

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

dom (f + g) in S

let f, g be PartFunc of X,COMPLEX; :: 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: Re g is_integrable_on M by A2;

A4: Im g is_integrable_on M by A2;

Im f is_integrable_on M by A1;

then dom ((Im f) + (Im g)) in S by A4, MESFUNC6:99;

then A5: dom (Im (f + g)) in S by Th5;

Re f is_integrable_on M by A1;

then dom ((Re f) + (Re g)) in S by A3, MESFUNC6:99;

then A6: dom (Re (f + g)) in S by Th5;

dom (<i> (#) (Im (f + g))) = dom (Im (f + g)) by VALUED_1:def 5;

then dom ((Re (f + g)) + (<i> (#) (Im (f + g)))) = (dom (Re (f + g))) /\ (dom (Im (f + g))) by VALUED_1:def 1;

then dom ((Re (f + g)) + (<i> (#) (Im (f + g)))) in S by A6, A5, FINSUB_1:def 2;

hence dom (f + g) in S by Th8; :: thesis: verum