let f be PartFunc of REAL,REAL; :: thesis: ( dom f = REAL implies ( f is infty_ext_Riemann_integrable iff for a being Real holds
( f is_+infty_ext_Riemann_integrable_on a & f is_-infty_ext_Riemann_integrable_on a ) ) )
assume A1: dom f = REAL ; :: thesis: ( f is infty_ext_Riemann_integrable iff for a being Real holds
( f is_+infty_ext_Riemann_integrable_on a & f is_-infty_ext_Riemann_integrable_on a ) )

hereby :: thesis: ( ( for a being Real holds
( f is_+infty_ext_Riemann_integrable_on a & f is_-infty_ext_Riemann_integrable_on a ) ) implies f is infty_ext_Riemann_integrable )

assume A2: f is infty_ext_Riemann_integrable ; :: thesis: for a being Real holds
( f is_+infty_ext_Riemann_integrable_on a & f is_-infty_ext_Riemann_integrable_on a )
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: verum

proof

let a be Real; :: thesis: ( f is_+infty_ext_Riemann_integrable_on a & f is_-infty_ext_Riemann_integrable_on a )

per cases ( 0 <= a or a < 0 ) ;

suppose A4: 0 <= a ; :: thesis: ( f is_+infty_ext_Riemann_integrable_on a & f is_-infty_ext_Riemann_integrable_on a )

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: f is_-infty_ext_Riemann_integrable_on a
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: verum

end;

suppose A6: a < 0 ; :: thesis: ( f is_+infty_ext_Riemann_integrable_on a & f is_-infty_ext_Riemann_integrable_on a )

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: f is_-infty_ext_Riemann_integrable_on a
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: verum

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: f is infty_ext_Riemann_integrable
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: verum