consider c being Real such that
A2: f is_-infty_improper_integrable_on c and
A3: f is_+infty_improper_integrable_on c and
A4: ( not improper_integral_-infty (f,c) = -infty or not improper_integral_+infty (f,c) = +infty ) and
A5: ( not improper_integral_-infty (f,c) = +infty or not improper_integral_+infty (f,c) = -infty ) by A1;

per cases by A2, Th22;

suppose A6: ( f is_-infty_ext_Riemann_integrable_on c & improper_integral_-infty (f,c) = infty_ext_left_integral (f,c) ) ; :: thesis:

per cases by A3, Th27;

suppose A7: ( f is_+infty_ext_Riemann_integrable_on c & improper_integral_+infty (f,c) = infty_ext_right_integral (f,c) ) ; :: thesis:

reconsider IT = (infty_ext_left_integral (f,c)) + (infty_ext_right_integral (f,c)) as ExtReal ;
take IT ; :: thesis:
IT = (improper_integral_-infty (f,c)) + (improper_integral_+infty (f,c)) by A6, A7, XXREAL_3:def 2;
hence ex c being Real st
( f is_-infty_improper_integrable_on c & f is_+infty_improper_integrable_on c & IT = (improper_integral_-infty (f,c)) + (improper_integral_+infty (f,c)) ) by A2, A3; :: thesis:

end;

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

then A8: (improper_integral_-infty (f,c)) + (improper_integral_+infty (f,c)) = +infty by A4, XXREAL_3:def 2;
take IT = +infty ; :: thesis:
thus ex c being Real st
( f is_-infty_improper_integrable_on c & f is_+infty_improper_integrable_on c & IT = (improper_integral_-infty (f,c)) + (improper_integral_+infty (f,c)) ) by A2, A3, A8; :: thesis:

end;

suppose improper_integral_+infty (f,c) = -infty ; :: thesis:

then A9: (improper_integral_-infty (f,c)) + (improper_integral_+infty (f,c)) = -infty by A5, XXREAL_3:def 2;
take IT = -infty ; :: thesis:
thus ex c being Real st
( f is_-infty_improper_integrable_on c & f is_+infty_improper_integrable_on c & IT = (improper_integral_-infty (f,c)) + (improper_integral_+infty (f,c)) ) by A2, A3, A9; :: thesis:

end;

end;

end;

suppose A10: improper_integral_-infty (f,c) = +infty ; :: thesis:

per cases by A3, A5, A10, Th27;

suppose ( f is_+infty_ext_Riemann_integrable_on c & improper_integral_+infty (f,c) = infty_ext_right_integral (f,c) ) ; :: thesis:

then A11: (improper_integral_-infty (f,c)) + (improper_integral_+infty (f,c)) = +infty by A10, XXREAL_3:def 2;
take IT = +infty ; :: thesis:
thus ex c being Real st
( f is_-infty_improper_integrable_on c & f is_+infty_improper_integrable_on c & IT = (improper_integral_-infty (f,c)) + (improper_integral_+infty (f,c)) ) by A2, A3, A11; :: thesis:

end;

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

then A12: (improper_integral_-infty (f,c)) + (improper_integral_+infty (f,c)) = +infty by A10, XXREAL_3:def 2;
take IT = +infty ; :: thesis:
thus ex c being Real st
( f is_-infty_improper_integrable_on c & f is_+infty_improper_integrable_on c & IT = (improper_integral_-infty (f,c)) + (improper_integral_+infty (f,c)) ) by A2, A3, A12; :: thesis:

end;

end;

end;

suppose A13: improper_integral_-infty (f,c) = -infty ; :: thesis:

per cases by A3, A4, A13, Th27;

suppose ( f is_+infty_ext_Riemann_integrable_on c & improper_integral_+infty (f,c) = infty_ext_right_integral (f,c) ) ; :: thesis:

then A14: (improper_integral_-infty (f,c)) + (improper_integral_+infty (f,c)) = -infty by A13, XXREAL_3:def 2;
take IT = -infty ; :: thesis:
thus ex c being Real st
( f is_-infty_improper_integrable_on c & f is_+infty_improper_integrable_on c & IT = (improper_integral_-infty (f,c)) + (improper_integral_+infty (f,c)) ) by A2, A3, A14; :: thesis:

end;

suppose improper_integral_+infty (f,c) = -infty ; :: thesis:

then A15: (improper_integral_-infty (f,c)) + (improper_integral_+infty (f,c)) = -infty by A13, XXREAL_3:def 2;
take IT = -infty ; :: thesis:
thus ex c being Real st
( f is_-infty_improper_integrable_on c & f is_+infty_improper_integrable_on c & IT = (improper_integral_-infty (f,c)) + (improper_integral_+infty (f,c)) ) by A2, A3, A15; :: thesis:

end;

end;

end;

end;