let f be PartFunc of REAL,REAL; 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; ( 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 )
; ( - 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; 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; verum