theorem Th4A: :: INTEGR22:12

for A being non empty closed_interval Subset of REAL
for r being Real
for rho, rho1 being Function of A,REAL
for u being PartFunc of REAL,REAL st rho is bounded_variation & rho1 is bounded_variation & dom u = A & rho = r (#) rho1 & u is_RiemannStieltjes_integrable_with rho1 holds
( u is_RiemannStieltjes_integrable_with rho & integral (u,rho) = r * (integral (u,rho1)) )