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)

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

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

reconsider rr = r as R_eal by XXREAL_0:def 1;
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;

end;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;

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