let f be PartFunc of REAL,REAL; :: thesis:
let a be Real; :: thesis:
assume that
A1: right_closed_halfline a c= dom f and
A2: f is_+infty_improper_integrable_on a and
A3: abs f is_+infty_ext_Riemann_integrable_on a ; :: thesis:
abs f is_+infty_improper_integrable_on a by A3, INTEGR25:21;
then A4: improper_integral_+infty ((abs f),a) = infty_ext_right_integral ((abs f),a) by A3, INTEGR25:27;
A5: for d being Real st a <= d holds
( f is_integrable_on ['a,d'] & f | ['a,d'] is bounded ) by A2, INTEGR25:def 2;
consider I being PartFunc of REAL,REAL such that
A6: dom I = right_closed_halfline a and
A7: for x being Real st x in dom I holds
I . x = integral (f,a,x) 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 2;
consider AI being PartFunc of REAL,REAL such that
A9: dom AI = right_closed_halfline a and
A10: for x being Real st x in dom AI holds
AI . x = integral ((abs f),a,x) and
A11: AI is convergent_in+infty by A3, INTEGR10:def 5;
A12: right_closed_halfline a = [.a,+infty.[ by LIMFUNC1:def 2;
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: ( a <= r1 & r1 < +infty ) by A12, A14, A9, XXREAL_1:3;
A18: ( a <= r2 & r2 < +infty ) by A12, A15, A9, XXREAL_1:3;
then [.a,r2.] c= [.a,+infty.[ by XXREAL_1:43;
then [.a,r2.] c= dom f by A12, A1;
then A19: [.a,r2.] c= dom (abs f) by VALUED_1:def 11;
[.a,r2.] = ['a,r2'] by A18, INTEGRA5:def 3;
then A20: ( abs f is_integrable_on ['a,r2'] & (abs f) | [.a,r2.] is bounded ) by A18, A3, INTEGR10:def 5;
A21: [.a,r1.] c= [.a,r2.] by A16, XXREAL_1:34;
f is Relation of REAL,COMPLEX by RELSET_1:7, NUMBERS:11;
then integral ((abs f),a,r2) >= integral ((abs f),a,r1) by A19, A20, A21, A17, Th14, MESFUNC6:55;
then AI . r2 >= integral ((abs f),a,r1) by A10, A15;
hence AI . r2 >= AI . r1 by A14, A10; :: 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 R < r1 & r1 in dom I holds
lim_in+infty AI < I . r1 by LIMFUNC1:46;
consider R1 being Real such that
A25: ( R < R1 & R1 in dom I ) by A23, LIMFUNC1:46;
A26: ( a <= R1 & R1 < +infty ) by A12, A6, A25, XXREAL_1:3;
then [.a,R1.] = ['a,R1'] by INTEGRA5:def 3;
then ['a,R1'] c= [.a,+infty.[ by A26, XXREAL_1:43;
then A27: ['a,R1'] c= dom f by A1, A12;
( f is_integrable_on ['a,R1'] & f | ['a,R1'] is bounded ) by A26, A2, INTEGR25:def 2;
then |.(integral (f,a,R1)).| <= integral ((abs f),a,R1) by A26, A27, INTEGRA6:8;
then |.(I . R1).| <= integral ((abs f),a,R1) 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, Th11, RFUNCT_2:def 3;
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 R < r1 & r1 in dom I holds
I . r1 < - (lim_in+infty AI) by LIMFUNC1:47;
consider R1 being Real such that
A34: ( R < R1 & R1 in dom I ) by A32, LIMFUNC1:47;
A35: ( a <= R1 & R1 < +infty ) by A12, A6, A34, XXREAL_1:3;
then [.a,R1.] = ['a,R1'] by INTEGRA5:def 3;
then ['a,R1'] c= [.a,+infty.[ by A35, XXREAL_1:43;
then A36: ['a,R1'] c= dom f by A1, A12;
( f is_integrable_on ['a,R1'] & f | ['a,R1'] is bounded ) by A35, A2, INTEGR25:def 2;
then |.(integral (f,a,R1)).| <= integral ((abs f),a,R1) by A35, A36, INTEGRA6:8;
then |.(I . R1).| <= integral ((abs f),a,R1) 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, Th11, RFUNCT_2:def 3;
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 a by A5, A6, A7, A8, A22, INTEGR10:def 5; :: thesis:
for g being Real st g in (dom I) /\ (right_open_halfline 1) holds
I . g <= AI . g

let g be Real; :: thesis:
assume g in (dom I) /\ (right_open_halfline 1) ; :: thesis:
then A40: g in dom I by XBOOLE_0:def 4;
then I . g = integral (f,a,g) by A7;
then A41: I . g <= |.(integral (f,a,g)).| by COMPLEX1:76;
A42: ( a <= g & g < +infty ) by A12, A40, A6, XXREAL_1:3;
then [.a,g.] = ['a,g'] by INTEGRA5:def 3;
then ['a,g'] c= [.a,+infty.[ by A42, XXREAL_1:43;
then A43: ['a,g'] c= dom f by A1, A12;
( f is_integrable_on ['a,g'] & f | ['a,g'] is bounded ) by A42, A2, INTEGR25:def 2;
then |.(integral (f,a,g)).| <= integral ((abs f),a,g) by A42, A43, INTEGRA6:8;
then |.(integral (f,a,g)).| <= 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:104;
then improper_integral_+infty (f,a) <= lim_in+infty AI by A2, A6, A7, A8, A22, A31, INTEGR25:29;
hence improper_integral_+infty (f,a) <= improper_integral_+infty ((abs f),a) by A4, A3, A9, A10, A11, INTEGR10:def 7; :: thesis:
thus improper_integral_+infty ((abs f),a) < +infty by A4, XREAL_0:def 1, XXREAL_0:9; :: thesis: