for f being PartFunc of REAL,REAL st dom f = REAL holds
( f is infty_ext_Riemann_integrable iff for a being Real holds
( f is_+infty_ext_Riemann_integrable_on a & f is_-infty_ext_Riemann_integrable_on a ) )