theorem Lm4A: :: INTEGR22:11

for A, B being non empty closed_interval Subset of REAL
for r being Real
for rho, rho1 being Function of A,REAL st B c= A & rho = r (#) rho1 holds
vol (B,rho) = r * (vol (B,rho1))