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_ext_Riemann_integrable_on a,b and
A4: abs f is_left_ext_Riemann_integrable_on a,b ; :: thesis:
set G = ext_left_integral (f,a,b);
set AG = ext_left_integral ((abs f),a,b);
A5: for d being Real st a < d & d <= b holds
( f is_integrable_on ['d,b'] & f | ['d,b'] is bounded ) by A3, INTEGR10:def 2;
consider I being PartFunc of REAL,REAL such that
A6: dom I = ].a,b.] and
A7: for x being Real st x in dom I holds
I . x = integral (f,x,b) and
A8: I is_right_convergent_in a and
A9: ext_left_integral (f,a,b) = lim_right (I,a) by A3, INTEGR10:def 4;
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 and
A13: ext_left_integral ((abs f),a,b) = lim_right (AI,a) by A4, INTEGR10:def 4;
A14: for d being Real st a < d & d <= b holds
( max+ f is_integrable_on ['d,b'] & (max+ f) | ['d,b'] is bounded )

let d be Real; :: thesis:
assume A15: ( a < d & d <= b ) ; :: thesis:
then A16: ( f is_integrable_on ['d,b'] & f | ['d,b'] is bounded ) by A3, INTEGR10:def 2;
A17: (f || ['d,b']) | ['d,b'] is bounded by A15, A3, INTEGR10:def 2;
['d,b'] = [.d,b.] by A15, INTEGRA5:def 3;
then ['d,b'] c= ].a,b.] by A15, XXREAL_1:39;
then A18: ['d,b'] c= dom f by A2;
then dom (f || ['d,b']) = ['d,b'] by RELAT_1:62;
then A19: f || ['d,b'] is Function of ['d,b'],REAL by FUNCT_2:67;
A20: max+ (f || ['d,b']) = max+ (f | ['d,b']) by A18, Th59
.= (max+ f) || ['d,b'] by MESFUNC6:66 ;
f || ['d,b'] is integrable by A5, A15, INTEGRA5:def 1;
hence max+ f is_integrable_on ['d,b'] by A20, A17, A19, INTEGRA4:20, INTEGRA5:def 1; :: thesis:
f | ['d,b'] is bounded_above by A16, SEQ_2:def 8;
then ( (max+ f) | ['d,b'] is bounded_above & (max+ f) | ['d,b'] is bounded_below ) by INTEGRA4:14, INTEGRA4:15;
hence (max+ f) | ['d,b'] is bounded by SEQ_2:def 8; :: thesis:

end;

ex Intf being PartFunc of REAL,REAL st
( dom Intf = ].a,b.] & ( for x being Real st x in dom Intf holds
Intf . x = integral ((max+ f),x,b) ) & Intf is_right_convergent_in a )

proof

reconsider A = ].a,b.] as non empty Subset of REAL by A1, XXREAL_1:32;
deffunc H₁( Element of A) -> Element of REAL = In ((integral ((max+ f),$1,b)),REAL);
consider Intf being Function of A,REAL such that
A21: for x being Element of A holds Intf . x = H₁(x) from FUNCT_2:sch 4();
A22: dom Intf = A by FUNCT_2:def 1;
then reconsider Intf = Intf as PartFunc of REAL,REAL by RELSET_1:5;
take Intf ; :: thesis:
A23: for x being Real st x in dom Intf holds
Intf . x = integral ((max+ f),x,b)

proof

let x be Real; :: thesis:
assume x in dom Intf ; :: thesis:
then x is Element of A by FUNCT_2:def 1;
then Intf . x = In ((integral ((max+ f),x,b)),REAL) by A21;
hence Intf . x = integral ((max+ f),x,b) ; :: thesis:

end;

A24: for r being Real st a < r holds
ex g being Real st
( g < r & a < g & g in dom Intf )

proof

let r be Real; :: thesis:
assume a < r ; :: thesis:
then consider g being Real such that
A25: ( g < r & a < g & g in dom I ) by A8, LIMFUNC2:10;
take g ; :: thesis:
thus ( g < r & a < g & g in dom Intf ) by A6, A25, FUNCT_2:def 1; :: thesis:

end;

for g1 being Real st 0 < g1 holds
ex r being Real st
( a < r & ( for r1 being Real st r1 < r & a < r1 & r1 in dom Intf holds
|.((Intf . r1) - (((ext_left_integral (f,a,b)) + (ext_left_integral ((abs f),a,b))) / 2)).| < g1 ) )

proof

let g1 be Real; :: thesis:
assume A26: 0 < g1 ; :: thesis:
then consider R1 being Real such that
A27: ( a < R1 & ( for r1 being Real st r1 < R1 & a < r1 & r1 in dom I holds
|.((I . r1) - (ext_left_integral (f,a,b))).| < g1 ) ) by A8, A9, LIMFUNC2:42;
consider R2 being Real such that
A28: ( a < R2 & ( for r1 being Real st r1 < R2 & a < r1 & r1 in dom AI holds
|.((AI . r1) - (ext_left_integral ((abs f),a,b))).| < g1 ) ) by A12, A13, A26, LIMFUNC2:42;
set RR1 = min (b,R1);
set RR2 = min (b,R2);
take R = min ((min (b,R1)),(min (b,R2))); :: thesis:
( a < min (b,R1) & a < min (b,R2) ) by A1, A27, A28, XXREAL_0:21;
hence a < R by XXREAL_0:21; :: thesis:

hereby :: thesis:

let r1 be Real; :: thesis:
assume A29: ( r1 < R & a < r1 & r1 in dom Intf ) ; :: thesis:
( b >= min (b,R1) & R1 >= min (b,R1) & R2 >= min (b,R2) & min (b,R1) >= R & min (b,R2) >= R ) by XXREAL_0:17;
then ( b >= R & R1 >= R & R2 >= R ) by XXREAL_0:2;
then A30: ( b > r1 & R1 > r1 & R2 > r1 ) by A29, XXREAL_0:2;
[.r1,b.] c= ].a,b.] by A29, XXREAL_1:39;
then A31: [.r1,b.] c= dom f by A2;
( f is_integrable_on ['r1,b'] & f | ['r1,b'] is bounded ) by A30, A29, A3, INTEGR10:def 2;
then 2 * (integral ((max+ f),r1,b)) = (integral (f,r1,b)) + (integral ((abs f),r1,b)) by A30, A31, Th62;
then 2 * (Intf . r1) = (integral (f,r1,b)) + (integral ((abs f),r1,b)) by A23, A29;
then 2 * (Intf . r1) = (I . r1) + (integral ((abs f),r1,b)) by A29, A22, A6, A7;
then 2 * (Intf . r1) = (I . r1) + (AI . r1) by A29, A22, A10, A11;
then (Intf . r1) - (((ext_left_integral (f,a,b)) + (ext_left_integral ((abs f),a,b))) / 2) = (((I . r1) - (ext_left_integral (f,a,b))) + ((AI . r1) - (ext_left_integral ((abs f),a,b)))) / 2 ;
then A32: |.((Intf . r1) - (((ext_left_integral (f,a,b)) + (ext_left_integral ((abs f),a,b))) / 2)).| = |.(((I . r1) - (ext_left_integral (f,a,b))) + ((AI . r1) - (ext_left_integral ((abs f),a,b)))).| / |.2.| by COMPLEX1:67
.= |.(((I . r1) - (ext_left_integral (f,a,b))) + ((AI . r1) - (ext_left_integral ((abs f),a,b)))).| / 2 by ABSVALUE:def 1 ;
A33: |.(((I . r1) - (ext_left_integral (f,a,b))) + ((AI . r1) - (ext_left_integral ((abs f),a,b)))).| <= |.((I . r1) - (ext_left_integral (f,a,b))).| + |.((AI . r1) - (ext_left_integral ((abs f),a,b))).| by COMPLEX1:56;
( |.((I . r1) - (ext_left_integral (f,a,b))).| < g1 & |.((AI . r1) - (ext_left_integral ((abs f),a,b))).| < g1 ) by A6, A10, A22, A27, A28, A30, A29;
then |.((I . r1) - (ext_left_integral (f,a,b))).| + |.((AI . r1) - (ext_left_integral ((abs f),a,b))).| < g1 + g1 by XREAL_1:8;
then |.(((I . r1) - (ext_left_integral (f,a,b))) + ((AI . r1) - (ext_left_integral ((abs f),a,b)))).| < 2 * g1 by A33, XXREAL_0:2;
then |.((Intf . r1) - (((ext_left_integral (f,a,b)) + (ext_left_integral ((abs f),a,b))) / 2)).| < (2 * g1) / 2 by A32, XREAL_1:74;
hence |.((Intf . r1) - (((ext_left_integral (f,a,b)) + (ext_left_integral ((abs f),a,b))) / 2)).| < g1 ; :: thesis:

end;

hence ( dom Intf = ].a,b.] & ( for x being Real st x in dom Intf holds
Intf . x = integral ((max+ f),x,b) ) & Intf is_right_convergent_in a ) by A23, A24, FUNCT_2:def 1, LIMFUNC2:10; :: thesis:

end;

hence max+ f is_left_ext_Riemann_integrable_on a,b by A14, INTEGR10:def 2; :: thesis: