theorem :: INTEGR25:48

for f, g being PartFunc of REAL,REAL
for a being Real st right_closed_halfline a c= dom f & right_closed_halfline a c= dom g & f is_+infty_improper_integrable_on a & g is_+infty_improper_integrable_on a & ( not improper_integral_+infty (f,a) = +infty or not improper_integral_+infty (g,a) = +infty ) & ( not improper_integral_+infty (f,a) = -infty or not improper_integral_+infty (g,a) = -infty ) holds
( f - g is_+infty_improper_integrable_on a & improper_integral_+infty ((f - g),a) = (improper_integral_+infty (f,a)) - (improper_integral_+infty (g,a)) )