let f be PartFunc of REAL,REAL; :: thesis:
let b be Real; :: thesis:
assume that
A1: left_closed_halfline b c= dom f and
A2: f is_-infty_improper_integrable_on b and
A3: abs f is_-infty_ext_Riemann_integrable_on b ; :: thesis:
abs f is_-infty_improper_integrable_on b by A3, INTEGR25:20;
then A4: improper_integral_-infty ((abs f),b) = infty_ext_left_integral ((abs f),b) by A3, INTEGR25:22;
A5: for a being Real st a <= b holds
( f is_integrable_on ['a,b'] & f | ['a,b'] is bounded ) by A2, INTEGR25:def 1;
consider I being PartFunc of REAL,REAL such that
A6: dom I = left_closed_halfline b and
A7: for x being Real st x in dom I holds
I . x = integral (f,x,b) and
A8: ( I is convergent_in-infty or I is divergent_in-infty_to+infty or I is divergent_in-infty_to-infty ) by A2, INTEGR25:def 1;
consider AI being PartFunc of REAL,REAL such that
A9: dom AI = left_closed_halfline b and
A10: for x being Real st x in dom AI holds
AI . x = integral ((abs f),x,b) and
A11: AI is convergent_in-infty by A3, INTEGR10:def 6;
A12: left_closed_halfline b = ].-infty,b.] by LIMFUNC1:def 1;
A13: for r1, r2 being Real st r1 in dom AI & r2 in dom AI & r1 < r2 holds
AI . r1 >= AI . r2

let r1, r2 be Real; :: thesis:
assume that
A14: r1 in dom AI and
A15: r2 in dom AI and
A16: r1 < r2 ; :: thesis:
A17: ( -infty < r2 & r2 <= b ) by A12, A15, A9, XXREAL_1:2;
A18: ( -infty < r1 & r1 <= b ) by A12, A14, A9, XXREAL_1:2;
then [.r1,b.] c= ].-infty,b.] by XXREAL_1:39;
then [.r1,b.] c= dom f by A12, A1;
then A19: [.r1,b.] c= dom (abs f) by VALUED_1:def 11;
[.r1,b.] = ['r1,b'] by A18, INTEGRA5:def 3;
then A20: ( abs f is_integrable_on ['r1,b'] & (abs f) | [.r1,b.] is bounded ) by A18, A3, INTEGR10:def 6;
A21: [.r2,b.] c= [.r1,b.] by A16, XXREAL_1:34;
f is Relation of REAL,COMPLEX by RELSET_1:7, NUMBERS:11;
then integral ((abs f),r1,b) >= integral ((abs f),r2,b) by A17, A19, A20, A21, Th14, MESFUNC6:55;
then AI . r1 >= integral ((abs f),r2,b) by A10, A14;
hence AI . r1 >= AI . r2 by A10, A15; :: thesis:

end;

A22: now :: thesis:

assume A23: I is divergent_in-infty_to+infty ; :: thesis:
then consider R being Real such that
A24: for r1 being Real st r1 < R & r1 in dom I holds
lim_in-infty AI < I . r1 by LIMFUNC1:48;
consider R1 being Real such that
A25: ( R1 < R & R1 in dom I ) by A23, LIMFUNC1:48;
A26: ( -infty < R1 & R1 <= b ) by A12, A6, A25, XXREAL_1:2;
then [.R1,b.] = ['R1,b'] by INTEGRA5:def 3;
then ['R1,b'] c= ].-infty,b.] by A26, XXREAL_1:39;
then A27: ['R1,b'] c= dom f by A1, A12;
( f is_integrable_on ['R1,b'] & f | ['R1,b'] is bounded ) by A26, A2, INTEGR25:def 1;
then |.(integral (f,R1,b)).| <= integral ((abs f),R1,b) by A26, A27, INTEGRA6:8;
then |.(I . R1).| <= integral ((abs f),R1,b) by A25, A7;
then A28: |.(I . R1).| <= AI . R1 by A25, A6, A9, A10;
AI . R1 <= lim_in-infty AI by A13, A25, A9, A6, A11, Th10, RFUNCT_2:def 4;
then A29: |.(I . R1).| <= lim_in-infty AI by A28, XXREAL_0:2;
A30: lim_in-infty AI < I . R1 by A24, A25;
I . R1 <= |.(I . R1).| by COMPLEX1:76;
hence contradiction by A29, A30, XXREAL_0:2; :: thesis:

end;

A31: now :: thesis:

assume A32: I is divergent_in-infty_to-infty ; :: thesis:
then consider R being Real such that
A33: for r1 being Real st r1 < R & r1 in dom I holds
I . r1 < - (lim_in-infty AI) by LIMFUNC1:49;
consider R1 being Real such that
A34: ( R1 < R & R1 in dom I ) by A32, LIMFUNC1:49;
A35: ( -infty < R1 & R1 <= b ) by A12, A6, A34, XXREAL_1:2;
then [.R1,b.] = ['R1,b'] by INTEGRA5:def 3;
then ['R1,b'] c= ].-infty,b.] by A35, XXREAL_1:39;
then A36: ['R1,b'] c= dom f by A1, A12;
( f is_integrable_on ['R1,b'] & f | ['R1,b'] is bounded ) by A35, A2, INTEGR25:def 1;
then |.(integral (f,R1,b)).| <= integral ((abs f),R1,b) by A35, A36, INTEGRA6:8;
then |.(I . R1).| <= integral ((abs f),R1,b) by A34, A7;
then A37: |.(I . R1).| <= AI . R1 by A34, A6, A9, A10;
AI . R1 <= lim_in-infty AI by A13, A34, A9, A6, A11, Th10, RFUNCT_2:def 4;
then A38: |.(I . R1).| <= lim_in-infty AI by A37, XXREAL_0:2;
A39: I . R1 < - (lim_in-infty AI) by A33, A34;
- |.(I . R1).| <= I . R1 by COMPLEX1:76;
then - |.(I . R1).| < - (lim_in-infty AI) by A39, XXREAL_0:2;
hence contradiction by A38, XREAL_1:24; :: thesis:

end;

hence f is_-infty_ext_Riemann_integrable_on b by A5, A6, A7, A8, A22, INTEGR10:def 6; :: thesis:
for g being Real st g in (dom I) /\ (left_open_halfline 1) holds
I . g <= AI . g

let g be Real; :: thesis:
assume g in (dom I) /\ (left_open_halfline 1) ; :: thesis:
then A40: g in dom I by XBOOLE_0:def 4;
then I . g = integral (f,g,b) by A7;
then A41: I . g <= |.(integral (f,g,b)).| by COMPLEX1:76;
A42: ( -infty < g & g <= b ) by A12, A40, A6, XXREAL_1:2;
then [.g,b.] = ['g,b'] by INTEGRA5:def 3;
then ['g,b'] c= ].-infty,b.] by A42, XXREAL_1:39;
then A43: ['g,b'] c= dom f by A1, A12;
( f is_integrable_on ['g,b'] & f | ['g,b'] is bounded ) by A42, A2, INTEGR25:def 1;
then |.(integral (f,g,b)).| <= integral ((abs f),g,b) by A42, A43, INTEGRA6:8;
then |.(integral (f,g,b)).| <= AI . g by A40, A6, A9, A10;
hence I . g <= AI . g by A41, XXREAL_0:2; :: thesis:

end;

then lim_in-infty I <= lim_in-infty AI by A11, A8, A22, A31, A6, A9, LIMFUNC1:105;
then improper_integral_-infty (f,b) <= lim_in-infty AI by A2, A6, A7, A8, A22, A31, INTEGR25:24;
hence improper_integral_-infty (f,b) <= improper_integral_-infty ((abs f),b) by A4, A3, A9, A10, A11, INTEGR10:def 8; :: thesis:
thus improper_integral_-infty ((abs f),b) < +infty by A4, XREAL_0:def 1, XXREAL_0:9; :: thesis: