theorem Th55: :: INTEGR24:55

for f being 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)) )