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
and
A2:
0 <= r
and
A3:
for x being object st x in dom f holds
f . x = r
; integral' (M,f) = r * (M . (dom f))