theorem Th25:
for
f being
PartFunc of
REAL,
REAL for
b,
c being
Real st
b <= c &
left_closed_halfline c c= dom f &
f is_-infty_improper_integrable_on c holds
(
f is_-infty_improper_integrable_on b & (
improper_integral_-infty (
f,
c)
= infty_ext_left_integral (
f,
c) implies
improper_integral_-infty (
f,
b)
= infty_ext_left_integral (
f,
b) ) & (
improper_integral_-infty (
f,
c)
= +infty implies
improper_integral_-infty (
f,
b)
= +infty ) & (
improper_integral_-infty (
f,
c)
= -infty implies
improper_integral_-infty (
f,
b)
= -infty ) )