let X be non empty set ; :: thesis: for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,COMPLEX
for E, A being Element of S st E = dom f & f is_integrable_on M & M . A = 0 holds
Integral M,(f | (E \ A)) = Integral M,f
let S be SigmaField of X; :: thesis: for M being sigma_Measure of S
for f being PartFunc of X,COMPLEX
for E, A being Element of S st E = dom f & f is_integrable_on M & M . A = 0 holds
Integral M,(f | (E \ A)) = Integral M,f
let M be sigma_Measure of S; :: thesis: for f being PartFunc of X,COMPLEX
for E, A being Element of S st E = dom f & f is_integrable_on M & M . A = 0 holds
Integral M,(f | (E \ A)) = Integral M,f
let f be PartFunc of X,COMPLEX ; :: thesis: for E, A being Element of S st E = dom f & f is_integrable_on M & M . A = 0 holds
Integral M,(f | (E \ A)) = Integral M,f
let E, A be Element of S; :: thesis: ( E = dom f & f is_integrable_on M & M . A = 0 implies Integral M,(f | (E \ A)) = Integral M,f )
assume that
A1: E = dom f and
A2: f is_integrable_on M and
A3: M . A = 0 ; :: thesis: Integral M,(f | (E \ A)) = Integral M,f
set C = E \ A;
A4: dom f = dom (Re f) by COMSEQ_3:def 3;
A5: Im f is_integrable_on M by A2, Def4;
then R_EAL (Im f) is_integrable_on M by MESFUNC6:def 9;
then consider IE being Element of S such that
A6: IE = dom (R_EAL (Im f)) and
A7: R_EAL (Im f) is_measurable_on IE by MESFUNC5:def 17;
A8: dom f = dom (Im f) by COMSEQ_3:def 4;
A9: Integral M,((Im f) | (E \ A)) = Integral M,(Im (f | (E \ A))) by Th7;
Im f is_measurable_on IE by A7, MESFUNC6:def 6;
then A10: Integral M,(Im (f | (E \ A))) = Integral M,(Im f) by A1, A3, A8, A6, A9, MESFUNC6:89;
(Im f) | (E \ A) is_integrable_on M by A5, MESFUNC6:91;
then A11: Im (f | (E \ A)) is_integrable_on M by Th7;
then A12: -infty < Integral M,(Im (f | (E \ A))) by MESFUNC6:90;
A13: Re f is_integrable_on M by A2, Def4;
then R_EAL (Re f) is_integrable_on M by MESFUNC6:def 9;
then consider RE being Element of S such that
A14: RE = dom (R_EAL (Re f)) and
A15: R_EAL (Re f) is_measurable_on RE by MESFUNC5:def 17;
A16: Integral M,((Re f) | (E \ A)) = Integral M,(Re (f | (E \ A))) by Th7;
Re f is_measurable_on RE by A15, MESFUNC6:def 6;
then A17: Integral M,(Re (f | (E \ A))) = Integral M,(Re f) by A1, A3, A4, A14, A16, MESFUNC6:89;
(Re f) | (E \ A) is_integrable_on M by A13, MESFUNC6:91;
then A18: Re (f | (E \ A)) is_integrable_on M by Th7;
then A19: Integral M,(Re (f | (E \ A))) < +infty by MESFUNC6:90;
A20: Integral M,(Im (f | (E \ A))) < +infty by A11, MESFUNC6:90;
-infty < Integral M,(Re (f | (E \ A))) by A18, MESFUNC6:90;
then reconsider R2 = Integral M,(Re (f | (E \ A))), I2 = Integral M,(Im (f | (E \ A))) as Real by A19, A12, A20, XXREAL_0:14;
f | (E \ A) is_integrable_on M by A18, A11, Def4;
hence Integral M,(f | (E \ A)) = R2 + (I2 * <i> ) by Def5
.= Integral M,f by A2, A17, A10, Def5 ;
:: thesis: verum