theorem Th35: :: COUSIN2:38

for I being non empty closed_interval Subset of REAL
for f being HK-integrable Function of I,REAL
for r being Real st f is HK-integrable holds
( r (#) f is HK-integrable Function of I,REAL & HK-integral (r (#) f) = r * (HK-integral f) )