theorem Th34: :: INTEGR25:34

for f being PartFunc of REAL,REAL
for b being Real st dom f = REAL & f is_-infty_improper_integrable_on b & f is_+infty_improper_integrable_on b & ( not improper_integral_-infty (f,b) = -infty or not improper_integral_+infty (f,b) = +infty ) & ( not improper_integral_-infty (f,b) = +infty or not improper_integral_+infty (f,b) = -infty ) holds
for b2 being Real st b <= b2 holds
(improper_integral_-infty (f,b)) + (improper_integral_+infty (f,b)) = (improper_integral_-infty (f,b2)) + (improper_integral_+infty (f,b2))