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 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))

per cases ( dom f = {} or dom f <> {} ) ;

suppose A4: dom f = {} ; :: thesis: integral' (M,f) = r * (M . (dom f))

then A5: M . (dom f) = 0 by VALUED_0:def 19;
integral' (M,f) = 0 by A4, Def14;
hence integral' (M,f) = r * (M . (dom f)) by A5; :: thesis: verum

end;

suppose A6: dom f <> {} ; :: thesis: integral' (M,f) = r * (M . (dom f))

then integral' (M,f) = integral (M,f) by Def14;
hence integral' (M,f) = r * (M . (dom f)) by A1, A2, A3, A6, Th103; :: thesis: verum

end;

end;