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 ( f is_integrable_on M & g is_integrable_on M ) ; :: thesis: dom (f + g) in S
then ( Re f is_integrable_on M & Im f is_integrable_on M & Re g is_integrable_on M & Im g is_integrable_on M ) by Def4;
then ( dom ((Re f) + (Re g)) in S & dom ((Im f) + (Im g)) in S ) by MESFUNC6:99;
then A1: ( dom (Re (f + g)) in S & dom (Im (f + g)) in S ) by COM19;
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 A1, MEASURE1:19;
hence dom (f + g) in S by COM99; :: thesis: verum