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 set st x in dom f holds
f . x = r ) holds
integral X,S,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 set st x in dom f holds
f . x = r ) holds
integral X,S,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 set st x in dom f holds
f . x = r ) holds
integral X,S,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 set st x in dom f holds
f . x = r ) holds
integral X,S,M,f = r * (M . (dom f))
let r be Real; :: thesis: ( dom f in S & 0 <= r & dom f <> {} & ( for x being set st x in dom f holds
f . x = r ) implies integral X,S,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 set st x in dom f holds
f . x = r ; :: thesis: integral X,S,M,f = r * (M . (dom f))
A5: f is_simple_func_in S by A1, A4, Lm5;
for x being set st x in dom f holds
0 <= f . x by A2, A4;
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 & dom v = dom F & ( for n being Nat st n in dom v holds
v . n = (a . n) * ((M * F) . n) ) & integral X,S,M,f = Sum v ) by A3, A5, MESFUNC4:4;
A7: ( dom f = union (rng F) & dom F = dom a & ( for n being Nat st n in dom F holds
for x being set st x in F . n holds
f . x = a . n ) ) by A6, MESFUNC3:def 1;
A8: dom v = dom (M * F) by A6, MESFUNC3:8;
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 A9: n in dom v ; :: thesis: v . n = r * ((M * F) . n)
then A10: F . n c= union (rng F) by A6, FUNCT_1:12, ZFMISC_1:92;
A11: v . n = (a . n) * ((M * F) . n) by A6, A9;

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 A12: (M * F) . n = 0 by A6, A9, FUNCT_1:23;
then v . n = 0 by A11;
hence v . n = r * ((M * F) . n) by A12; :: thesis: verum

end;

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

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

end;

end;

end;

then integral X,S,M,f = (R_EAL r) * (Sum (M * F)) by A6, A8, MESFUNC3:10
.= (R_EAL r) * (M . (union (rng F))) by MESFUNC3:9 ;
hence integral X,S,M,f = r * (M . (dom f)) by A6, MESFUNC3:def 1; :: thesis: verum