theorem Th45: :: INTEGR25:45

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