theorem :: MESFUNC7:17

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 E being Element of S
for F being non empty Subset of ExtREAL st (dom f) /\ (dom g) = E & rng f = F & g is real-valued & f is E -measurable & rng f is real-bounded & g is_integrable_on M holds
( (f (#) g) | E is_integrable_on M & ex c being Element of REAL st
( c >= inf F & c <= sup F & Integral (M,((f (#) |.g.|) | E)) = c * (Integral (M,(|.g.| | E))) ) )