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

proof

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

end;

per cases ;

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

then A12: ( left_improper_integral (f,a,b) = ext_left_integral (f,a,b) & left_improper_integral (g,a,b) = ext_left_integral (g,a,b) ) by A4, A5, Th34;
A13: ( f + g is_left_ext_Riemann_integrable_on a,b & ext_left_integral ((f + g),a,b) = (ext_left_integral (f,a,b)) + (ext_left_integral (g,a,b)) ) by A1, A2, A3, A11, Th28;
thus f + g is_left_improper_integrable_on a,b by A1, A2, A3, A11, Th28, Th32; :: thesis:
then left_improper_integral ((f + g),a,b) = ext_left_integral ((f + g),a,b) by A13, Th34;
hence left_improper_integral ((f + g),a,b) = (left_improper_integral (f,a,b)) + (left_improper_integral (g,a,b)) by A12, A13, XXREAL_3:def 2; :: thesis:

end;

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

then A15: left_improper_integral (f,a,b) = ext_left_integral (f,a,b) by A4, Th34;
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,x,b) and
A18: Intf is_right_convergent_in a by A14, INTEGR10:def 2;
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,x,b) and
( Intg is_right_convergent_in a or Intg is_right_divergent_to+infty_in a or Intg is_right_divergent_to-infty_in a ) 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),x,b)

proof

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

end;

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

proof

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

end;

per cases by A5, A14, Th34;

suppose A30: left_improper_integral (g,a,b) = +infty ; :: thesis:

then A31: Intg is_right_divergent_to+infty_in a by A5, A19, A20, Th49;
A32: ex r being Real st
( 0 < r & Intf | ].a,(a + r).[ is bounded_below ) by A18, Th10;
then A33: Intf + Intg is_right_divergent_to+infty_in a by A30, A28, A5, A19, A20, Th49, LIMFUNC2:19;
thus f + g is_left_improper_integrable_on a,b by A8, A21, A22, A32, A31, A28, LIMFUNC2:19; :: thesis:
then left_improper_integral ((f + g),a,b) = +infty by A21, A22, A33, Def3;
hence left_improper_integral ((f + g),a,b) = (left_improper_integral (f,a,b)) + (left_improper_integral (g,a,b)) by A15, A30, XXREAL_3:def 2; :: thesis:

end;

suppose A34: left_improper_integral (g,a,b) = -infty ; :: thesis:

then A35: Intg is_right_divergent_to-infty_in a by A5, A19, A20, Th50;
A36: ex r being Real st
( 0 < r & Intf | ].a,(a + r).[ is bounded_above ) by A18, Th10;
then A37: Intf + Intg is_right_divergent_to-infty_in a by A34, A28, A5, A19, A20, Th50, Th16;
thus f + g is_left_improper_integrable_on a,b by A8, A21, A22, A36, A35, A28, Th16; :: thesis:
then left_improper_integral ((f + g),a,b) = -infty by A21, A22, A37, Def3;
hence left_improper_integral ((f + g),a,b) = (left_improper_integral (f,a,b)) + (left_improper_integral (g,a,b)) by A15, A34, XXREAL_3:def 2; :: thesis:

end;

suppose A38: ( not f is_left_ext_Riemann_integrable_on a,b & g is_left_ext_Riemann_integrable_on a,b ) ; :: thesis:

then A39: left_improper_integral (g,a,b) = ext_left_integral (g,a,b) by A5, Th34;
consider Intg being PartFunc of REAL,REAL such that
A40: dom Intg = ].a,b.] and
A41: for x being Real st x in dom Intg holds
Intg . x = integral (g,x,b) and
A42: Intg is_right_convergent_in a by A38, INTEGR10:def 2;
consider Intf being PartFunc of REAL,REAL such that
A43: dom Intf = ].a,b.] and
A44: for x being Real st x in dom Intf holds
Intf . x = integral (f,x,b) and
( Intf is_right_convergent_in a or Intf is_right_divergent_to+infty_in a or Intf is_right_divergent_to-infty_in a ) by A4;
A45: dom (Intf + Intg) = ].a,b.] /\ ].a,b.] by A40, A43, VALUED_1:def 1
.= ].a,b.] ;
A46: for x being Real st x in dom (Intf + Intg) holds
(Intf + Intg) . x = integral ((f + g),x,b)

proof

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

end;

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

proof

let r be Real; :: thesis:
assume a < r ; :: thesis:
then consider g being Real such that
A53: ( a < g & g < min (b,r) ) by A1, XXREAL_0:21, XREAL_1:5;
take g ; :: thesis:
( min (b,r) <= b & min (b,r) <= r ) by XXREAL_0:17;
then ( g < b & g < r ) by A53, XXREAL_0:2;
hence ( g < r & a < g & g in dom (Intf + Intg) ) by A53, A45, XXREAL_1:2; :: thesis:

end;

per cases by A4, A38, Th34;

suppose A54: left_improper_integral (f,a,b) = +infty ; :: thesis:

ex r being Real st
( 0 < r & Intg | ].a,(a + r).[ is bounded_below ) by A42, Th10;
then A55: Intf + Intg is_right_divergent_to+infty_in a by A54, A52, A4, A43, A44, Th49, LIMFUNC2:19;
hence f + g is_left_improper_integrable_on a,b by A8, A45, A46; :: thesis:
then left_improper_integral ((f + g),a,b) = +infty by A45, A46, A55, Def3;
hence left_improper_integral ((f + g),a,b) = (left_improper_integral (f,a,b)) + (left_improper_integral (g,a,b)) by A39, A54, XXREAL_3:def 2; :: thesis:

end;

suppose A56: left_improper_integral (f,a,b) = -infty ; :: thesis:

ex r being Real st
( 0 < r & Intg | ].a,(a + r).[ is bounded_above ) by A42, Th10;
then A57: Intf + Intg is_right_divergent_to-infty_in a by A56, A52, A4, A43, A44, Th50, Th16;
hence f + g is_left_improper_integrable_on a,b by A8, A45, A46; :: thesis:
then left_improper_integral ((f + g),a,b) = -infty by A45, A46, A57, Def3;
hence left_improper_integral ((f + g),a,b) = (left_improper_integral (f,a,b)) + (left_improper_integral (g,a,b)) by A39, A56, XXREAL_3:def 2; :: thesis:

end;

suppose A58: ( not f is_left_ext_Riemann_integrable_on a,b & not g is_left_ext_Riemann_integrable_on a,b ) ; :: thesis:

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

proof

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

end;

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

proof

let r be Real; :: thesis:
assume a < r ; :: thesis:
then consider g being Real such that
A71: ( a < g & g < min (b,r) ) by A1, XXREAL_0:21, XREAL_1:5;
take g ; :: thesis:
( min (b,r) <= b & min (b,r) <= r ) by XXREAL_0:17;
then ( g < b & g < r ) by A71, XXREAL_0:2;
hence ( g < r & a < g & g in dom (Intf + Intg) ) by A71, A63, XXREAL_1:2; :: thesis:

end;

per cases by A4, A58, Th34;

suppose A72: left_improper_integral (f,a,b) = +infty ; :: thesis:

then A73: Intf is_right_divergent_to+infty_in a by A4, A59, A60, Th49;
left_improper_integral (g,a,b) = +infty by A72, A5, A58, Th34, A6;
then A74: ex r being Real st
( 0 < r & Intg | ].a,(a + r).[ is bounded_below ) by A5, A61, A62, Th49, Th12;
then A75: Intf + Intg is_right_divergent_to+infty_in a by A70, A72, A4, A59, A60, Th49, LIMFUNC2:19;
thus f + g is_left_improper_integrable_on a,b by A8, A63, A64, A74, A73, A70, LIMFUNC2:19; :: thesis:
then left_improper_integral ((f + g),a,b) = +infty by A63, A64, A75, Def3;
hence left_improper_integral ((f + g),a,b) = (left_improper_integral (f,a,b)) + (left_improper_integral (g,a,b)) by A6, A72, XXREAL_3:def 2; :: thesis:

end;

suppose A76: left_improper_integral (f,a,b) = -infty ; :: thesis:

then A77: Intf is_right_divergent_to-infty_in a by A4, A59, A60, Th50;
left_improper_integral (g,a,b) = -infty by A76, A5, A58, Th34, A7;
then A78: ex r being Real st
( 0 < r & Intg | ].a,(a + r).[ is bounded_above ) by A5, A61, A62, Th50, Th13;
then A79: Intf + Intg is_right_divergent_to-infty_in a by A76, A70, A4, A59, A60, Th50, Th16;
thus f + g is_left_improper_integrable_on a,b by A8, A63, A64, A77, A70, A78, Th16; :: thesis:
then left_improper_integral ((f + g),a,b) = -infty by A63, A64, A79, Def3;
hence left_improper_integral ((f + g),a,b) = (left_improper_integral (f,a,b)) + (left_improper_integral (g,a,b)) by A7, A76, XXREAL_3:def 2; :: thesis:

end;