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 f is_integrable_on M & ( for x being object st x in (dom f) \ A holds
f . x = 0 ) 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 f is_integrable_on M & ( for x being object st x in (dom f) \ A holds
f . x = 0 ) 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 f is_integrable_on M & ( for x being object st x in (dom f) \ A holds
f . x = 0 ) holds
Integral (M,f) = Integral (M,(f | A))
let f be PartFunc of X,ExtREAL; :: thesis: for A being Element of S st f is_integrable_on M & ( for x being object st x in (dom f) \ A holds
f . x = 0 ) holds
Integral (M,f) = Integral (M,(f | A))
let A be Element of S; :: thesis: ( f is_integrable_on M & ( for x being object st x in (dom f) \ A holds
f . x = 0 ) implies Integral (M,f) = Integral (M,(f | A)) )
assume that
A1: f is_integrable_on M and
A2: for x being object st x in (dom f) \ A holds
f . x = 0 ; :: thesis: Integral (M,f) = Integral (M,(f | A))
consider E being Element of S such that
A3: ( E = dom f & f is E -measurable ) by A1, MESFUNC5:def 17;
reconsider B = E \ A as Element of S ;
A4: Integral (M,(f | (A \/ B))) = (Integral (M,(f | A))) + (Integral (M,(f | B))) by A1, MESFUNC5:98, XBOOLE_1:79;
A \/ B = (dom f) \/ A by A3, XBOOLE_1:39;
then A5: f | (A \/ B) = f by RELAT_1:68, XBOOLE_1:7;
A6: B c= dom f by A3, XBOOLE_1:36;
dom (f | B) = (dom f) /\ B by RELAT_1:61;
then A7: dom (f | B) = B by A3, 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 A9: x in dom (f | B) ; :: thesis: (f | B) . x = 0
then (f | B) . x = (f | B) /. x by PARTFUN1:def 6
.= f /. x by A9, PARTFUN1:80
.= f . x by A9, A7, A6, PARTFUN1:def 6 ;
hence (f | B) . x = 0 by A2, A9, A7, A3; :: thesis: verum
end;
then Integral (M,(f | B)) = 0 * (M . (dom (f | B))) by A7, Th27
.= 0 ;
hence Integral (M,f) = Integral (M,(f | A)) by A4, A5, XXREAL_3:4; :: thesis: verum