theorem Th37: :: INTEGR24:37

for f being PartFunc of REAL,REAL
for a, b, c being Real st a < b & b <= c & ].a,c.] c= dom f & f is_left_improper_integrable_on a,c holds
( f is_left_improper_integrable_on a,b & ( left_improper_integral (f,a,c) = ext_left_integral (f,a,c) implies left_improper_integral (f,a,b) = ext_left_integral (f,a,b) ) & ( left_improper_integral (f,a,c) = +infty implies left_improper_integral (f,a,b) = +infty ) & ( left_improper_integral (f,a,c) = -infty implies left_improper_integral (f,a,b) = -infty ) )