theorem
for
f,
g being
PartFunc of
REAL,
REAL for
a,
b being
Real st
a < b &
[.a,b.[ c= dom f &
[.a,b.[ c= dom g &
f is_right_improper_integrable_on a,
b &
g is_right_improper_integrable_on a,
b & ( not
right_improper_integral (
f,
a,
b)
= +infty or not
right_improper_integral (
g,
a,
b)
= +infty ) & ( not
right_improper_integral (
f,
a,
b)
= -infty or not
right_improper_integral (
g,
a,
b)
= -infty ) holds
(
f - g is_right_improper_integrable_on a,
b &
right_improper_integral (
(f - g),
a,
b)
= (right_improper_integral (f,a,b)) - (right_improper_integral (g,a,b)) )