let f be PartFunc of REAL,REAL; :: thesis:
let a, c be Real; :: thesis:
assume f is_improper_integrable_on a,c ; :: thesis:
then consider b being Real such that
A1: ( a < b & b < c ) and
A2: f is_left_improper_integrable_on a,b and
A3: f is_right_improper_integrable_on b,c and
A4: ( not left_improper_integral (f,a,b) = -infty or not right_improper_integral (f,b,c) = +infty ) and
A5: ( not left_improper_integral (f,a,b) = +infty or not right_improper_integral (f,b,c) = -infty ) ;
consider IL being PartFunc of REAL,REAL such that
A6: dom IL = ].a,b.] and
A7: for x being Real st x in dom IL holds
IL . x = integral (f,x,b) and
A8: ( IL is_right_convergent_in a or IL is_right_divergent_to+infty_in a or IL is_right_divergent_to-infty_in a ) by A2;
consider IR being PartFunc of REAL,REAL such that
A9: dom IR = [.b,c.[ and
A10: for x being Real st x in dom IR holds
IR . x = integral (f,b,x) and
A11: ( IR is_left_convergent_in c or IR is_left_divergent_to+infty_in c or IR is_left_divergent_to-infty_in c ) by A3;

per cases by A8;

suppose IL is_right_convergent_in a ; :: thesis:

then f is_left_ext_Riemann_integrable_on a,b by A2, A6, A7, INTEGR10:def 2;
then A12: left_improper_integral (f,a,b) = ext_left_integral (f,a,b) by A2, Th34;

per cases by A11;

suppose IR is_left_convergent_in c ; :: thesis:

then f is_right_ext_Riemann_integrable_on b,c by A3, A9, A10, INTEGR10:def 1;
then right_improper_integral (f,b,c) = ext_right_integral (f,b,c) by A3, Th39;
hence ex b being Real st
( a < b & b < c & ( ( left_improper_integral (f,a,b) = ext_left_integral (f,a,b) & right_improper_integral (f,b,c) = ext_right_integral (f,b,c) ) or (left_improper_integral (f,a,b)) + (right_improper_integral (f,b,c)) = +infty or (left_improper_integral (f,a,b)) + (right_improper_integral (f,b,c)) = -infty ) ) by A1, A12; :: thesis:

end;

suppose IR is_left_divergent_to+infty_in c ; :: thesis:

then right_improper_integral (f,b,c) = +infty by A3, A9, A10, Def4;
then (left_improper_integral (f,a,b)) + (right_improper_integral (f,b,c)) = +infty by A12, XXREAL_3:def 2;
hence ex b being Real st
( a < b & b < c & ( ( left_improper_integral (f,a,b) = ext_left_integral (f,a,b) & right_improper_integral (f,b,c) = ext_right_integral (f,b,c) ) or (left_improper_integral (f,a,b)) + (right_improper_integral (f,b,c)) = +infty or (left_improper_integral (f,a,b)) + (right_improper_integral (f,b,c)) = -infty ) ) by A1; :: thesis:

end;

suppose IR is_left_divergent_to-infty_in c ; :: thesis:

then right_improper_integral (f,b,c) = -infty by A3, A9, A10, Def4;
then (left_improper_integral (f,a,b)) + (right_improper_integral (f,b,c)) = -infty by A12, XXREAL_3:def 2;
hence ex b being Real st
( a < b & b < c & ( ( left_improper_integral (f,a,b) = ext_left_integral (f,a,b) & right_improper_integral (f,b,c) = ext_right_integral (f,b,c) ) or (left_improper_integral (f,a,b)) + (right_improper_integral (f,b,c)) = +infty or (left_improper_integral (f,a,b)) + (right_improper_integral (f,b,c)) = -infty ) ) by A1; :: thesis:

end;

end;

end;

suppose A13: IL is_right_divergent_to+infty_in a ; :: thesis:

then A14: left_improper_integral (f,a,b) = +infty by A2, A6, A7, Def3;

per cases by A11, A3, A9, A10, A13, A5, A2, A6, A7, Def3, Def4;

suppose IR is_left_convergent_in c ; :: thesis:

then f is_right_ext_Riemann_integrable_on b,c by A3, A9, A10, INTEGR10:def 1;
then right_improper_integral (f,b,c) = ext_right_integral (f,b,c) by A3, Th39;
then (left_improper_integral (f,a,b)) + (right_improper_integral (f,b,c)) = +infty by A14, XXREAL_3:def 2;
hence ex b being Real st
( a < b & b < c & ( ( left_improper_integral (f,a,b) = ext_left_integral (f,a,b) & right_improper_integral (f,b,c) = ext_right_integral (f,b,c) ) or (left_improper_integral (f,a,b)) + (right_improper_integral (f,b,c)) = +infty or (left_improper_integral (f,a,b)) + (right_improper_integral (f,b,c)) = -infty ) ) by A1; :: thesis:

end;

suppose IR is_left_divergent_to+infty_in c ; :: thesis:

then right_improper_integral (f,b,c) = +infty by A3, A9, A10, Def4;
then (left_improper_integral (f,a,b)) + (right_improper_integral (f,b,c)) = +infty by A14, XXREAL_3:def 2;
hence ex b being Real st
( a < b & b < c & ( ( left_improper_integral (f,a,b) = ext_left_integral (f,a,b) & right_improper_integral (f,b,c) = ext_right_integral (f,b,c) ) or (left_improper_integral (f,a,b)) + (right_improper_integral (f,b,c)) = +infty or (left_improper_integral (f,a,b)) + (right_improper_integral (f,b,c)) = -infty ) ) by A1; :: thesis:

end;

end;

end;

suppose A15: IL is_right_divergent_to-infty_in a ; :: thesis:

then A16: left_improper_integral (f,a,b) = -infty by A2, A6, A7, Def3;

per cases by A11, A3, A9, A10, A15, A4, A2, A6, A7, Def3, Def4;

suppose IR is_left_convergent_in c ; :: thesis:

then f is_right_ext_Riemann_integrable_on b,c by A3, A9, A10, INTEGR10:def 1;
then right_improper_integral (f,b,c) = ext_right_integral (f,b,c) by A3, Th39;
then (left_improper_integral (f,a,b)) + (right_improper_integral (f,b,c)) = -infty by A16, XXREAL_3:def 2;
hence ex b being Real st
( a < b & b < c & ( ( left_improper_integral (f,a,b) = ext_left_integral (f,a,b) & right_improper_integral (f,b,c) = ext_right_integral (f,b,c) ) or (left_improper_integral (f,a,b)) + (right_improper_integral (f,b,c)) = +infty or (left_improper_integral (f,a,b)) + (right_improper_integral (f,b,c)) = -infty ) ) by A1; :: thesis:

end;

suppose IR is_left_divergent_to-infty_in c ; :: thesis:

then right_improper_integral (f,b,c) = -infty by A3, A9, A10, Def4;
then (left_improper_integral (f,a,b)) + (right_improper_integral (f,b,c)) = -infty by A16, XXREAL_3:def 2;
hence ex b being Real st
( a < b & b < c & ( ( left_improper_integral (f,a,b) = ext_left_integral (f,a,b) & right_improper_integral (f,b,c) = ext_right_integral (f,b,c) ) or (left_improper_integral (f,a,b)) + (right_improper_integral (f,b,c)) = +infty or (left_improper_integral (f,a,b)) + (right_improper_integral (f,b,c)) = -infty ) ) by A1; :: thesis:

end;

end;

end;

end;