let f be PartFunc of REAL,REAL; :: thesis:
let a, b be Real; :: thesis:
assume that
A1: a < b and
A2: [.a,b.[ c= dom f and
A3: f is_right_improper_integrable_on a,b and
A4: abs f is_right_ext_Riemann_integrable_on a,b ; :: thesis:
abs f is_right_improper_integrable_on a,b by A4, INTEGR24:33;
then A5: right_improper_integral ((abs f),a,b) = ext_right_integral ((abs f),a,b) by A4, INTEGR24:39;
A6: for d being Real st a <= d & d < b holds
( f is_integrable_on ['a,d'] & f | ['a,d'] is bounded ) by A3, INTEGR24:def 2;
consider I being PartFunc of REAL,REAL such that
A7: dom I = [.a,b.[ and
A8: for x being Real st x in dom I holds
I . x = integral (f,a,x) and
A9: ( I is_left_convergent_in b or I is_left_divergent_to+infty_in b or I is_left_divergent_to-infty_in b ) by A3, INTEGR24:def 2;
consider AI being PartFunc of REAL,REAL such that
A10: dom AI = [.a,b.[ and
A11: for x being Real st x in dom AI holds
AI . x = integral ((abs f),a,x) and
A12: AI is_left_convergent_in b by A4, INTEGR10: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: a <= r1 by A14, A10, XXREAL_1:3;
A18: ( a <= r2 & r2 < b ) by A15, A10, XXREAL_1:3;
then [.a,r2.] c= [.a,b.[ by XXREAL_1:43;
then [.a,r2.] c= dom f by A2;
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, A4, INTEGR10:def 1;
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,r1) <= integral ((abs f),a,r2) by A19, A20, A21, A17, Th14, MESFUNC6:55;
then AI . r1 <= integral ((abs f),a,r2) by A11, A14;
hence AI . r1 <= AI . r2 by A11, A15; :: thesis:

end;

A22: now :: thesis:

assume A23: I is_left_divergent_to+infty_in b ; :: thesis:
then consider R being Real such that
A24: ( R < b & ( for r1 being Real st R < r1 & r1 < b & r1 in dom I holds
lim_left (AI,b) < I . r1 ) ) by LIMFUNC2:8;
consider R1 being Real such that
A25: ( R < R1 & R1 < b & R1 in dom I ) by A24, A23, LIMFUNC2:8;
A26: ( a <= R1 & R1 < b ) by A7, A25, XXREAL_1:3;
then [.a,R1.] = ['a,R1'] by INTEGRA5:def 3;
then ['a,R1'] c= [.a,b.[ by A25, XXREAL_1:43;
then A27: ['a,R1'] c= dom f by A2;
( f is_integrable_on ['a,R1'] & f | ['a,R1'] is bounded ) by A26, A3, INTEGR24: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, A8;
then A28: |.(I . R1).| <= AI . R1 by A25, A7, A10, A11;
AI . R1 <= lim_left (AI,b) by A13, A25, A10, A7, A12, Th6, RFUNCT_2:def 3;
then A29: |.(I . R1).| <= lim_left (AI,b) by A28, XXREAL_0:2;
A30: lim_left (AI,b) < 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_left_divergent_to-infty_in b ; :: thesis:
then consider R being Real such that
A33: ( R < b & ( for r1 being Real st R < r1 & r1 < b & r1 in dom I holds
I . r1 < - (lim_left (AI,b)) ) ) by LIMFUNC2:9;
consider R1 being Real such that
A34: ( R < R1 & R1 < b & R1 in dom I ) by A33, A32, LIMFUNC2:9;
A35: ( a <= R1 & R1 < b ) by A7, A34, XXREAL_1:3;
then [.a,R1.] = ['a,R1'] by INTEGRA5:def 3;
then ['a,R1'] c= [.a,b.[ by A34, XXREAL_1:43;
then A36: ['a,R1'] c= dom f by A2;
( f is_integrable_on ['a,R1'] & f | ['a,R1'] is bounded ) by A35, A3, INTEGR24: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, A8;
then A37: |.(I . R1).| <= AI . R1 by A34, A7, A10, A11;
AI . R1 <= lim_left (AI,b) by A13, A34, A10, A7, A12, Th6, RFUNCT_2:def 3;
then A38: |.(I . R1).| <= lim_left (AI,b) by A37, XXREAL_0:2;
A39: I . R1 < - (lim_left (AI,b)) by A33, A34;
- |.(I . R1).| <= I . R1 by COMPLEX1:76;
then - |.(I . R1).| < - (lim_left (AI,b)) by A39, XXREAL_0:2;
hence contradiction by A38, XREAL_1:24; :: thesis:

end;

hence f is_right_ext_Riemann_integrable_on a,b by A6, A7, A8, A9, A22, INTEGR10:def 1; :: thesis:
consider r being Real such that
A40: ( 0 < r & r < b - a ) by A1, XREAL_1:5, XREAL_1:50;
for g being Real st g in (dom I) /\ ].(b - r),b.[ holds
I . g <= AI . g

let g be Real; :: thesis:
assume g in (dom I) /\ ].(b - r),b.[ ; :: thesis:
then A41: g in dom I by XBOOLE_0:def 4;
then I . g = integral (f,a,g) by A8;
then A42: I . g <= |.(integral (f,a,g)).| by COMPLEX1:76;
A43: ( a <= g & g < b ) by A41, A7, XXREAL_1:3;
then [.a,g.] = ['a,g'] by INTEGRA5:def 3;
then ['a,g'] c= [.a,b.[ by A43, XXREAL_1:43;
then A44: ['a,g'] c= dom f by A2;
( f is_integrable_on ['a,g'] & f | ['a,g'] is bounded ) by A43, A3, INTEGR24:def 2;
then |.(integral (f,a,g)).| <= integral ((abs f),a,g) by A43, A44, INTEGRA6:8;
then |.(integral (f,a,g)).| <= AI . g by A41, A7, A10, A11;
hence I . g <= AI . g by A42, XXREAL_0:2; :: thesis:

end;

then lim_left (I,b) <= lim_left (AI,b) by A9, A22, A31, A7, A10, A12, A40, LIMFUNC2:67;
then right_improper_integral (f,a,b) <= lim_left (AI,b) by A3, A7, A8, A9, A22, A31, INTEGR24:41;
hence right_improper_integral (f,a,b) <= right_improper_integral ((abs f),a,b) by A5, A4, A10, A11, A12, INTEGR10:def 3; :: thesis:
thus right_improper_integral ((abs f),a,b) < +infty by A5, XREAL_0:def 1, XXREAL_0:9; :: thesis: