let f be PartFunc of REAL,REAL; :: thesis:
assume f is_improper_integrable_on_REAL ; :: thesis:
then consider b being Real such that
A1: f is_-infty_improper_integrable_on b and
A2: f is_+infty_improper_integrable_on b and
A3: ( not improper_integral_-infty (f,b) = -infty or not improper_integral_+infty (f,b) = +infty ) and
A4: ( not improper_integral_-infty (f,b) = +infty or not improper_integral_+infty (f,b) = -infty ) ;
consider IL being PartFunc of REAL,REAL such that
A5: dom IL = left_closed_halfline b and
A6: for x being Real st x in dom IL holds
IL . x = integral (f,x,b) and
A7: ( IL is convergent_in-infty or IL is divergent_in-infty_to+infty or IL is divergent_in-infty_to-infty ) by A1;
consider IR being PartFunc of REAL,REAL such that
A8: dom IR = right_closed_halfline b and
A9: for x being Real st x in dom IR holds
IR . x = integral (f,b,x) and
A10: ( IR is convergent_in+infty or IR is divergent_in+infty_to+infty or IR is divergent_in+infty_to-infty ) by A2;

per cases by A7;

suppose IL is convergent_in-infty ; :: thesis:

then f is_-infty_ext_Riemann_integrable_on b by A1, A5, A6, INTEGR10:def 6;
then A11: improper_integral_-infty (f,b) = infty_ext_left_integral (f,b) by A1, Th22;

per cases by A10;

suppose IR is convergent_in+infty ; :: thesis:

then f is_+infty_ext_Riemann_integrable_on b by A2, A8, A9, INTEGR10:def 5;
then improper_integral_+infty (f,b) = infty_ext_right_integral (f,b) by A2, Th27;
hence ex b being Real st
( ( improper_integral_-infty (f,b) = infty_ext_left_integral (f,b) & improper_integral_+infty (f,b) = infty_ext_right_integral (f,b) ) or (improper_integral_-infty (f,b)) + (improper_integral_+infty (f,b)) = +infty or (improper_integral_-infty (f,b)) + (improper_integral_+infty (f,b)) = -infty ) by A11; :: thesis:

end;

suppose IR is divergent_in+infty_to+infty ; :: thesis:

then improper_integral_+infty (f,b) = +infty by A2, A8, A9, Def4;
then (improper_integral_-infty (f,b)) + (improper_integral_+infty (f,b)) = +infty by A11, XXREAL_3:def 2;
hence ex b being Real st
( ( improper_integral_-infty (f,b) = infty_ext_left_integral (f,b) & improper_integral_+infty (f,b) = infty_ext_right_integral (f,b) ) or (improper_integral_-infty (f,b)) + (improper_integral_+infty (f,b)) = +infty or (improper_integral_-infty (f,b)) + (improper_integral_+infty (f,b)) = -infty ) ; :: thesis:

end;

suppose IR is divergent_in+infty_to-infty ; :: thesis:

then improper_integral_+infty (f,b) = -infty by A2, A8, A9, Def4;
then (improper_integral_-infty (f,b)) + (improper_integral_+infty (f,b)) = -infty by A11, XXREAL_3:def 2;
hence ex b being Real st
( ( improper_integral_-infty (f,b) = infty_ext_left_integral (f,b) & improper_integral_+infty (f,b) = infty_ext_right_integral (f,b) ) or (improper_integral_-infty (f,b)) + (improper_integral_+infty (f,b)) = +infty or (improper_integral_-infty (f,b)) + (improper_integral_+infty (f,b)) = -infty ) ; :: thesis:

end;

end;

end;

suppose A12: IL is divergent_in-infty_to+infty ; :: thesis:

then A13: improper_integral_-infty (f,b) = +infty by A1, A5, A6, Def3;

per cases by A10, A2, A8, A9, A12, A4, A1, A5, A6, Def3, Def4;

suppose IR is convergent_in+infty ; :: thesis:

then f is_+infty_ext_Riemann_integrable_on b by A2, A8, A9, INTEGR10:def 5;
then improper_integral_+infty (f,b) = infty_ext_right_integral (f,b) by A2, Th27;
then (improper_integral_-infty (f,b)) + (improper_integral_+infty (f,b)) = +infty by A13, XXREAL_3:def 2;
hence ex b being Real st
( ( improper_integral_-infty (f,b) = infty_ext_left_integral (f,b) & improper_integral_+infty (f,b) = infty_ext_right_integral (f,b) ) or (improper_integral_-infty (f,b)) + (improper_integral_+infty (f,b)) = +infty or (improper_integral_-infty (f,b)) + (improper_integral_+infty (f,b)) = -infty ) ; :: thesis:

end;

suppose IR is divergent_in+infty_to+infty ; :: thesis:

then improper_integral_+infty (f,b) = +infty by A2, A8, A9, Def4;
then (improper_integral_-infty (f,b)) + (improper_integral_+infty (f,b)) = +infty by A13, XXREAL_3:def 2;
hence ex b being Real st
( ( improper_integral_-infty (f,b) = infty_ext_left_integral (f,b) & improper_integral_+infty (f,b) = infty_ext_right_integral (f,b) ) or (improper_integral_-infty (f,b)) + (improper_integral_+infty (f,b)) = +infty or (improper_integral_-infty (f,b)) + (improper_integral_+infty (f,b)) = -infty ) ; :: thesis:

end;

end;

end;

suppose A14: IL is divergent_in-infty_to-infty ; :: thesis:

then A15: improper_integral_-infty (f,b) = -infty by A1, A5, A6, Def3;

per cases by A10, A2, A8, A9, A14, A3, A1, A5, A6, Def3, Def4;

suppose IR is convergent_in+infty ; :: thesis:

then f is_+infty_ext_Riemann_integrable_on b by A2, A8, A9, INTEGR10:def 5;
then improper_integral_+infty (f,b) = infty_ext_right_integral (f,b) by A2, Th27;
then (improper_integral_-infty (f,b)) + (improper_integral_+infty (f,b)) = -infty by A15, XXREAL_3:def 2;
hence ex b being Real st
( ( improper_integral_-infty (f,b) = infty_ext_left_integral (f,b) & improper_integral_+infty (f,b) = infty_ext_right_integral (f,b) ) or (improper_integral_-infty (f,b)) + (improper_integral_+infty (f,b)) = +infty or (improper_integral_-infty (f,b)) + (improper_integral_+infty (f,b)) = -infty ) ; :: thesis:

end;

suppose IR is divergent_in+infty_to-infty ; :: thesis:

then improper_integral_+infty (f,b) = -infty by A2, A8, A9, Def4;
then (improper_integral_-infty (f,b)) + (improper_integral_+infty (f,b)) = -infty by A15, XXREAL_3:def 2;
hence ex b being Real st
( ( improper_integral_-infty (f,b) = infty_ext_left_integral (f,b) & improper_integral_+infty (f,b) = infty_ext_right_integral (f,b) ) or (improper_integral_-infty (f,b)) + (improper_integral_+infty (f,b)) = +infty or (improper_integral_-infty (f,b)) + (improper_integral_+infty (f,b)) = -infty ) ; :: thesis:

end;

end;

end;

end;