let X be non empty set ; :: thesis:
let S be SigmaField of X; :: thesis:
let M be sigma_Measure of S; :: thesis:
let f be PartFunc of X, ExtREAL ; :: thesis:
let c be Real; :: thesis:
assume that
A1: f is_simple_func_in S and
A2: f is nonnegative and
A3: 0 <= c ; :: thesis:
set g = c (#) f;
A4: dom (c (#) f) = dom f by MESFUNC1:def 6;
A5: for x being set st x in dom f holds
0 <= f . x by A2, SUPINF_2:70;
A6: for x being set st x in dom (c (#) f) holds
(c (#) f) . x = (R_EAL c) * (f . x) by MESFUNC1:def 6;
A7: ( 0 <= R_EAL c & R_EAL c < +infty ) by A3, XXREAL_0:9;

per cases ;

suppose A8: dom (c (#) f) = {} ; :: thesis:

then integral' M,f = 0 by A4, Def14;
then (R_EAL c) * (integral' M,f) = 0 by EXTREAL1:22;
hence integral' M,(c (#) f) = (R_EAL c) * (integral' M,f) by A8, Def14; :: thesis:

end;

suppose A9: dom (c (#) f) <> {} ; :: thesis:

then integral' M,f = integral X,S,M,f by A4, Def14;
then integral X,S,M,(c (#) f) = (R_EAL c) * (integral' M,f) by A1, A4, A5, A6, A7, A9, MESFUNC4:6;
hence integral' M,(c (#) f) = (R_EAL c) * (integral' M,f) by A9, Def14; :: thesis:

end;