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;
Re f is_integrable_on M by A1;
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 ;
then A8: Integral (M,(Re (f | E))) < +infty by MESFUNC6:90;
A9: Im (f | E) is_integrable_on M by A6;
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 Element of 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;
Im f is_integrable_on M by A1;
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 ;
then A18: Integral (M,(Re (f + g))) < +infty by MESFUNC6:90;
A19: Im (f + g) is_integrable_on M by A16;
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 Element of REAL by A18, A20, A21, XXREAL_0:14;
A22: Integral (M,(f + g)) = R + (I * <i>) by A16, Def3;
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 ;
then A26: Integral (M,(Re (g | E))) < +infty by MESFUNC6:90;
A27: Im (g | E) is_integrable_on M by A24;
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 Element of 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 I = I1 + I2 by Th7;
then I = I1 + I2 ;
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, Def3;
then Integral (M,(f + g)) = (Integral (M,(f | E))) + (Integral (M,(g | E))) by A24, Def3;
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