theorem Th25: :: INTEGRA2:25

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