theorem Th31:
for
f being
PartFunc of
REAL,
REAL for
b,
c being
Real st
b >= c &
right_closed_halfline c c= dom f &
f | ['c,b'] is
bounded &
f is_+infty_improper_integrable_on b &
f is_integrable_on ['c,b'] holds
(
f is_+infty_improper_integrable_on c & (
improper_integral_+infty (
f,
b)
= infty_ext_right_integral (
f,
b) implies
improper_integral_+infty (
f,
c)
= (improper_integral_+infty (f,b)) + (integral (f,c,b)) ) & (
improper_integral_+infty (
f,
b)
= +infty implies
improper_integral_+infty (
f,
c)
= +infty ) & (
improper_integral_+infty (
f,
b)
= -infty implies
improper_integral_+infty (
f,
c)
= -infty ) )