for f being PartFunc of REAL,REAL
for a, c being Real st f is_improper_integrable_on a,c holds
ex b being Real st
( a < b & b < c & ( ( left_improper_integral (f,a,b) = ext_left_integral (f,a,b) & right_improper_integral (f,b,c) = ext_right_integral (f,b,c) ) or (left_improper_integral (f,a,b)) + (right_improper_integral (f,b,c)) = +infty or (left_improper_integral (f,a,b)) + (right_improper_integral (f,b,c)) = -infty ) )