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 r being Real st dom f in S & 0 <= r & ( for x being object st x in dom f holds
f . x = r ) holds
Integral (M,f) = r * (M . (dom f))
let S be SigmaField of X; for M being sigma_Measure of S
for f being PartFunc of X,ExtREAL
for r being Real st dom f in S & 0 <= r & ( for x being object st x in dom f holds
f . x = r ) holds
Integral (M,f) = r * (M . (dom f))
let M be sigma_Measure of S; for f being PartFunc of X,ExtREAL
for r being Real st dom f in S & 0 <= r & ( for x being object st x in dom f holds
f . x = r ) holds
Integral (M,f) = r * (M . (dom f))
let f be PartFunc of X,ExtREAL; for r being Real st dom f in S & 0 <= r & ( for x being object st x in dom f holds
f . x = r ) holds
Integral (M,f) = r * (M . (dom f))
let r be Real; ( dom f in S & 0 <= r & ( for x being object st x in dom f holds
f . x = r ) implies Integral (M,f) = r * (M . (dom f)) )
assume that
A1:
( dom f in S & 0 <= r )
and
A2:
for x being object st x in dom f holds
f . x = r
; Integral (M,f) = r * (M . (dom f))
then
rng f c= REAL
;
then reconsider g = f as PartFunc of X,REAL by RELSET_1:6;
A4:
Integral (M,g) = r * (M . (dom g))
by A1, A2, MESFUNC6:97;
f = R_EAL g
by MESFUNC5:def 7;
hence
Integral (M,f) = r * (M . (dom f))
by A4, MESFUNC6:def 3; verum