let f be PartFunc of REAL,REAL; :: thesis: 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)) )
let b be Real; :: thesis: ( left_closed_halfline b c= dom f & f is_-infty_improper_integrable_on b implies ( - f is_-infty_improper_integrable_on b & improper_integral_-infty ((- f),b) = - (improper_integral_-infty (f,b)) ) )
assume A1: ( left_closed_halfline b c= dom f & f is_-infty_improper_integrable_on b ) ; :: thesis: ( - f is_-infty_improper_integrable_on b & improper_integral_-infty ((- f),b) = - (improper_integral_-infty (f,b)) )
hence - f is_-infty_improper_integrable_on b by Th41; :: thesis: improper_integral_-infty ((- f),b) = - (improper_integral_-infty (f,b))
improper_integral_-infty ((- f),b) = (- 1) * (improper_integral_-infty (f,b)) by A1, Th41;
hence improper_integral_-infty ((- f),b) = - (improper_integral_-infty (f,b)) by XXREAL_3:91; :: thesis: verum