theorem :: INTEGR25:32

for f being PartFunc of REAL,REAL st f is_improper_integrable_on_REAL holds
ex b being Real st
( ( improper_integral_-infty (f,b) = infty_ext_left_integral (f,b) & improper_integral_+infty (f,b) = infty_ext_right_integral (f,b) ) or (improper_integral_-infty (f,b)) + (improper_integral_+infty (f,b)) = +infty or (improper_integral_-infty (f,b)) + (improper_integral_+infty (f,b)) = -infty )