theorem Th30:
for
f being
PartFunc of
REAL,
REAL for
b,
c being
Real st
b >= c &
right_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_right_integral (
f,
c) implies
improper_integral_+infty (
f,
b)
= infty_ext_right_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 ) )