let f be PartFunc of REAL,REAL; :: thesis: for r being Real st dom f = REAL & f is_improper_integrable_on_REAL holds
( - f is_improper_integrable_on_REAL & improper_integral_on_REAL (- f) = - (improper_integral_on_REAL f) )
let r be Real; :: thesis: ( dom f = REAL & f is_improper_integrable_on_REAL implies ( - f is_improper_integrable_on_REAL & improper_integral_on_REAL (- f) = - (improper_integral_on_REAL f) ) )
assume ( dom f = REAL & f is_improper_integrable_on_REAL ) ; :: thesis: ( - f is_improper_integrable_on_REAL & improper_integral_on_REAL (- f) = - (improper_integral_on_REAL f) )
then ( (- 1) (#) f is_improper_integrable_on_REAL & improper_integral_on_REAL ((- 1) (#) f) = (- 1) * (improper_integral_on_REAL f) ) by Th49;
hence ( - f is_improper_integrable_on_REAL & improper_integral_on_REAL (- f) = - (improper_integral_on_REAL f) ) by XXREAL_3:91; :: thesis: verum