theorem :: INTEGR10:10

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