theorem :: MESFUN12:24

for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for E being Element of S
for f being PartFunc of X,ExtREAL
for r being Real st E = dom f & ( f is nonpositive or f is nonnegative ) & f is E -measurable holds
Integral (M,(r (#) f)) = r * (Integral (M,f)) by Lm1, Lm2;