for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f, g being PartFunc of X,ExtREAL
for c being R_eal st f is_simple_func_in S & dom f <> {} & f is nonnegative & 0. <= c & c < +infty & dom g = dom f & ( for x being set st x in dom g holds
g . x = c * (f . x) ) holds
integral (M,g) = c * (integral (M,f))