theorem Th23: :: INTEGRA2:23

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