let f be PartFunc of REAL,REAL; :: thesis: for a being Real st right_closed_halfline a c= dom f & f is_+infty_ext_Riemann_integrable_on a holds
for b, c being Real st a <= b & b < c holds
( f is_right_ext_Riemann_integrable_on b,c & f is_left_ext_Riemann_integrable_on b,c )
let a be Real; :: thesis: ( right_closed_halfline a c= dom f & f is_+infty_ext_Riemann_integrable_on a implies for b, c being Real st a <= b & b < c holds
( f is_right_ext_Riemann_integrable_on b,c & f is_left_ext_Riemann_integrable_on b,c ) )
assume that
A1: right_closed_halfline a c= dom f and
A2: f is_+infty_ext_Riemann_integrable_on a ; :: thesis: for b, c being Real st a <= b & b < c 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: ( a <= b & b < c implies ( f is_right_ext_Riemann_integrable_on b,c & f is_left_ext_Riemann_integrable_on b,c ) )
assume A3: ( a <= b & b < c ) ; :: thesis: ( f is_right_ext_Riemann_integrable_on b,c & f is_left_ext_Riemann_integrable_on b,c )
then a < c by XXREAL_0:2;
then A4: ( f is_integrable_on ['a,c'] & f | ['a,c'] is bounded ) by A2, INTEGR10:def 5;
['a,c'] = [.a,c.] by A3, XXREAL_0:2, INTEGRA5:def 3;
then ['a,c'] c= [.a,+infty.[ by XXREAL_1:251;
then ['a,c'] 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;