theorem Th32: :: COUSIN2:35

for I being non empty closed_interval Subset of REAL
for TD being tagged_division of I
for f being HK-integrable Function of I,REAL
for r being Real holds tagged_volume ((r (#) f),TD) = r * (tagged_volume (f,TD))