:: deftheorem defines infty_ext_Riemann_integrable INTEGR10:def 9 :
for f being PartFunc of REAL,REAL holds
( f is infty_ext_Riemann_integrable iff ( f is_+infty_ext_Riemann_integrable_on 0 & f is_-infty_ext_Riemann_integrable_on 0 ) );