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