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