let X be non empty set ; 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; 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; 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; 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; ( 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
; 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;
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; verum