theorem
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 ) )