for f being PartFunc of REAL,REAL st dom f = REAL & f is_improper_integrable_on_REAL holds
for b1, b2 being Real holds (improper_integral_-infty (f,b1)) + (improper_integral_+infty (f,b1)) = (improper_integral_-infty (f,b2)) + (improper_integral_+infty (f,b2))