let f be PartFunc of REAL,REAL; :: thesis: for a, b, r being Real st ].a,b.[ c= dom f & f is_improper_integrable_on a,b holds
( - f is_improper_integrable_on a,b & improper_integral ((- f),a,b) = - (improper_integral (f,a,b)) )
let a, b, r be Real; :: thesis: ( ].a,b.[ c= dom f & f is_improper_integrable_on a,b implies ( - f is_improper_integrable_on a,b & improper_integral ((- f),a,b) = - (improper_integral (f,a,b)) ) )
assume ( ].a,b.[ c= dom f & f is_improper_integrable_on a,b ) ; :: thesis: ( - f is_improper_integrable_on a,b & improper_integral ((- f),a,b) = - (improper_integral (f,a,b)) )
then ( (- 1) (#) f is_improper_integrable_on a,b & improper_integral (((- 1) (#) f),a,b) = (- 1) * (improper_integral (f,a,b)) ) by Th61;
hence ( - f is_improper_integrable_on a,b & improper_integral ((- f),a,b) = - (improper_integral (f,a,b)) ) by XXREAL_3:91; :: thesis: verum