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 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; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: Integral (M,f) = r * (M . (dom f))

now :: thesis: for y being object st y in rng f holds
y in REAL

let y be object ; :: thesis: ( y in rng f implies y in REAL )
assume y in rng f ; :: thesis: y in REAL
then consider x being object such that
A3: ( x in dom f & y = f . x ) by FUNCT_1:def 3;
y = r by A2, A3;
hence y in REAL by XREAL_0:def 1; :: thesis: verum

end;

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; :: thesis: verum