let f be PartFunc of REAL,REAL; :: thesis: for a being Real st right_closed_halfline a c= dom f & f is_+infty_ext_Riemann_integrable_on a & abs f is_+infty_ext_Riemann_integrable_on a holds
max+ f is_+infty_ext_Riemann_integrable_on a
let a be Real; :: thesis: ( right_closed_halfline a c= dom f & f is_+infty_ext_Riemann_integrable_on a & abs f is_+infty_ext_Riemann_integrable_on a implies max+ f is_+infty_ext_Riemann_integrable_on a )
assume that
A1: right_closed_halfline a c= dom f and
A2: f is_+infty_ext_Riemann_integrable_on a and
A3: abs f is_+infty_ext_Riemann_integrable_on a ; :: thesis: max+ f is_+infty_ext_Riemann_integrable_on a
A4: a in REAL by XREAL_0:def 1;
A5: right_closed_halfline a = [.a,+infty.[ by LIMFUNC1:def 2;
set G = infty_ext_right_integral (f,a);
set AG = infty_ext_right_integral ((abs f),a);
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 and
A9: infty_ext_right_integral (f,a) = lim_in+infty I by A2, INTEGR10:def 7;
consider AI being PartFunc of REAL,REAL such that
A10: dom AI = right_closed_halfline a and
A11: for x being Real st x in dom AI holds
AI . x = integral ((abs f),a,x) and
A12: AI is convergent_in+infty and
A13: infty_ext_right_integral ((abs f),a) = lim_in+infty AI by A3, INTEGR10:def 7;
A14: for d being Real st a <= d holds
( max+ f is_integrable_on ['a,d'] & (max+ f) | ['a,d'] is bounded )

proof

let d be Real; :: thesis: ( a <= d implies ( max+ f is_integrable_on ['a,d'] & (max+ f) | ['a,d'] is bounded ) )
assume A15: a <= d ; :: 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 A2, INTEGR10:def 5;
A17: (f || ['a,d']) | ['a,d'] is bounded by A15, A2, INTEGR10:def 5;
A18: d in REAL by XREAL_0:def 1;
['a,d'] = [.a,d.] by A15, INTEGRA5:def 3;
then ['a,d'] c= [.a,+infty.[ by A18, XXREAL_0:9, XXREAL_1:43;
then A19: ['a,d'] c= dom f by A1, A5;
then A20: dom (f || ['a,d']) = ['a,d'] by RELAT_1:62;
A21: max+ (f || ['a,d']) = max+ (f | ['a,d']) by A19, Th59
.= (max+ f) || ['a,d'] by MESFUNC6:66 ;
A22: f || ['a,d'] is Function of ['a,d'],REAL by A20, FUNCT_2:67;
f || ['a,d'] is integrable by A15, A2, INTEGR10:def 5, INTEGRA5:def 1;
hence max+ f is_integrable_on ['a,d'] by A21, A17, A22, 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 = right_closed_halfline a & ( for x being Real st x in dom Intf holds
Intf . x = integral ((max+ f),a,x) ) & Intf is convergent_in+infty )

proof

reconsider A = [.a,+infty.[ as non empty Subset of REAL by A4, XXREAL_0:9, 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
A23: for x being Element of A holds Intf . x = H₁(x) from FUNCT_2:sch 4();
A24: 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 = right_closed_halfline a & ( for x being Real st x in dom Intf holds
Intf . x = integral ((max+ f),a,x) ) & Intf is convergent_in+infty )
A25: 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 A23;
hence Intf . x = integral ((max+ f),a,x) ; :: thesis: verum

end;

A26: for r being Real ex g being Real st
( r < g & g in dom Intf ) by A5, A6, A8, A24, LIMFUNC1:44;
for g1 being Real st 0 < g1 holds
ex r being Real st
for r1 being Real st r < r1 & r1 in dom Intf holds
|.((Intf . r1) - (((infty_ext_right_integral (f,a)) + (infty_ext_right_integral ((abs f),a))) / 2)).| < g1

proof

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

hereby :: thesis: verum

let r1 be Real; :: thesis: ( R < r1 & r1 in dom Intf implies |.((Intf . r1) - (((infty_ext_right_integral (f,a)) + (infty_ext_right_integral ((abs f),a))) / 2)).| < g1 )
assume A30: ( R < r1 & r1 in dom Intf ) ; :: thesis: |.((Intf . r1) - (((infty_ext_right_integral (f,a)) + (infty_ext_right_integral ((abs f),a))) / 2)).| < g1
A31: r1 in REAL by XREAL_0:def 1;
( 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 A32: ( a < r1 & R1 < r1 & R2 < r1 ) by A30, XXREAL_0:2;
[.a,r1.] c= [.a,+infty.[ by A31, XXREAL_0:9, XXREAL_1:43;
then A33: [.a,r1.] c= dom f by A1, A5;
( f is_integrable_on ['a,r1'] & f | ['a,r1'] is bounded ) by A32, A2, INTEGR10:def 5;
then 2 * (integral ((max+ f),a,r1)) = (integral (f,a,r1)) + (integral ((abs f),a,r1)) by A32, A33, Th62;
then 2 * (Intf . r1) = (integral (f,a,r1)) + (integral ((abs f),a,r1)) by A25, A30;
then 2 * (Intf . r1) = (I . r1) + (integral ((abs f),a,r1)) by A5, A30, A24, A6, A7;
then 2 * (Intf . r1) = (I . r1) + (AI . r1) by A5, A30, A24, A10, A11;
then (Intf . r1) - (((infty_ext_right_integral (f,a)) + (infty_ext_right_integral ((abs f),a))) / 2) = (((I . r1) - (infty_ext_right_integral (f,a))) + ((AI . r1) - (infty_ext_right_integral ((abs f),a)))) / 2 ;
then A34: |.((Intf . r1) - (((infty_ext_right_integral (f,a)) + (infty_ext_right_integral ((abs f),a))) / 2)).| = |.(((I . r1) - (infty_ext_right_integral (f,a))) + ((AI . r1) - (infty_ext_right_integral ((abs f),a)))).| / |.2.| by COMPLEX1:67
.= |.(((I . r1) - (infty_ext_right_integral (f,a))) + ((AI . r1) - (infty_ext_right_integral ((abs f),a)))).| / 2 by ABSVALUE:def 1 ;
A35: |.(((I . r1) - (infty_ext_right_integral (f,a))) + ((AI . r1) - (infty_ext_right_integral ((abs f),a)))).| <= |.((I . r1) - (infty_ext_right_integral (f,a))).| + |.((AI . r1) - (infty_ext_right_integral ((abs f),a))).| by COMPLEX1:56;
( |.((I . r1) - (infty_ext_right_integral (f,a))).| < g1 & |.((AI . r1) - (infty_ext_right_integral ((abs f),a))).| < g1 ) by A5, A6, A10, A24, A28, A29, A32, A30;
then |.((I . r1) - (infty_ext_right_integral (f,a))).| + |.((AI . r1) - (infty_ext_right_integral ((abs f),a))).| < g1 + g1 by XREAL_1:8;
then |.(((I . r1) - (infty_ext_right_integral (f,a))) + ((AI . r1) - (infty_ext_right_integral ((abs f),a)))).| < 2 * g1 by A35, XXREAL_0:2;
then |.((Intf . r1) - (((infty_ext_right_integral (f,a)) + (infty_ext_right_integral ((abs f),a))) / 2)).| < (2 * g1) / 2 by A34, XREAL_1:74;
hence |.((Intf . r1) - (((infty_ext_right_integral (f,a)) + (infty_ext_right_integral ((abs f),a))) / 2)).| < g1 ; :: thesis: verum

end;

end;

hence ( dom Intf = right_closed_halfline a & ( for x being Real st x in dom Intf holds
Intf . x = integral ((max+ f),a,x) ) & Intf is convergent_in+infty ) by A5, A25, A26, LIMFUNC1:44, FUNCT_2:def 1; :: thesis: verum

end;

hence max+ f is_+infty_ext_Riemann_integrable_on a by A14, INTEGR10:def 5; :: thesis: verum