let f be PartFunc of REAL,REAL; :: thesis: for a, b being Real st a < b & [.a,b.[ c= dom f & f is_right_improper_integrable_on a,b holds
( - f is_right_improper_integrable_on a,b & right_improper_integral ((- f),a,b) = - (right_improper_integral (f,a,b)) )
let a, b be Real; :: thesis: ( a < b & [.a,b.[ c= dom f & f is_right_improper_integrable_on a,b implies ( - f is_right_improper_integrable_on a,b & right_improper_integral ((- f),a,b) = - (right_improper_integral (f,a,b)) ) )
assume A1: ( a < b & [.a,b.[ c= dom f & f is_right_improper_integrable_on a,b ) ; :: thesis: ( - f is_right_improper_integrable_on a,b & right_improper_integral ((- f),a,b) = - (right_improper_integral (f,a,b)) )
hence - f is_right_improper_integrable_on a,b by Th54; :: thesis: right_improper_integral ((- f),a,b) = - (right_improper_integral (f,a,b))
right_improper_integral ((- f),a,b) = (- 1) * (right_improper_integral (f,a,b)) by A1, Th54;
hence right_improper_integral ((- f),a,b) = - (right_improper_integral (f,a,b)) by XXREAL_3:91; :: thesis: verum