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