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;
then R_EAL (Im f) is_integrable_on M ;
then consider IE being Element of S such that
A6: IE = dom (R_EAL (Im f)) and
A7: R_EAL (Im f) is IE -measurable ;
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 IE -measurable by A7;
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;
then R_EAL (Re f) is_integrable_on M ;
then consider RE being Element of S such that
A14: RE = dom (R_EAL (Re f)) and
A15: R_EAL (Re f) is RE -measurable ;
A16: Integral (M,((Re f) | (E \ A))) = Integral (M,(Re (f | (E \ A)))) by Th7;
Re f is RE -measurable by A15;
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 Element of REAL by A19, A12, A20, XXREAL_0:14;
f | (E \ A) is_integrable_on M by A18, A11;
hence Integral (M,(f | (E \ A))) = R2 + (I2 * <i>) by Def3
.= Integral (M,f) by A2, A17, A10, Def3 ;
:: thesis: verum