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_left_improper_integrable_on a,b and
A4: abs f is_left_ext_Riemann_integrable_on a,b ; :: thesis:
abs f is_left_improper_integrable_on a,b by A4, INTEGR24:32;
then A5: left_improper_integral ((abs f),a,b) = ext_left_integral ((abs f),a,b) by A4, INTEGR24:34;
A6: for d being Real st a < d & d <= b holds
( f is_integrable_on ['d,b'] & f | ['d,b'] is bounded ) by A3, INTEGR24:def 1;
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,x,b) and
A9: ( I is_right_convergent_in a or I is_right_divergent_to+infty_in a or I is_right_divergent_to-infty_in a ) by A3, INTEGR24:def 1;
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),x,b) and
A12: AI is_right_convergent_in a by A4, INTEGR10: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 <= b ) by A14, A10, XXREAL_1:2;
then [.r1,b.] c= ].a,b.] by XXREAL_1:39;
then [.r1,b.] c= dom f by A2;
then A18: [.r1,b.] c= dom (abs f) by VALUED_1:def 11;
A19: ( a < r2 & r2 <= b ) by A15, A10, XXREAL_1:2;
[.r1,b.] = ['r1,b'] by A17, INTEGRA5:def 3;
then A20: ( abs f is_integrable_on ['r1,b'] & (abs f) | [.r1,b.] is bounded ) by A4, A17, INTEGR10:def 2;
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 A19, A18, A20, A21, Th14, MESFUNC6:55;
then AI . r1 >= integral ((abs f),r2,b) by A11, A14;
hence AI . r1 >= AI . r2 by A11, A15; :: thesis:

end;

A22: now :: thesis:

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

end;

hence f is_left_ext_Riemann_integrable_on a,b by A6, A7, A8, A9, A22, INTEGR10:def 2; :: 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) /\ ].a,(a + r).[ holds
I . g <= AI . g

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

end;

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