consider c being Real such that
A2: ( a < c & c < b ) and
A3: f is_left_improper_integrable_on a,c and
A4: f is_right_improper_integrable_on c,b and
A5: ( not left_improper_integral (f,a,c) = -infty or not right_improper_integral (f,c,b) = +infty ) and
A6: ( not left_improper_integral (f,a,c) = +infty or not right_improper_integral (f,c,b) = -infty ) by A1;

per cases by A3, Th34;

suppose A7: ( f is_left_ext_Riemann_integrable_on a,c & left_improper_integral (f,a,c) = ext_left_integral (f,a,c) ) ; :: thesis:

per cases by A4, Th39;

suppose A8: ( f is_right_ext_Riemann_integrable_on c,b & right_improper_integral (f,c,b) = ext_right_integral (f,c,b) ) ; :: thesis:

reconsider IT = (ext_left_integral (f,a,c)) + (ext_right_integral (f,c,b)) as ExtReal ;
take IT ; :: thesis:
IT = (left_improper_integral (f,a,c)) + (right_improper_integral (f,c,b)) by A7, A8, XXREAL_3:def 2;
hence ex c being Real st
( a < c & c < b & f is_left_improper_integrable_on a,c & f is_right_improper_integrable_on c,b & IT = (left_improper_integral (f,a,c)) + (right_improper_integral (f,c,b)) ) by A2, A3, A4; :: thesis:

end;

suppose right_improper_integral (f,c,b) = +infty ; :: thesis:

then A9: (left_improper_integral (f,a,c)) + (right_improper_integral (f,c,b)) = +infty by A5, XXREAL_3:def 2;
take IT = +infty ; :: thesis:
thus ex c being Real st
( a < c & c < b & f is_left_improper_integrable_on a,c & f is_right_improper_integrable_on c,b & IT = (left_improper_integral (f,a,c)) + (right_improper_integral (f,c,b)) ) by A2, A3, A4, A9; :: thesis:

end;

suppose right_improper_integral (f,c,b) = -infty ; :: thesis:

then A10: (left_improper_integral (f,a,c)) + (right_improper_integral (f,c,b)) = -infty by A6, XXREAL_3:def 2;
take IT = -infty ; :: thesis:
thus ex c being Real st
( a < c & c < b & f is_left_improper_integrable_on a,c & f is_right_improper_integrable_on c,b & IT = (left_improper_integral (f,a,c)) + (right_improper_integral (f,c,b)) ) by A2, A3, A4, A10; :: thesis:

end;

end;

end;

suppose A11: left_improper_integral (f,a,c) = +infty ; :: thesis:

per cases by A4, A6, Th39;

suppose ( f is_right_ext_Riemann_integrable_on c,b & right_improper_integral (f,c,b) = ext_right_integral (f,c,b) ) ; :: thesis:

then A12: (left_improper_integral (f,a,c)) + (right_improper_integral (f,c,b)) = +infty by A11, XXREAL_3:def 2;
take IT = +infty ; :: thesis:
thus ex c being Real st
( a < c & c < b & f is_left_improper_integrable_on a,c & f is_right_improper_integrable_on c,b & IT = (left_improper_integral (f,a,c)) + (right_improper_integral (f,c,b)) ) by A2, A3, A4, A12; :: thesis:

end;

suppose right_improper_integral (f,c,b) = +infty ; :: thesis:

then A13: (left_improper_integral (f,a,c)) + (right_improper_integral (f,c,b)) = +infty by A11, XXREAL_3:def 2;
take IT = +infty ; :: thesis:
thus ex c being Real st
( a < c & c < b & f is_left_improper_integrable_on a,c & f is_right_improper_integrable_on c,b & IT = (left_improper_integral (f,a,c)) + (right_improper_integral (f,c,b)) ) by A2, A3, A4, A13; :: thesis:

end;

end;

end;

suppose A14: left_improper_integral (f,a,c) = -infty ; :: thesis:

per cases by A4, A5, Th39;

suppose ( f is_right_ext_Riemann_integrable_on c,b & right_improper_integral (f,c,b) = ext_right_integral (f,c,b) ) ; :: thesis:

then A15: (left_improper_integral (f,a,c)) + (right_improper_integral (f,c,b)) = -infty by A14, XXREAL_3:def 2;
take IT = -infty ; :: thesis:
thus ex c being Real st
( a < c & c < b & f is_left_improper_integrable_on a,c & f is_right_improper_integrable_on c,b & IT = (left_improper_integral (f,a,c)) + (right_improper_integral (f,c,b)) ) by A2, A3, A4, A15; :: thesis:

end;

suppose right_improper_integral (f,c,b) = -infty ; :: thesis:

then A16: (left_improper_integral (f,a,c)) + (right_improper_integral (f,c,b)) = -infty by A14, XXREAL_3:def 2;
take IT = -infty ; :: thesis:
thus ex c being Real st
( a < c & c < b & f is_left_improper_integrable_on a,c & f is_right_improper_integrable_on c,b & IT = (left_improper_integral (f,a,c)) + (right_improper_integral (f,c,b)) ) by A2, A3, A4, A16; :: thesis:

end;

end;

end;

end;