let f be PartFunc of REAL,REAL; :: thesis: for d being Real st left_closed_halfline d c= dom f & f is_-infty_ext_Riemann_integrable_on d holds
for b, c being Real st b < c & c <= d holds
( f is_right_ext_Riemann_integrable_on b,c & f is_left_ext_Riemann_integrable_on b,c )
let d be Real; :: thesis: ( left_closed_halfline d c= dom f & f is_-infty_ext_Riemann_integrable_on d implies for b, c being Real st b < c & c <= d holds
( f is_right_ext_Riemann_integrable_on b,c & f is_left_ext_Riemann_integrable_on b,c ) )
assume that
A1: left_closed_halfline d c= dom f and
A2: f is_-infty_ext_Riemann_integrable_on d ; :: thesis: for b, c being Real st b < c & c <= d holds
( f is_right_ext_Riemann_integrable_on b,c & f is_left_ext_Riemann_integrable_on b,c )

hereby :: thesis: verum

let b, c be Real; :: thesis: ( b < c & c <= d implies ( f is_right_ext_Riemann_integrable_on b,c & f is_left_ext_Riemann_integrable_on b,c ) )
assume A3: ( b < c & c <= d ) ; :: thesis: ( f is_right_ext_Riemann_integrable_on b,c & f is_left_ext_Riemann_integrable_on b,c )
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: verum

end;