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,ExtREAL

for E, A being Element of S st E = dom f & f is E -measurable & 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,ExtREAL

for E, A being Element of S st E = dom f & f is E -measurable & 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,ExtREAL

for E, A being Element of S st E = dom f & f is E -measurable & M . A = 0 holds

Integral (M,(f | (E \ A))) = Integral (M,f)

let f be PartFunc of X,ExtREAL; :: thesis: for E, A being Element of S st E = dom f & f is E -measurable & 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 E -measurable & M . A = 0 implies Integral (M,(f | (E \ A))) = Integral (M,f) )

assume that

A1: E = dom f and

A2: f is E -measurable and

A3: M . A = 0 ; :: thesis: Integral (M,(f | (E \ A))) = Integral (M,f)

set B = E \ A;

A4: dom f = dom (max+ f) by MESFUNC2:def 2;

A5: max- f is nonnegative by Lm1;

A6: max+ f is nonnegative by Lm1;

A7: dom f = dom (max- f) by MESFUNC2:def 3;

Integral (M,(f | (E \ A))) = (integral+ (M,((max+ f) | (E \ A)))) - (integral+ (M,(max- (f | (E \ A))))) by Th28

.= (integral+ (M,((max+ f) | (E \ A)))) - (integral+ (M,((max- f) | (E \ A)))) by Th28

.= (integral+ (M,(max+ f))) - (integral+ (M,((max- f) | (E \ A)))) by A1, A2, A3, A4, A6, Th84, MESFUNC2:25 ;

hence Integral (M,(f | (E \ A))) = Integral (M,f) by A1, A2, A3, A7, A5, Th84, MESFUNC2:26; :: thesis: verum

for M being sigma_Measure of S

for f being PartFunc of X,ExtREAL

for E, A being Element of S st E = dom f & f is E -measurable & 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,ExtREAL

for E, A being Element of S st E = dom f & f is E -measurable & 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,ExtREAL

for E, A being Element of S st E = dom f & f is E -measurable & M . A = 0 holds

Integral (M,(f | (E \ A))) = Integral (M,f)

let f be PartFunc of X,ExtREAL; :: thesis: for E, A being Element of S st E = dom f & f is E -measurable & 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 E -measurable & M . A = 0 implies Integral (M,(f | (E \ A))) = Integral (M,f) )

assume that

A1: E = dom f and

A2: f is E -measurable and

A3: M . A = 0 ; :: thesis: Integral (M,(f | (E \ A))) = Integral (M,f)

set B = E \ A;

A4: dom f = dom (max+ f) by MESFUNC2:def 2;

A5: max- f is nonnegative by Lm1;

A6: max+ f is nonnegative by Lm1;

A7: dom f = dom (max- f) by MESFUNC2:def 3;

Integral (M,(f | (E \ A))) = (integral+ (M,((max+ f) | (E \ A)))) - (integral+ (M,(max- (f | (E \ A))))) by Th28

.= (integral+ (M,((max+ f) | (E \ A)))) - (integral+ (M,((max- f) | (E \ A)))) by Th28

.= (integral+ (M,(max+ f))) - (integral+ (M,((max- f) | (E \ A)))) by A1, A2, A3, A4, A6, Th84, MESFUNC2:25 ;

hence Integral (M,(f | (E \ A))) = Integral (M,f) by A1, A2, A3, A7, A5, Th84, MESFUNC2:26; :: thesis: verum