theorem Th58: :: INTEGR24:58

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_improper_integrable_on a,b & g is_right_improper_integrable_on a,b & ( not right_improper_integral (f,a,b) = +infty or not right_improper_integral (g,a,b) = -infty ) & ( not right_improper_integral (f,a,b) = -infty or not right_improper_integral (g,a,b) = +infty ) holds
( f + g is_right_improper_integrable_on a,b & right_improper_integral ((f + g),a,b) = (right_improper_integral (f,a,b)) + (right_improper_integral (g,a,b)) )