for f being PartFunc of REAL,REAL
for b being Real st dom f = REAL & f is_improper_integrable_on_REAL holds
( f is_-infty_improper_integrable_on b & f is_+infty_improper_integrable_on b & improper_integral_on_REAL f = (improper_integral_-infty (f,b)) + (improper_integral_+infty (f,b)) )