let f be PartFunc of REAL,REAL; :: thesis: 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 ) )
let b, c be Real; :: thesis: ( 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'] implies ( 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 ) ) )
assume that
A1: b >= c and
A2: right_closed_halfline c c= dom f and
A3: f | ['c,b'] is bounded and
A4: f is_+infty_improper_integrable_on b and
A5: f is_integrable_on ['c,b'] ; :: thesis: ( 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 ) )

per cases ( f is_+infty_ext_Riemann_integrable_on b or not f is_+infty_ext_Riemann_integrable_on b ) ;

suppose f is_+infty_ext_Riemann_integrable_on b ; :: thesis: ( 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 ) )

then improper_integral_+infty (f,b) = infty_ext_right_integral (f,b) by A4, Th27;
hence ( 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 ) ) by A1, A2, A3, A4, A5, Lm15; :: thesis: verum

end;

suppose A6: not f is_+infty_ext_Riemann_integrable_on b ; :: thesis: ( 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 ) )

per cases ( improper_integral_+infty (f,b) = +infty or improper_integral_+infty (f,b) = -infty ) by A4, A6, Th27;

suppose improper_integral_+infty (f,b) = +infty ; :: thesis: ( 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 ) )

hence ( 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 ) ) by A1, A2, A3, A4, A5, Lm16; :: thesis: verum

end;

suppose improper_integral_+infty (f,b) = -infty ; :: thesis: ( 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 ) )

hence ( 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 ) ) by A1, A2, A3, A4, A5, Lm17; :: thesis: verum

end;

end;

end;

end;