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 ) )