theorem Th26:
for
f being
PartFunc of
REAL,
REAL for
b,
c being
Real st
b <= c &
left_closed_halfline c c= dom f &
f | ['b,c'] is
bounded &
f is_-infty_improper_integrable_on b &
f is_integrable_on ['b,c'] holds
(
f is_-infty_improper_integrable_on c & (
improper_integral_-infty (
f,
b)
= infty_ext_left_integral (
f,
b) implies
improper_integral_-infty (
f,
c)
= (improper_integral_-infty (f,b)) + (integral (f,b,c)) ) & (
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 ) )