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_measurable_on E & 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_measurable_on E & 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_measurable_on E & 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_measurable_on E & 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_measurable_on E & M . A = 0 implies integral+ M,(f | (E \ A)) = integral+ M,f )
assume A1: ( f is nonnegative & E = dom f & f is_measurable_on E & M . A = 0 ) ; :: thesis: integral+ M,(f | (E \ A)) = integral+ M,f
set B = E \ A;
A2: integral+ M,(f | (A \/ (E \ A))) = (integral+ M,(f | A)) + (integral+ M,(f | (E \ A))) by A1, Th87, XBOOLE_1:79;
f | (A \/ (E \ A)) = f

proof

A \/ (E \ A) = A \/ E by XBOOLE_1:39;
then A3: dom f = (dom f) /\ (A \/ (E \ A)) by A1, XBOOLE_1:7, XBOOLE_1:28
.= dom (f | (A \/ (E \ A))) by RELAT_1:90 ;
for x being set st x in dom (f | (A \/ (E \ A))) holds
(f | (A \/ (E \ A))) . x = f . x by FUNCT_1:70;
hence f | (A \/ (E \ A)) = f by A3, FUNCT_1:9; :: thesis: verum

end;

then integral+ M,f = 0. + (integral+ M,(f | (E \ A))) by A1, A2, Th88;
hence integral+ M,(f | (E \ A)) = integral+ M,f by XXREAL_3:4; :: thesis: verum