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

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