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 that
A1: f is_integrable_on M and
A2: 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)) )
A3: Re g is_integrable_on M by A2, Def4;
Re f is_integrable_on M by A1, Def4;
then consider E being Element of S such that
A4: E = (dom (Re f)) /\ (dom (Re g)) and
A5: Integral M,((Re f) + (Re g)) = (Integral M,((Re f) | E)) + (Integral M,((Re g) | E)) by A3, MESFUNC6:101;
A6: f | E is_integrable_on M by A1, Th23;
then A7: Re (f | E) is_integrable_on M by Def4;
then A8: Integral M,(Re (f | E)) < +infty by MESFUNC6:90;
A9: Im (f | E) is_integrable_on M by A6, Def4;
then A10: -infty < Integral M,(Im (f | E)) by MESFUNC6:90;
A11: Integral M,(Im (f | E)) < +infty by A9, MESFUNC6:90;
-infty < Integral M,(Re (f | E)) by A7, MESFUNC6:90;
then reconsider R1 = Integral M,(Re (f | E)), I1 = Integral M,(Im (f | E)) as Real by A8, A10, A11, XXREAL_0:14;
A12: dom f = dom (Re f) by COMSEQ_3:def 3;
A13: Im g is_integrable_on M by A2, Def4;
Im f is_integrable_on M by A1, Def4;
then A14: 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 A13, MESFUNC6:101;
A15: Integral M,((Im f) + (Im g)) = Integral M,(Im (f + g)) by Th5;
A16: f + g is_integrable_on M by A1, A2, Th33;
then A17: Re (f + g) is_integrable_on M by Def4;
then A18: Integral M,(Re (f + g)) < +infty by MESFUNC6:90;
A19: Im (f + g) is_integrable_on M by A16, Def4;
then A20: -infty < Integral M,(Im (f + g)) by MESFUNC6:90;
A21: Integral M,(Im (f + g)) < +infty by A19, MESFUNC6:90;
-infty < Integral M,(Re (f + g)) by A17, MESFUNC6:90;
then reconsider R = Integral M,(Re (f + g)), I = Integral M,(Im (f + g)) as Real by A18, A20, A21, XXREAL_0:14;
A22: Integral M,(f + g) = R + (I * <i> ) by A16, Def5;
A23: dom g = dom (Im g) by COMSEQ_3:def 4;
A24: g | E is_integrable_on M by A2, Th23;
then A25: Re (g | E) is_integrable_on M by Def4;
then A26: Integral M,(Re (g | E)) < +infty by MESFUNC6:90;
A27: Im (g | E) is_integrable_on M by A24, Def4;
then A28: -infty < Integral M,(Im (g | E)) by MESFUNC6:90;
A29: Integral M,(Im (g | E)) < +infty by A27, MESFUNC6:90;
-infty < Integral M,(Re (g | E)) by A25, MESFUNC6:90;
then reconsider R2 = Integral M,(Re (g | E)), I2 = Integral M,(Im (g | E)) as Real by A26, A28, A29, XXREAL_0:14;
A30: dom g = dom (Re g) by COMSEQ_3:def 3;
Integral M,((Re f) + (Re g)) = Integral M,(Re (f + g)) by Th5;
then Integral M,(Re (f + g)) = (Integral M,(Re (f | E))) + (Integral M,((Re g) | E)) by A5, Th7
.= (Integral M,(Re (f | E))) + (Integral M,(Re (g | E))) by Th7 ;
then A31: R = R1 + R2 by SUPINF_2:1;
dom f = dom (Im f) by COMSEQ_3:def 4;
then Integral M,(Im (f + g)) = (Integral M,(Im (f | E))) + (Integral M,((Im g) | E)) by A4, A12, A30, A23, A14, A15, Th7;
then R_EAL I = (R_EAL I1) + (R_EAL I2) by Th7;
then I = I1 + I2 by SUPINF_2:1;
then Integral M,(f + g) = (R1 + (I1 * <i> )) + (R2 + (I2 * <i> )) by A31, A22;
then Integral M,(f + g) = (Integral M,(f | E)) + (R2 + (I2 * <i> )) by A6, Def5;
then Integral M,(f + g) = (Integral M,(f | E)) + (Integral M,(g | E)) by A24, 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 A4, A12, A30; :: thesis: verum