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 A being Element of S st ex E being Element of S st
( E = dom f & f is E -measurable ) & ( for x being object st x in (dom f) \ A holds
f . x = 0 ) & f is nonnegative holds
Integral (M,f) = Integral (M,(f | A))
let S be SigmaField of X; :: thesis: for M being sigma_Measure of S
for f being PartFunc of X,ExtREAL
for A being Element of S st ex E being Element of S st
( E = dom f & f is E -measurable ) & ( for x being object st x in (dom f) \ A holds
f . x = 0 ) & f is nonnegative holds
Integral (M,f) = Integral (M,(f | A))
let M be sigma_Measure of S; :: thesis: for f being PartFunc of X,ExtREAL
for A being Element of S st ex E being Element of S st
( E = dom f & f is E -measurable ) & ( for x being object st x in (dom f) \ A holds
f . x = 0 ) & f is nonnegative holds
Integral (M,f) = Integral (M,(f | A))
let f be PartFunc of X,ExtREAL; :: thesis: for A being Element of S st ex E being Element of S st
( E = dom f & f is E -measurable ) & ( for x being object st x in (dom f) \ A holds
f . x = 0 ) & f is nonnegative holds
Integral (M,f) = Integral (M,(f | A))
let A be Element of S; :: thesis: ( ex E being Element of S st
( E = dom f & f is E -measurable ) & ( for x being object st x in (dom f) \ A holds
f . x = 0 ) & f is nonnegative implies Integral (M,f) = Integral (M,(f | A)) )
assume that
A1: ex E being Element of S st
( E = dom f & f is E -measurable ) and
A2: for x being object st x in (dom f) \ A holds
f . x = 0 and
A3: f is nonnegative ; :: thesis: Integral (M,f) = Integral (M,(f | A))
consider E being Element of S such that
A4: ( E = dom f & f is E -measurable ) by A1;
reconsider B = E \ A as Element of S ;
A6: Integral (M,(f | (A \/ B))) = (Integral (M,(f | A))) + (Integral (M,(f | B))) by A1, A3, MESFUNC5:91, XBOOLE_1:79;
A \/ B = (dom f) \/ A by A4, XBOOLE_1:39;
then A7: f | (A \/ B) = f by RELAT_1:68, XBOOLE_1:7;
A8: B c= dom f by A4, XBOOLE_1:36;
dom (f | B) = (dom f) /\ B by RELAT_1:61;
then A9: dom (f | B) = B by A4, XBOOLE_1:28, XBOOLE_1:36;

now :: thesis: for x being object st x in dom (f | B) holds
(f | B) . x = 0

let x be object ; :: thesis: ( x in dom (f | B) implies (f | B) . x = 0 )
assume A10: x in dom (f | B) ; :: thesis: (f | B) . x = 0
then (f | B) . x = (f | B) /. x by PARTFUN1:def 6
.= f /. x by A10, PARTFUN1:80
.= f . x by A10, A8, A9, PARTFUN1:def 6 ;
hence (f | B) . x = 0 by A2, A10, A9, A4; :: thesis: verum

end;

then Integral (M,(f | B)) = 0 * (M . (dom (f | B))) by A9, Th27
.= 0 ;
hence Integral (M,f) = Integral (M,(f | A)) by A6, A7, XXREAL_3:4; :: thesis: verum