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

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