for f being PartFunc of REAL,REAL
for a being Real st f is_+infty_ext_Riemann_integrable_on a holds
f is_+infty_improper_integrable_on a