let X be non empty set ; 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; 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; 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; ( 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
; 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; verum