let f be PartFunc of REAL,REAL; :: thesis:
assume A1: dom f = REAL ; :: thesis:

hereby :: thesis:

assume A2: f is infty_ext_Riemann_integrable ; :: thesis:
then A3: ( f is_+infty_ext_Riemann_integrable_on 0 & f is_-infty_ext_Riemann_integrable_on 0 ) by INTEGR10:def 9;
thus for a being Real holds
( f is_+infty_ext_Riemann_integrable_on a & f is_-infty_ext_Riemann_integrable_on a ) :: thesis:

proof

let a be Real; :: thesis:

per cases ;

suppose A4: 0 <= a ; :: thesis:

right_closed_halfline 0 c= dom f by A1;
hence f is_+infty_ext_Riemann_integrable_on a by A2, A4, Th16, INTEGR10:def 9; :: thesis:
A5: left_closed_halfline a c= dom f by A1;
( f is_integrable_on ['0,a'] & f | ['0,a'] is bounded ) by A3, A4, INTEGR10:def 5;
hence f is_-infty_ext_Riemann_integrable_on a by A3, A4, A5, Th17; :: thesis:

end;

suppose A6: a < 0 ; :: thesis:

A7: right_closed_halfline a c= dom f by A1;
( f is_integrable_on ['a,0'] & f | ['a,0'] is bounded ) by A3, A6, INTEGR10:def 6;
hence f is_+infty_ext_Riemann_integrable_on a by A3, A6, A7, Th18; :: thesis:
left_closed_halfline 0 c= dom f by A1;
hence f is_-infty_ext_Riemann_integrable_on a by A2, A6, Th15, INTEGR10:def 9; :: thesis:

end;

end;

end;

end;

assume for a being Real holds
( f is_+infty_ext_Riemann_integrable_on a & f is_-infty_ext_Riemann_integrable_on a ) ; :: thesis:
then ( f is_+infty_ext_Riemann_integrable_on 0 & f is_-infty_ext_Riemann_integrable_on 0 ) ;
hence f is infty_ext_Riemann_integrable by INTEGR10:def 9; :: thesis: