theorem Th26: :: INTEGRA2:26

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_below & r <= 0 holds
(upper_volume ((r (#) f),D)) . i = r * ((lower_volume (f,D)) . i)