theorem Th31: :: COUSIN2:34

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
for i being Nat st i in dom TD holds
(tagged_volume ((r (#) f),TD)) . i = (r * (f . ((tagged_of TD) . i))) * (vol (divset ((division_of TD),i)))