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 & dom f <> {} & ( 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 & dom f <> {} & ( 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 & dom f <> {} & ( 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 & dom f <> {} & ( 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 & dom f <> {} & ( 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: dom f <> {} and
A4: for x being object st x in dom f holds
f . x = r ; :: thesis: integral (M,f) = r * (M . (dom f))
for x being object st x in dom f holds
0 <= f . x by A2, A4;
then a5: f is nonnegative by SUPINF_2:52;
f is_simple_func_in S by A1, A4, Lm4;
then consider F being Finite_Sep_Sequence of S, a, v being FinSequence of ExtREAL such that
A6: F,a are_Re-presentation_of f and
A7: dom v = dom F and
A8: for n being Nat st n in dom v holds
v . n = (a . n) * ((M * F) . n) and
A9: integral (M,f) = Sum v by A3, a5, MESFUNC4:4;
A10: dom f = union (rng F) by A6, MESFUNC3:def 1;
A11: for n being Nat st n in dom v holds
v . n = r * ((M * F) . n)

proof

let n be Nat; :: thesis: ( n in dom v implies v . n = r * ((M * F) . n) )
assume A12: n in dom v ; :: thesis: v . n = r * ((M * F) . n)
then A13: F . n c= union (rng F) by A7, FUNCT_1:3, ZFMISC_1:74;
A14: v . n = (a . n) * ((M * F) . n) by A8, A12;

per cases ( F . n = {} or F . n <> {} ) ;

suppose F . n = {} ; :: thesis: v . n = r * ((M * F) . n)

then M . (F . n) = 0 by VALUED_0:def 19;
then A15: (M * F) . n = 0 by A7, A12, FUNCT_1:13;
then v . n = 0 by A14;
hence v . n = r * ((M * F) . n) by A15; :: thesis: verum

end;

suppose F . n <> {} ; :: thesis: v . n = r * ((M * F) . n)

then consider x being object such that
A16: x in F . n by XBOOLE_0:def 1;
a . n = f . x by A6, A7, A12, A16, MESFUNC3:def 1;
hence v . n = r * ((M * F) . n) by A4, A10, A13, A14, A16; :: thesis: verum

end;

end;

end;

reconsider rr = r as R_eal by XXREAL_0:def 1;
dom v = dom (M * F) by A7, MESFUNC3:8;
then integral (M,f) = rr * (Sum (M * F)) by A9, A11, MESFUNC3:10
.= rr * (M . (union (rng F))) by MESFUNC3:9 ;
hence integral (M,f) = r * (M . (dom f)) by A6, MESFUNC3:def 1; :: thesis: verum