theorem :: INTEGR10:6

for f, g being PartFunc of REAL,REAL
for a, b being Real st a < b & ['a,b'] c= dom f & ['a,b'] c= dom g & f is_left_ext_Riemann_integrable_on a,b & g is_left_ext_Riemann_integrable_on a,b holds
( f + g is_left_ext_Riemann_integrable_on a,b & ext_left_integral ((f + g),a,b) = (ext_left_integral (f,a,b)) + (ext_left_integral (g,a,b)) )