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 c being Real st f is_simple_func_in S & f is nonnegative & 0 <= c holds

integral' (M,(c (#) f)) = c * (integral' (M,f))

let S be SigmaField of X; :: thesis: for M being sigma_Measure of S

for f being PartFunc of X,ExtREAL

for c being Real st f is_simple_func_in S & f is nonnegative & 0 <= c holds

integral' (M,(c (#) f)) = c * (integral' (M,f))

let M be sigma_Measure of S; :: thesis: for f being PartFunc of X,ExtREAL

for c being Real st f is_simple_func_in S & f is nonnegative & 0 <= c holds

integral' (M,(c (#) f)) = c * (integral' (M,f))

let f be PartFunc of X,ExtREAL; :: thesis: for c being Real st f is_simple_func_in S & f is nonnegative & 0 <= c holds

integral' (M,(c (#) f)) = c * (integral' (M,f))

let c be Real; :: thesis: ( f is_simple_func_in S & f is nonnegative & 0 <= c implies integral' (M,(c (#) f)) = c * (integral' (M,f)) )

assume that

A1: f is_simple_func_in S and

A2: f is nonnegative and

A3: 0 <= c ; :: thesis: integral' (M,(c (#) f)) = c * (integral' (M,f))

set g = c (#) f;

A5: dom (c (#) f) = dom f by MESFUNC1:def 6;

A6: for x being set st x in dom (c (#) f) holds

(c (#) f) . x = c * (f . x) by MESFUNC1:def 6;

for M being sigma_Measure of S

for f being PartFunc of X,ExtREAL

for c being Real st f is_simple_func_in S & f is nonnegative & 0 <= c holds

integral' (M,(c (#) f)) = c * (integral' (M,f))

let S be SigmaField of X; :: thesis: for M being sigma_Measure of S

for f being PartFunc of X,ExtREAL

for c being Real st f is_simple_func_in S & f is nonnegative & 0 <= c holds

integral' (M,(c (#) f)) = c * (integral' (M,f))

let M be sigma_Measure of S; :: thesis: for f being PartFunc of X,ExtREAL

for c being Real st f is_simple_func_in S & f is nonnegative & 0 <= c holds

integral' (M,(c (#) f)) = c * (integral' (M,f))

let f be PartFunc of X,ExtREAL; :: thesis: for c being Real st f is_simple_func_in S & f is nonnegative & 0 <= c holds

integral' (M,(c (#) f)) = c * (integral' (M,f))

let c be Real; :: thesis: ( f is_simple_func_in S & f is nonnegative & 0 <= c implies integral' (M,(c (#) f)) = c * (integral' (M,f)) )

assume that

A1: f is_simple_func_in S and

A2: f is nonnegative and

A3: 0 <= c ; :: thesis: integral' (M,(c (#) f)) = c * (integral' (M,f))

set g = c (#) f;

A5: dom (c (#) f) = dom f by MESFUNC1:def 6;

A6: for x being set st x in dom (c (#) f) holds

(c (#) f) . x = c * (f . x) by MESFUNC1:def 6;

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

end;

suppose A7:
dom (c (#) f) = {}
; :: thesis: integral' (M,(c (#) f)) = c * (integral' (M,f))

then
integral' (M,f) = 0
by A5, Def14;

then c * (integral' (M,f)) = 0 ;

hence integral' (M,(c (#) f)) = c * (integral' (M,f)) by A7, Def14; :: thesis: verum

end;then c * (integral' (M,f)) = 0 ;

hence integral' (M,(c (#) f)) = c * (integral' (M,f)) by A7, Def14; :: thesis: verum

suppose A8:
dom (c (#) f) <> {}
; :: thesis: integral' (M,(c (#) f)) = c * (integral' (M,f))

then A9:
integral' (M,f) = integral (M,f)
by A5, Def14;

reconsider cc = c as R_eal by XXREAL_0:def 1;

c in REAL by XREAL_0:def 1;

then c < +infty by XXREAL_0:9;

then integral (M,(c (#) f)) = cc * (integral' (M,f)) by A1, A3, A5, A2, A6, A8, MESFUNC4:6, A9;

hence integral' (M,(c (#) f)) = c * (integral' (M,f)) by A8, Def14; :: thesis: verum

end;reconsider cc = c as R_eal by XXREAL_0:def 1;

c in REAL by XREAL_0:def 1;

then c < +infty by XXREAL_0:9;

then integral (M,(c (#) f)) = cc * (integral' (M,f)) by A1, A3, A5, A2, A6, A8, MESFUNC4:6, A9;

hence integral' (M,(c (#) f)) = c * (integral' (M,f)) by A8, Def14; :: thesis: verum