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:
A4: for x being set st x in dom f holds
0 <= f . x by A2, SUPINF_2:51;
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 = (R_EAL c) * (f . x) by MESFUNC1:def 6;

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

then integral' (M,f) = 0 by A5, Def14;
then c * (integral' (M,f)) = 0 ;
hence integral' (M,(c (#) f)) = (R_EAL c) * (integral' (M,f)) by A7, Def14; :: thesis:

end;

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

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

end;

end;