for f being PartFunc of REAL,REAL
for r being Real st dom f = REAL & f is_improper_integrable_on_REAL holds
( r (#) f is_improper_integrable_on_REAL & improper_integral_on_REAL (r (#) f) = r * (improper_integral_on_REAL f) )