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,REAL
for r being Real st dom f in S & 0 <= r & ( for x being set st x in dom f holds
f . x = r ) holds
Integral M,f = (R_EAL r) * (M . (dom f))
let S be SigmaField of X; :: thesis: for M being sigma_Measure of S
for f being PartFunc of X,REAL
for r being Real st dom f in S & 0 <= r & ( for x being set st x in dom f holds
f . x = r ) holds
Integral M,f = (R_EAL r) * (M . (dom f))
let M be sigma_Measure of S; :: thesis: for f being PartFunc of X,REAL
for r being Real st dom f in S & 0 <= r & ( for x being set st x in dom f holds
f . x = r ) holds
Integral M,f = (R_EAL r) * (M . (dom f))
let f be PartFunc of X,REAL ; :: thesis: for r being Real st dom f in S & 0 <= r & ( for x being set st x in dom f holds
f . x = r ) holds
Integral M,f = (R_EAL r) * (M . (dom f))
let r be Real; :: thesis: ( dom f in S & 0 <= r & ( for x being set st x in dom f holds
f . x = r ) implies Integral M,f = (R_EAL r) * (M . (dom f)) )
assume A1: ( dom f in S & 0 <= r & ( for x being set st x in dom f holds
f . x = r ) ) ; :: thesis: Integral M,f = (R_EAL r) * (M . (dom f))
then reconsider A = dom (R_EAL f) as Element of S ;
A2: (R_EAL r) * (M . (dom (R_EAL f))) = integral' M,(R_EAL f) by A1, MESFUNC5:110;
A3: ( R_EAL f is_simple_func_in S & R_EAL f is nonnegative )

proof

thus R_EAL f is_simple_func_in S by A1, Th2; :: thesis: R_EAL f is nonnegative
for x being set st x in dom (R_EAL f) holds
0. <= (R_EAL f) . x by A1;
hence R_EAL f is nonnegative by SUPINF_2:71; :: thesis: verum

end;

then A4: R_EAL f is_measurable_on A by MESFUNC2:37;
integral+ M,(R_EAL f) = (R_EAL r) * (M . (dom (R_EAL f))) by A2, A3, MESFUNC5:83;
hence Integral M,f = (R_EAL r) * (M . (dom f)) by A3, A4, MESFUNC5:94; :: thesis: verum