theorem Th86: :: MESFUNC5:86

for X being non empty set
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 0 <= c & ex A being Element of S st
( A = dom f & f is A -measurable ) & f is nonnegative holds
integral+ (M,(c (#) f)) = c * (integral+ (M,f))