for f being PartFunc of REAL,REAL
for b being Real holds
( not f is_-infty_improper_integrable_on b or ( f is_-infty_ext_Riemann_integrable_on b & improper_integral_-infty (f,b) = infty_ext_left_integral (f,b) ) or ( not f is_-infty_ext_Riemann_integrable_on b & improper_integral_-infty (f,b) = +infty ) or ( not f is_-infty_ext_Riemann_integrable_on b & improper_integral_-infty (f,b) = -infty ) )