theorem Th46: :: INTEGR25:46
for f, g being PartFunc of REAL,REAL
for a being Real st right_closed_halfline a c= dom f & right_closed_halfline a c= dom g & f is_+infty_improper_integrable_on a & g is_+infty_improper_integrable_on a & ( not improper_integral_+infty (f,a) = +infty or not improper_integral_+infty (g,a) = -infty ) & ( not improper_integral_+infty (f,a) = -infty or not improper_integral_+infty (g,a) = +infty ) holds
( f + g is_+infty_improper_integrable_on a & improper_integral_+infty ((f + g),a) = (improper_integral_+infty (f,a)) + (improper_integral_+infty (g,a)) )