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