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
ex E being Element of S st
( E = (dom f) /\ (dom g) & Integral M,(f + g) = (Integral M,(f | E)) + (Integral M,(g | E)) )
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
ex E being Element of S st
( E = (dom f) /\ (dom g) & Integral M,(f + g) = (Integral M,(f | E)) + (Integral M,(g | E)) )
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
ex E being Element of S st
( E = (dom f) /\ (dom g) & Integral M,(f + g) = (Integral M,(f | E)) + (Integral M,(g | E)) )
let f, g be PartFunc of X,COMPLEX ; :: thesis: ( f is_integrable_on M & g is_integrable_on M implies ex E being Element of S st
( E = (dom f) /\ (dom g) & Integral M,(f + g) = (Integral M,(f | E)) + (Integral M,(g | E)) ) )
assume A1: ( f is_integrable_on M & g is_integrable_on M ) ; :: thesis: ex E being Element of S st
( E = (dom f) /\ (dom g) & Integral M,(f + g) = (Integral M,(f | E)) + (Integral M,(g | E)) )
then A2: ( 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 consider E being Element of S such that
A3: ( E = (dom (Re f)) /\ (dom (Re g)) & Integral M,((Re f) + (Re g)) = (Integral M,((Re f) | E)) + (Integral M,((Re g) | E)) ) by MESFUNC6:101;
D1: ( dom f = dom (Re f) & dom g = dom (Re g) & dom f = dom (Im f) & dom g = dom (Im g) ) by Def1, Def2;
A3I: ex Ei being Element of S st
( Ei = (dom (Im f)) /\ (dom (Im g)) & Integral M,((Im f) + (Im g)) = (Integral M,((Im f) | Ei)) + (Integral M,((Im g) | Ei)) ) by A2, MESFUNC6:101;
A4: f + g is_integrable_on M by A1, Th100;
then ( Re (f + g) is_integrable_on M & Im (f + g) is_integrable_on M ) by Def4;
then ( -infty < Integral M,(Re (f + g)) & Integral M,(Re (f + g)) < +infty & -infty < Integral M,(Im (f + g)) & Integral M,(Im (f + g)) < +infty ) by MESFUNC6:90;
then reconsider R = Integral M,(Re (f + g)), I = Integral M,(Im (f + g)) as Real by XXREAL_0:14;
A5: ( f | E is_integrable_on M & g | E is_integrable_on M ) by A1, Th91;
then ( Re (f | E) is_integrable_on M & Im (f | E) is_integrable_on M ) by Def4;
then ( -infty < Integral M,(Re (f | E)) & Integral M,(Re (f | E)) < +infty & -infty < Integral M,(Im (f | E)) & Integral M,(Im (f | E)) < +infty ) by MESFUNC6:90;
then reconsider R1 = Integral M,(Re (f | E)), I1 = Integral M,(Im (f | E)) as Real by XXREAL_0:14;
( Re (g | E) is_integrable_on M & Im (g | E) is_integrable_on M ) by A5, Def4;
then ( -infty < Integral M,(Re (g | E)) & Integral M,(Re (g | E)) < +infty & -infty < Integral M,(Im (g | E)) & Integral M,(Im (g | E)) < +infty ) by MESFUNC6:90;
then reconsider R2 = Integral M,(Re (g | E)), I2 = Integral M,(Im (g | E)) as Real by XXREAL_0:14;
Integral M,((Re f) + (Re g)) = Integral M,(Re (f + g)) by COM19;
then B1: Integral M,(Re (f + g)) = (Integral M,(Re (f | E))) + (Integral M,((Re g) | E)) by A3, COM91
.= (Integral M,(Re (f | E))) + (Integral M,(Re (g | E))) by COM91 ;
Integral M,((Im f) + (Im g)) = Integral M,(Im (f + g)) by COM19;
then Integral M,(Im (f + g)) = (Integral M,(Im (f | E))) + (Integral M,((Im g) | E)) by A3I, A3, D1, COM91;
then ( R_EAL R = (R_EAL R1) + (R_EAL R2) & R_EAL I = (R_EAL I1) + (R_EAL I2) ) by B1, COM91;
then C3: ( R = R1 + R2 & I = I1 + I2 ) by SUPINF_2:1;
Integral M,(f + g) = R + (I * <i> ) by A4, Def5;
then Integral M,(f + g) = (R1 + (I1 * <i> )) + (R2 + (I2 * <i> )) by C3;
then Integral M,(f + g) = (Integral M,(f | E)) + (R2 + (I2 * <i> )) by A5, Def5;
then Integral M,(f + g) = (Integral M,(f | E)) + (Integral M,(g | E)) by A5, Def5;
hence ex E being Element of S st
( E = (dom f) /\ (dom g) & Integral M,(f + g) = (Integral M,(f | E)) + (Integral M,(g | E)) ) by D1, A3; :: thesis: verum