theorem Th41: :: INTEGR25:41

for f being PartFunc of REAL,REAL
for b, r being Real st left_closed_halfline b c= dom f & f is_-infty_improper_integrable_on b holds
( r (#) f is_-infty_improper_integrable_on b & improper_integral_-infty ((r (#) f),b) = r * (improper_integral_-infty (f,b)) )