theorem Th29:
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_right_ext_Riemann_integrable_on a,
b &
g is_right_ext_Riemann_integrable_on a,
b holds
(
f + g is_right_ext_Riemann_integrable_on a,
b &
ext_right_integral (
(f + g),
a,
b)
= (ext_right_integral (f,a,b)) + (ext_right_integral (g,a,b)) )