theorem Th8: :: INTEGR10:8

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_ext_Riemann_integrable_on a & g is_+infty_ext_Riemann_integrable_on a holds
( f + g is_+infty_ext_Riemann_integrable_on a & infty_ext_right_integral ((f + g),a) = (infty_ext_right_integral (f,a)) + (infty_ext_right_integral (g,a)) )