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 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,REAL
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,REAL
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,REAL; :: 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 and
A2: 0 <= r and
A3: for x being object st x in dom f holds
f . x = r ; :: thesis: Integral (M,f) = r * (M . (dom f))
A4: for x being object st x in dom (R_EAL f) holds
0. <= (R_EAL f) . x by A2, A3;
reconsider A = dom (R_EAL f) as Element of S by A1;
A5: R_EAL f is A -measurable by A3, Th2, MESFUNC2:34;
( r * (M . (dom (R_EAL f))) = integral' (M,(R_EAL f)) & R_EAL f is_simple_func_in S ) by A1, A2, A3, Th2, MESFUNC5:104;
then integral+ (M,(R_EAL f)) = r * (M . (dom (R_EAL f))) by A4, MESFUNC5:77, SUPINF_2:52;
hence Integral (M,f) = r * (M . (dom f)) by A4, A5, MESFUNC5:88, SUPINF_2:52; :: thesis: verum