for f being PartFunc of REAL,REAL
for b being Real st f is_-infty_ext_Riemann_integrable_on b holds
f is_-infty_improper_integrable_on b