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;

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

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;

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;

end;