let f be PartFunc of REAL,REAL; :: thesis: for a, b being Real st a < b & [.a,b.[ c= dom f & f is_right_ext_Riemann_integrable_on a,b & abs f is_right_ext_Riemann_integrable_on a,b holds
max+ f is_right_ext_Riemann_integrable_on a,b
let a, b be Real; :: thesis: ( a < b & [.a,b.[ c= dom f & f is_right_ext_Riemann_integrable_on a,b & abs f is_right_ext_Riemann_integrable_on a,b implies max+ f is_right_ext_Riemann_integrable_on a,b )
assume that
A1: a < b and
A2: [.a,b.[ c= dom f and
A3: f is_right_ext_Riemann_integrable_on a,b and
A4: abs f is_right_ext_Riemann_integrable_on a,b ; :: thesis: max+ f is_right_ext_Riemann_integrable_on a,b
set G = ext_right_integral (f,a,b);
set AG = ext_right_integral ((abs f),a,b);
A5: for d being Real st a <= d & d < b holds
( f is_integrable_on ['a,d'] & f | ['a,d'] is bounded ) by A3, INTEGR10:def 1;
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,a,x) and
A8: I is_left_convergent_in b and
A9: ext_right_integral (f,a,b) = lim_left (I,b) by A3, INTEGR10:def 3;
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 and
A13: ext_right_integral ((abs f),a,b) = lim_left (AI,b) by A4, INTEGR10:def 3;
A14: for d being Real st a <= d & d < b holds
( max+ f is_integrable_on ['a,d'] & (max+ f) | ['a,d'] is bounded )

proof

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

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),a,x) ) & Intf is_left_convergent_in b )

proof

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

proof

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

end;

A25: for r being Real st r < b holds
ex g being Real st
( r < g & g < b & g in dom Intf ) by A6, A23, A8, LIMFUNC2:7;
for g1 being Real st 0 < g1 holds
ex r being Real st
( r < b & ( for r1 being Real st r < r1 & r1 < b & r1 in dom Intf holds
|.((Intf . r1) - (((ext_right_integral (f,a,b)) + (ext_right_integral ((abs f),a,b))) / 2)).| < g1 ) )

proof

let g1 be Real; :: thesis: ( 0 < g1 implies ex r being Real st
( r < b & ( for r1 being Real st r < r1 & r1 < b & r1 in dom Intf holds
|.((Intf . r1) - (((ext_right_integral (f,a,b)) + (ext_right_integral ((abs f),a,b))) / 2)).| < g1 ) ) )
assume A26: 0 < g1 ; :: thesis: ex r being Real st
( r < b & ( for r1 being Real st r < r1 & r1 < b & r1 in dom Intf holds
|.((Intf . r1) - (((ext_right_integral (f,a,b)) + (ext_right_integral ((abs f),a,b))) / 2)).| < g1 ) )
then consider R1 being Real such that
A27: ( R1 < b & ( for r1 being Real st R1 < r1 & r1 < b & r1 in dom I holds
|.((I . r1) - (ext_right_integral (f,a,b))).| < g1 ) ) by A8, A9, LIMFUNC2:41;
consider R2 being Real such that
A28: ( R2 < b & ( for r1 being Real st R2 < r1 & r1 < b & r1 in dom AI holds
|.((AI . r1) - (ext_right_integral ((abs f),a,b))).| < g1 ) ) by A12, A13, A26, LIMFUNC2:41;
set RR1 = max (a,R1);
set RR2 = max (a,R2);
take R = max ((max (a,R1)),(max (a,R2))); :: thesis: ( R < b & ( for r1 being Real st R < r1 & r1 < b & r1 in dom Intf holds
|.((Intf . r1) - (((ext_right_integral (f,a,b)) + (ext_right_integral ((abs f),a,b))) / 2)).| < g1 ) )
( max (a,R1) < b & max (a,R2) < b ) by A1, A27, A28, XXREAL_0:29;
hence R < b by XXREAL_0:29; :: thesis: for r1 being Real st R < r1 & r1 < b & r1 in dom Intf holds
|.((Intf . r1) - (((ext_right_integral (f,a,b)) + (ext_right_integral ((abs f),a,b))) / 2)).| < g1

hereby :: thesis: verum

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

end;

end;

hence ( dom Intf = [.a,b.[ & ( for x being Real st x in dom Intf holds
Intf . x = integral ((max+ f),a,x) ) & Intf is_left_convergent_in b ) by A24, A25, LIMFUNC2:7, FUNCT_2:def 1; :: thesis: verum

end;

hence max+ f is_right_ext_Riemann_integrable_on a,b by A14, INTEGR10:def 1; :: thesis: verum