theorem Th33: :: INTEGR25:33

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 b1 being Real st b1 <= b holds
(improper_integral_-infty (f,b)) + (improper_integral_+infty (f,b)) = (improper_integral_-infty (f,b1)) + (improper_integral_+infty (f,b1))