let f, g 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: [.a,b.[ c= dom g and
A4: f is_right_improper_integrable_on a,b and
A5: g is_right_improper_integrable_on a,b and
A6: ( not right_improper_integral (f,a,b) = +infty or not right_improper_integral (g,a,b) = -infty ) and
A7: ( not right_improper_integral (f,a,b) = -infty or not right_improper_integral (g,a,b) = +infty ) ; :: thesis:
A8: for d being Real st a <= d & d < b holds
( f + g is_integrable_on ['a,d'] & (f + g) | ['a,d'] is bounded )

proof

let d be Real; :: thesis:
assume A9: ( a <= d & d < b ) ; :: thesis:
then A10: ( f is_integrable_on ['a,d'] & f | ['a,d'] is bounded & g is_integrable_on ['a,d'] & g | ['a,d'] is bounded ) by A4, A5;
[.a,d.] c= [.a,b.[ by A9, XXREAL_1:43;
then ['a,d'] c= [.a,b.[ by A9, INTEGRA5:def 3;
then ( ['a,d'] c= dom f & ['a,d'] c= dom g ) by A2, A3;
hence f + g is_integrable_on ['a,d'] by A10, INTEGRA6:11; :: thesis:
(f + g) | (['a,d'] /\ ['a,d']) is bounded by A10, RFUNCT_1:83;
hence (f + g) | ['a,d'] is bounded ; :: thesis:

end;

per cases ;

suppose A11: ( f is_right_ext_Riemann_integrable_on a,b & g is_right_ext_Riemann_integrable_on a,b ) ; :: thesis:

then A12: ( right_improper_integral (f,a,b) = ext_right_integral (f,a,b) & right_improper_integral (g,a,b) = ext_right_integral (g,a,b) ) by A4, A5, Th39;
A13: ( f + g is_right_ext_Riemann_integrable_on a,b & ext_right_integral ((f + g),a,b) = (ext_right_integral (f,a,b)) + (ext_right_integral (g,a,b)) ) by A1, A2, A3, A11, Th29;
thus f + g is_right_improper_integrable_on a,b by A1, A2, A3, A11, Th29, Th33; :: thesis:
then right_improper_integral ((f + g),a,b) = ext_right_integral ((f + g),a,b) by A13, Th39;
hence right_improper_integral ((f + g),a,b) = (right_improper_integral (f,a,b)) + (right_improper_integral (g,a,b)) by A12, A13, XXREAL_3:def 2; :: thesis:

end;

suppose A14: ( f is_right_ext_Riemann_integrable_on a,b & not g is_right_ext_Riemann_integrable_on a,b ) ; :: thesis:

then A15: right_improper_integral (f,a,b) = ext_right_integral (f,a,b) by A4, Th39;
consider Intf being PartFunc of REAL,REAL such that
A16: dom Intf = [.a,b.[ and
A17: for x being Real st x in dom Intf holds
Intf . x = integral (f,a,x) and
A18: Intf is_left_convergent_in b by A14, INTEGR10:def 1;
consider Intg being PartFunc of REAL,REAL such that
A19: dom Intg = [.a,b.[ and
A20: for x being Real st x in dom Intg holds
Intg . x = integral (g,a,x) and
( Intg is_left_convergent_in b or Intg is_left_divergent_to+infty_in b or Intg is_left_divergent_to-infty_in b ) by A5;
A21: dom (Intf + Intg) = [.a,b.[ /\ [.a,b.[ by A16, A19, VALUED_1:def 1
.= [.a,b.[ ;
A22: for x being Real st x in dom (Intf + Intg) holds
(Intf + Intg) . x = integral ((f + g),a,x)

proof

let x be Real; :: thesis:
assume A23: x in dom (Intf + Intg) ; :: thesis:
then A24: ( a <= x & x < b ) by A21, XXREAL_1:3;
then [.a,x.] c= [.a,b.[ by XXREAL_1:43;
then A25: ( [.a,x.] c= dom f & [.a,x.] c= dom g ) by A2, A3;
A26: ['a,x'] = [.a,x.] by A24, INTEGRA5:def 3;
( f is_integrable_on ['a,x'] & f | ['a,x'] is bounded & g is_integrable_on ['a,x'] & g | ['a,x'] is bounded ) by A4, A5, A24;
then integral ((f + g),['a,x']) = (integral (f,['a,x'])) + (integral (g,['a,x'])) by A25, A26, INTEGRA6:11;
then A27: integral ((f + g),a,x) = (integral (f,['a,x'])) + (integral (g,['a,x'])) by A24, INTEGRA5:def 4
.= (integral (f,a,x)) + (integral (g,['a,x'])) by A24, INTEGRA5:def 4
.= (integral (f,a,x)) + (integral (g,a,x)) by A24, INTEGRA5:def 4 ;
(Intf + Intg) . x = (Intf . x) + (Intg . x) by A23, VALUED_1:def 1
.= (integral (f,a,x)) + (Intg . x) by A23, A21, A16, A17
.= (integral (f,a,x)) + (integral (g,a,x)) by A23, A21, A19, A20 ;
hence (Intf + Intg) . x = integral ((f + g),a,x) by A27; :: thesis:

end;

A28: for r being Real st r < b holds
ex g being Real st
( r < g & g < b & g in dom (Intf + Intg) )

proof

let r be Real; :: thesis:
assume r < b ; :: thesis:
then consider g being Real such that
A29: ( max (a,r) < g & g < b ) by A1, XXREAL_0:29, XREAL_1:5;
take g ; :: thesis:
( max (a,r) >= a & max (a,r) >= r ) by XXREAL_0:25;
then ( r < g & a < g ) by A29, XXREAL_0:2;
hence ( r < g & g < b & g in dom (Intf + Intg) ) by A29, A21, XXREAL_1:3; :: thesis:

end;

A30: ( ex r being Real st
( 0 < r & Intf | ].(b - r),b.[ is bounded_below ) & ex r being Real st
( 0 < r & Intf | ].(b - r),b.[ is bounded_above ) ) by A18, Th11;

per cases by A5, A14, Th39;

suppose A31: right_improper_integral (g,a,b) = +infty ; :: thesis:

then A32: Intf + Intg is_left_divergent_to+infty_in b by A28, A5, A19, A20, A30, Th51, LIMFUNC2:17;
hence f + g is_right_improper_integrable_on a,b by A8, A21, A22; :: thesis:
then right_improper_integral ((f + g),a,b) = +infty by A21, A22, A32, Def4;
hence right_improper_integral ((f + g),a,b) = (right_improper_integral (f,a,b)) + (right_improper_integral (g,a,b)) by A15, A31, XXREAL_3:def 2; :: thesis:

end;

suppose A33: right_improper_integral (g,a,b) = -infty ; :: thesis:

then A34: Intf + Intg is_left_divergent_to-infty_in b by A28, A5, A19, A20, A30, Th52, Th17;
hence f + g is_right_improper_integrable_on a,b by A8, A21, A22; :: thesis:
then right_improper_integral ((f + g),a,b) = -infty by A21, A22, A34, Def4;
hence right_improper_integral ((f + g),a,b) = (right_improper_integral (f,a,b)) + (right_improper_integral (g,a,b)) by A15, A33, XXREAL_3:def 2; :: thesis:

end;

suppose A35: ( not f is_right_ext_Riemann_integrable_on a,b & g is_right_ext_Riemann_integrable_on a,b ) ; :: thesis:

then A36: right_improper_integral (g,a,b) = ext_right_integral (g,a,b) by A5, Th39;
consider Intg being PartFunc of REAL,REAL such that
A37: dom Intg = [.a,b.[ and
A38: for x being Real st x in dom Intg holds
Intg . x = integral (g,a,x) and
A39: Intg is_left_convergent_in b by A35, INTEGR10:def 1;
consider Intf being PartFunc of REAL,REAL such that
A40: dom Intf = [.a,b.[ and
A41: for x being Real st x in dom Intf holds
Intf . x = integral (f,a,x) and
( Intf is_left_convergent_in b or Intf is_left_divergent_to+infty_in b or Intf is_left_divergent_to-infty_in b ) by A4;
A42: dom (Intf + Intg) = [.a,b.[ /\ [.a,b.[ by A37, A40, VALUED_1:def 1
.= [.a,b.[ ;
A43: for x being Real st x in dom (Intf + Intg) holds
(Intf + Intg) . x = integral ((f + g),a,x)

proof

let x be Real; :: thesis:
assume A44: x in dom (Intf + Intg) ; :: thesis:
then A45: ( a <= x & x < b ) by A42, XXREAL_1:3;
then [.a,x.] c= [.a,b.[ by XXREAL_1:43;
then A46: ( [.a,x.] c= dom f & [.a,x.] c= dom g ) by A2, A3;
A47: ['a,x'] = [.a,x.] by A45, INTEGRA5:def 3;
( f is_integrable_on ['a,x'] & f | ['a,x'] is bounded & g is_integrable_on ['a,x'] & g | ['a,x'] is bounded ) by A4, A5, A45;
then integral ((f + g),['a,x']) = (integral (f,['a,x'])) + (integral (g,['a,x'])) by A46, A47, INTEGRA6:11;
then A48: integral ((f + g),a,x) = (integral (f,['a,x'])) + (integral (g,['a,x'])) by A45, INTEGRA5:def 4
.= (integral (f,a,x)) + (integral (g,['a,x'])) by A45, INTEGRA5:def 4
.= (integral (f,a,x)) + (integral (g,a,x)) by A45, INTEGRA5:def 4 ;
(Intf + Intg) . x = (Intf . x) + (Intg . x) by A44, VALUED_1:def 1
.= (integral (f,a,x)) + (Intg . x) by A44, A42, A40, A41
.= (integral (f,a,x)) + (integral (g,a,x)) by A44, A42, A37, A38 ;
hence (Intf + Intg) . x = integral ((f + g),a,x) by A48; :: thesis:

end;

A49: for r being Real st r < b holds
ex g being Real st
( r < g & g < b & g in dom (Intf + Intg) )

proof

let r be Real; :: thesis:
assume r < b ; :: thesis:
then consider g being Real such that
A50: ( max (a,r) < g & g < b ) by A1, XXREAL_0:29, XREAL_1:5;
take g ; :: thesis:
( max (a,r) >= a & max (a,r) >= r ) by XXREAL_0:25;
then ( r < g & a < g ) by A50, XXREAL_0:2;
hence ( r < g & g < b & g in dom (Intf + Intg) ) by A50, A42, XXREAL_1:3; :: thesis:

end;

A51: ( ex r being Real st
( 0 < r & Intg | ].(b - r),b.[ is bounded_below ) & ex r being Real st
( 0 < r & Intg | ].(b - r),b.[ is bounded_above ) ) by A39, Th11;

per cases by A4, A35, Th39;

suppose A52: right_improper_integral (f,a,b) = +infty ; :: thesis:

then A53: Intf + Intg is_left_divergent_to+infty_in b by A49, A4, A40, A41, A51, Th51, LIMFUNC2:17;
hence f + g is_right_improper_integrable_on a,b by A8, A42, A43; :: thesis:
then right_improper_integral ((f + g),a,b) = +infty by A42, A43, A53, Def4;
hence right_improper_integral ((f + g),a,b) = (right_improper_integral (f,a,b)) + (right_improper_integral (g,a,b)) by A36, A52, XXREAL_3:def 2; :: thesis:

end;

suppose A54: right_improper_integral (f,a,b) = -infty ; :: thesis:

then A55: Intf + Intg is_left_divergent_to-infty_in b by A49, A4, A40, A41, A51, Th52, Th17;
hence f + g is_right_improper_integrable_on a,b by A8, A42, A43; :: thesis:
then right_improper_integral ((f + g),a,b) = -infty by A42, A43, A55, Def4;
hence right_improper_integral ((f + g),a,b) = (right_improper_integral (f,a,b)) + (right_improper_integral (g,a,b)) by A36, A54, XXREAL_3:def 2; :: thesis:

end;

suppose A56: ( not f is_right_ext_Riemann_integrable_on a,b & not g is_right_ext_Riemann_integrable_on a,b ) ; :: thesis:

consider Intf being PartFunc of REAL,REAL such that
A57: dom Intf = [.a,b.[ and
A58: for x being Real st x in dom Intf holds
Intf . x = integral (f,a,x) and
( Intf is_left_convergent_in b or Intf is_left_divergent_to+infty_in b or Intf is_left_divergent_to-infty_in b ) by A4;
consider Intg being PartFunc of REAL,REAL such that
A59: dom Intg = [.a,b.[ and
A60: for x being Real st x in dom Intg holds
Intg . x = integral (g,a,x) and
( Intg is_left_convergent_in b or Intg is_left_divergent_to+infty_in b or Intg is_left_divergent_to-infty_in b ) by A5;
A61: dom (Intf + Intg) = [.a,b.[ /\ [.a,b.[ by A59, A57, VALUED_1:def 1
.= [.a,b.[ ;
A62: for x being Real st x in dom (Intf + Intg) holds
(Intf + Intg) . x = integral ((f + g),a,x)

proof

let x be Real; :: thesis:
assume A63: x in dom (Intf + Intg) ; :: thesis:
then A64: ( a <= x & x < b ) by A61, XXREAL_1:3;
then [.a,x.] c= [.a,b.[ by XXREAL_1:43;
then A65: ( [.a,x.] c= dom f & [.a,x.] c= dom g ) by A2, A3;
A66: ['a,x'] = [.a,x.] by A64, INTEGRA5:def 3;
( f is_integrable_on ['a,x'] & f | ['a,x'] is bounded & g is_integrable_on ['a,x'] & g | ['a,x'] is bounded ) by A4, A5, A64;
then integral ((f + g),['a,x']) = (integral (f,['a,x'])) + (integral (g,['a,x'])) by A65, A66, INTEGRA6:11;
then A67: integral ((f + g),a,x) = (integral (f,['a,x'])) + (integral (g,['a,x'])) by A64, INTEGRA5:def 4
.= (integral (f,a,x)) + (integral (g,['a,x'])) by A64, INTEGRA5:def 4
.= (integral (f,a,x)) + (integral (g,a,x)) by A64, INTEGRA5:def 4 ;
(Intf + Intg) . x = (Intf . x) + (Intg . x) by A63, VALUED_1:def 1
.= (integral (f,a,x)) + (Intg . x) by A63, A61, A57, A58
.= (integral (f,a,x)) + (integral (g,a,x)) by A63, A61, A59, A60 ;
hence (Intf + Intg) . x = integral ((f + g),a,x) by A67; :: thesis:

end;

A68: for r being Real st r < b holds
ex g being Real st
( r < g & g < b & g in dom (Intf + Intg) )

proof

let r be Real; :: thesis:
assume r < b ; :: thesis:
then consider g being Real such that
A69: ( max (a,r) < g & g < b ) by A1, XXREAL_0:29, XREAL_1:5;
take g ; :: thesis:
( max (a,r) >= a & max (a,r) >= r ) by XXREAL_0:25;
then ( r < g & a < g ) by A69, XXREAL_0:2;
hence ( r < g & g < b & g in dom (Intf + Intg) ) by A69, A61, XXREAL_1:3; :: thesis:

end;

per cases by A4, A56, Th39;

suppose A70: right_improper_integral (f,a,b) = +infty ; :: thesis:

then right_improper_integral (g,a,b) = +infty by A5, A56, Th39, A6;
then ex r being Real st
( 0 < r & Intg | ].(b - r),b.[ is bounded_below ) by A5, A59, A60, Th51, Th14;
then A71: Intf + Intg is_left_divergent_to+infty_in b by A70, A68, A4, A57, A58, Th51, LIMFUNC2:17;
hence f + g is_right_improper_integrable_on a,b by A8, A61, A62; :: thesis:
then right_improper_integral ((f + g),a,b) = +infty by A61, A62, A71, Def4;
hence right_improper_integral ((f + g),a,b) = (right_improper_integral (f,a,b)) + (right_improper_integral (g,a,b)) by A70, A6, XXREAL_3:def 2; :: thesis:

end;

suppose A72: right_improper_integral (f,a,b) = -infty ; :: thesis:

then right_improper_integral (g,a,b) = -infty by A5, A56, Th39, A7;
then ex r being Real st
( 0 < r & Intg | ].(b - r),b.[ is bounded_above ) by A5, A59, A60, Th52, Th15;
then A73: Intf + Intg is_left_divergent_to-infty_in b by A72, A68, A4, A57, A58, Th52, Th17;
hence f + g is_right_improper_integrable_on a,b by A8, A61, A62; :: thesis:
then right_improper_integral ((f + g),a,b) = -infty by A61, A62, A73, Def4;
hence right_improper_integral ((f + g),a,b) = (right_improper_integral (f,a,b)) + (right_improper_integral (g,a,b)) by A72, A7, XXREAL_3:def 2; :: thesis:

end;