theorem Th24: :: INTEGRA2:24

for r being Real
for i being Nat
for A being non empty closed_interval Subset of REAL
for f being Function of A,REAL
for D being Division of A st i in dom D & f | A is bounded_above & r <= 0 holds
(lower_volume ((r (#) f),D)) . i = r * ((upper_volume (f,D)) . i)