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