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 f is nonnegative & 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 f is nonnegative & 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 f is nonnegative & 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 f is nonnegative & 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: ( f is nonnegative & E = dom f & f is E -measurable & M . A = 0 implies integral+ (M,(f | (E \ A))) = integral+ (M,f) )

assume that

A1: f is nonnegative and

A2: E = dom f and

A3: f is E -measurable and

A4: M . A = 0 ; :: thesis: integral+ (M,(f | (E \ A))) = integral+ (M,f)

set B = E \ A;

A \/ (E \ A) = A \/ E by XBOOLE_1:39;

then A5: dom f = (dom f) /\ (A \/ (E \ A)) by A2, XBOOLE_1:7, XBOOLE_1:28

.= dom (f | (A \/ (E \ A))) by RELAT_1:61 ;

for x being object st x in dom (f | (A \/ (E \ A))) holds

(f | (A \/ (E \ A))) . x = f . x by FUNCT_1:47;

then A6: f | (A \/ (E \ A)) = f by A5, FUNCT_1:2;

integral+ (M,(f | (A \/ (E \ A)))) = (integral+ (M,(f | A))) + (integral+ (M,(f | (E \ A)))) by A1, A2, A3, Th81, XBOOLE_1:79;

then integral+ (M,f) = 0. + (integral+ (M,(f | (E \ A)))) by A1, A2, A3, A4, A6, Th82;

hence integral+ (M,(f | (E \ A))) = integral+ (M,f) by XXREAL_3:4; :: thesis: verum

for M being sigma_Measure of S

for f being PartFunc of X,ExtREAL

for E, A being Element of S st f is nonnegative & 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 f is nonnegative & 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 f is nonnegative & 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 f is nonnegative & 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: ( f is nonnegative & E = dom f & f is E -measurable & M . A = 0 implies integral+ (M,(f | (E \ A))) = integral+ (M,f) )

assume that

A1: f is nonnegative and

A2: E = dom f and

A3: f is E -measurable and

A4: M . A = 0 ; :: thesis: integral+ (M,(f | (E \ A))) = integral+ (M,f)

set B = E \ A;

A \/ (E \ A) = A \/ E by XBOOLE_1:39;

then A5: dom f = (dom f) /\ (A \/ (E \ A)) by A2, XBOOLE_1:7, XBOOLE_1:28

.= dom (f | (A \/ (E \ A))) by RELAT_1:61 ;

for x being object st x in dom (f | (A \/ (E \ A))) holds

(f | (A \/ (E \ A))) . x = f . x by FUNCT_1:47;

then A6: f | (A \/ (E \ A)) = f by A5, FUNCT_1:2;

integral+ (M,(f | (A \/ (E \ A)))) = (integral+ (M,(f | A))) + (integral+ (M,(f | (E \ A)))) by A1, A2, A3, Th81, XBOOLE_1:79;

then integral+ (M,f) = 0. + (integral+ (M,(f | (E \ A)))) by A1, A2, A3, A4, A6, Th82;

hence integral+ (M,(f | (E \ A))) = integral+ (M,f) by XXREAL_3:4; :: thesis: verum