theorem Th42: :: INTEGR25:42

for f being PartFunc of REAL,REAL
for a, r being Real st right_closed_halfline a c= dom f & f is_+infty_improper_integrable_on a holds
( r (#) f is_+infty_improper_integrable_on a & improper_integral_+infty ((r (#) f),a) = r * (improper_integral_+infty (f,a)) )