theorem :: INTEGRA9:29

for r, p being Real
for f, g being PartFunc of REAL,REAL
for A being non empty closed_interval Subset of REAL st (f (#) g) | A is bounded & f (#) g is_integrable_on A & A c= dom (f (#) g) holds
|||((r (#) f),(p (#) g),A)||| = (r * p) * |||(f,g,A)|||