let f be PartFunc of REAL,REAL; :: thesis:
let d be Real; :: thesis:
assume that
A1: left_closed_halfline d c= dom f and
A2: f is_-infty_ext_Riemann_integrable_on d ; :: thesis:

hereby :: thesis:

let b, c be Real; :: thesis:
assume A3: ( b < c & c <= d ) ; :: thesis:
then b < d by XXREAL_0:2;
then A4: ( f is_integrable_on ['b,d'] & f | ['b,d'] is bounded ) by A2, INTEGR10:def 6;
['b,d'] = [.b,d.] by A3, XXREAL_0:2, INTEGRA5:def 3;
then ['b,d'] c= ].-infty,d.] by XXREAL_1:265;
then ['b,d'] c= dom f by A1;
then ( f is_integrable_on ['b,c'] & f | ['b,c'] is bounded & ['b,c'] c= dom f ) by A3, A4, INTEGRA6:18;
hence ( f is_right_ext_Riemann_integrable_on b,c & f is_left_ext_Riemann_integrable_on b,c ) by A3, INTEGR24:19, INTEGR24:18; :: thesis:

end;