theorem Th51: :: INTEGR25:51

for f, g being PartFunc of REAL,REAL st dom f = REAL & dom g = REAL & f is_improper_integrable_on_REAL & g is_improper_integrable_on_REAL & ( not improper_integral_on_REAL f = +infty or not improper_integral_on_REAL g = -infty ) & ( not improper_integral_on_REAL f = -infty or not improper_integral_on_REAL g = +infty ) holds
( f + g is_improper_integrable_on_REAL & improper_integral_on_REAL (f + g) = (improper_integral_on_REAL f) + (improper_integral_on_REAL g) )