let f, g be PartFunc of REAL,REAL; :: thesis:
let b be Real; :: thesis:
assume that
A1: left_closed_halfline b c= dom f and
A2: left_closed_halfline b c= dom g and
A3: f is_-infty_improper_integrable_on b and
A4: g is_-infty_improper_integrable_on b and
A5: ( not improper_integral_-infty (f,b) = +infty or not improper_integral_-infty (g,b) = -infty ) and
A6: ( not improper_integral_-infty (f,b) = -infty or not improper_integral_-infty (g,b) = +infty ) ; :: thesis:
A7: for d being Real st d <= b holds
( f + g is_integrable_on ['d,b'] & (f + g) | ['d,b'] is bounded )

proof

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

end;

per cases ;

suppose A10: ( f is_-infty_ext_Riemann_integrable_on b & g is_-infty_ext_Riemann_integrable_on b ) ; :: thesis:

then A11: ( improper_integral_-infty (f,b) = infty_ext_left_integral (f,b) & improper_integral_-infty (g,b) = infty_ext_left_integral (g,b) ) by A3, A4, Th22;
A12: ( f + g is_-infty_ext_Riemann_integrable_on b & infty_ext_left_integral ((f + g),b) = (infty_ext_left_integral (f,b)) + (infty_ext_left_integral (g,b)) ) by A1, A2, A10, INTEGR10:10;
thus f + g is_-infty_improper_integrable_on b by A1, A2, A10, INTEGR10:10, Th20; :: thesis:
then improper_integral_-infty ((f + g),b) = infty_ext_left_integral ((f + g),b) by A12, Th22;
hence improper_integral_-infty ((f + g),b) = (improper_integral_-infty (f,b)) + (improper_integral_-infty (g,b)) by A11, A12, XXREAL_3:def 2; :: thesis:

end;

suppose A13: ( f is_-infty_ext_Riemann_integrable_on b & not g is_-infty_ext_Riemann_integrable_on b ) ; :: thesis:

then A14: improper_integral_-infty (f,b) = infty_ext_left_integral (f,b) by A3, Th22;
consider Intf being PartFunc of REAL,REAL such that
A15: dom Intf = left_closed_halfline b and
A16: for x being Real st x in dom Intf holds
Intf . x = integral (f,x,b) and
A17: Intf is convergent_in-infty by A13, INTEGR10:def 6;
consider Intg being PartFunc of REAL,REAL such that
A18: dom Intg = left_closed_halfline b and
A19: for x being Real st x in dom Intg holds
Intg . x = integral (g,x,b) and
( Intg is convergent_in-infty or Intg is divergent_in-infty_to+infty or Intg is divergent_in-infty_to-infty ) by A4;
A20: dom (Intf + Intg) = (left_closed_halfline b) /\ (left_closed_halfline b) by A15, A18, VALUED_1:def 1
.= left_closed_halfline b ;
A21: 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 A22: x in dom (Intf + Intg) ; :: thesis:
then A23: x <= b by A20, XXREAL_1:2;
[.x,b.] c= left_closed_halfline b by XXREAL_1:265;
then A24: ( [.x,b.] c= dom f & [.x,b.] c= dom g ) by A1, A2;
A25: ['x,b'] = [.x,b.] by A23, 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 A3, A4, A23;
then integral ((f + g),['x,b']) = (integral (f,['x,b'])) + (integral (g,['x,b'])) by A24, A25, INTEGRA6:11;
then A26: integral ((f + g),x,b) = (integral (f,['x,b'])) + (integral (g,['x,b'])) by A23, INTEGRA5:def 4
.= (integral (f,x,b)) + (integral (g,['x,b'])) by A23, INTEGRA5:def 4
.= (integral (f,x,b)) + (integral (g,x,b)) by A23, INTEGRA5:def 4 ;
(Intf + Intg) . x = (Intf . x) + (Intg . x) by A22, VALUED_1:def 1
.= (integral (f,x,b)) + (Intg . x) by A22, A20, A15, A16
.= (integral (f,x,b)) + (integral (g,x,b)) by A22, A20, A18, A19 ;
hence (Intf + Intg) . x = integral ((f + g),x,b) by A26; :: thesis:

end;

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

proof

let r be Real; :: thesis:
consider g being Real such that
A28: g < min (b,r) by XREAL_1:2;
take g ; :: thesis:
( min (b,r) <= b & min (b,r) <= r ) by XXREAL_0:17;
hence ( g < r & g in dom (Intf + Intg) ) by A20, A28, XXREAL_0:2, XXREAL_1:234; :: thesis:

end;

per cases by A4, A13, Th22;

suppose A29: improper_integral_-infty (g,b) = +infty ; :: thesis:

then A30: Intg is divergent_in-infty_to+infty by A4, A18, A19, Th37;
A31: ex r being Real st Intf | (left_open_halfline r) is bounded_below by A17, Th5;
then A32: Intf + Intg is divergent_in-infty_to+infty by A29, A27, A4, A18, A19, Th37, LIMFUNC1:56;
thus f + g is_-infty_improper_integrable_on b by A7, A20, A21, A31, A30, A27, LIMFUNC1:56; :: thesis:
then improper_integral_-infty ((f + g),b) = +infty by A20, A21, A32, Def3;
hence improper_integral_-infty ((f + g),b) = (improper_integral_-infty (f,b)) + (improper_integral_-infty (g,b)) by A14, A29, XXREAL_3:def 2; :: thesis:

end;

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

then A34: Intg is divergent_in-infty_to-infty by A4, A18, A19, Th38;
A35: ex r being Real st Intf | (left_open_halfline r) is bounded_above by A17, Th5;
then A36: Intf + Intg is divergent_in-infty_to-infty by A33, A27, A4, A18, A19, Th38, Th11;
thus f + g is_-infty_improper_integrable_on b by A7, A20, A21, A35, A34, A27, Th11; :: thesis:
then improper_integral_-infty ((f + g),b) = -infty by A20, A21, A36, Def3;
hence improper_integral_-infty ((f + g),b) = (improper_integral_-infty (f,b)) + (improper_integral_-infty (g,b)) by A14, A33, XXREAL_3:def 2; :: thesis:

end;

suppose A37: ( not f is_-infty_ext_Riemann_integrable_on b & g is_-infty_ext_Riemann_integrable_on b ) ; :: thesis:

then A38: improper_integral_-infty (g,b) = infty_ext_left_integral (g,b) by A4, Th22;
consider Intg being PartFunc of REAL,REAL such that
A39: dom Intg = left_closed_halfline b and
A40: for x being Real st x in dom Intg holds
Intg . x = integral (g,x,b) and
A41: Intg is convergent_in-infty by A37, INTEGR10:def 6;
consider Intf being PartFunc of REAL,REAL such that
A42: dom Intf = left_closed_halfline b and
A43: for x being Real st x in dom Intf holds
Intf . x = integral (f,x,b) and
( Intf is convergent_in-infty or Intf is divergent_in-infty_to+infty or Intf is divergent_in-infty_to-infty ) by A3;
A44: dom (Intf + Intg) = (left_closed_halfline b) /\ (left_closed_halfline b) by A39, A42, VALUED_1:def 1
.= left_closed_halfline b ;
A45: 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 A46: x in dom (Intf + Intg) ; :: thesis:
then A47: x <= b by A44, XXREAL_1:2;
[.x,b.] c= left_closed_halfline b by XXREAL_1:265;
then A48: ( [.x,b.] c= dom f & [.x,b.] c= dom g ) by A1, A2;
A49: ['x,b'] = [.x,b.] by A47, 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 A3, A4, A47;
then integral ((f + g),['x,b']) = (integral (f,['x,b'])) + (integral (g,['x,b'])) by A48, A49, INTEGRA6:11;
then A50: integral ((f + g),x,b) = (integral (f,['x,b'])) + (integral (g,['x,b'])) by A47, INTEGRA5:def 4
.= (integral (f,x,b)) + (integral (g,['x,b'])) by A47, INTEGRA5:def 4
.= (integral (f,x,b)) + (integral (g,x,b)) by A47, INTEGRA5:def 4 ;
(Intf + Intg) . x = (Intf . x) + (Intg . x) by A46, VALUED_1:def 1
.= (integral (f,x,b)) + (Intg . x) by A46, A44, A42, A43
.= (integral (f,x,b)) + (integral (g,x,b)) by A46, A44, A39, A40 ;
hence (Intf + Intg) . x = integral ((f + g),x,b) by A50; :: thesis:

end;

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

proof

let r be Real; :: thesis:
consider g being Real such that
A52: g < min (b,r) by XREAL_1:2;
take g ; :: thesis:
( min (b,r) <= b & min (b,r) <= r ) by XXREAL_0:17;
hence ( g < r & g in dom (Intf + Intg) ) by A44, A52, XXREAL_0:2, XXREAL_1:234; :: thesis:

end;

per cases by A3, A37, Th22;

suppose A53: improper_integral_-infty (f,b) = +infty ; :: thesis:

ex r being Real st Intg | (left_open_halfline r) is bounded_below by A41, Th5;
then A54: Intf + Intg is divergent_in-infty_to+infty by A53, A51, A3, A42, A43, Th37, LIMFUNC1:56;
hence f + g is_-infty_improper_integrable_on b by A7, A44, A45; :: thesis:
then improper_integral_-infty ((f + g),b) = +infty by A44, A45, A54, Def3;
hence improper_integral_-infty ((f + g),b) = (improper_integral_-infty (f,b)) + (improper_integral_-infty (g,b)) by A38, A53, XXREAL_3:def 2; :: thesis:

end;

suppose A55: improper_integral_-infty (f,b) = -infty ; :: thesis:

ex r being Real st Intg | (left_open_halfline r) is bounded_above by A41, Th5;
then A56: Intf + Intg is divergent_in-infty_to-infty by A55, A51, A3, A42, A43, Th38, Th11;
hence f + g is_-infty_improper_integrable_on b by A7, A44, A45; :: thesis:
then improper_integral_-infty ((f + g),b) = -infty by A44, A45, A56, Def3;
hence improper_integral_-infty ((f + g),b) = (improper_integral_-infty (f,b)) + (improper_integral_-infty (g,b)) by A38, A55, XXREAL_3:def 2; :: thesis:

end;

suppose A57: ( not f is_-infty_ext_Riemann_integrable_on b & not g is_-infty_ext_Riemann_integrable_on b ) ; :: thesis:

consider Intf being PartFunc of REAL,REAL such that
A58: dom Intf = left_closed_halfline b and
A59: for x being Real st x in dom Intf holds
Intf . x = integral (f,x,b) and
( Intf is convergent_in-infty or Intf is divergent_in-infty_to+infty or Intf is divergent_in-infty_to-infty ) by A3;
consider Intg being PartFunc of REAL,REAL such that
A60: dom Intg = left_closed_halfline b and
A61: for x being Real st x in dom Intg holds
Intg . x = integral (g,x,b) and
( Intg is convergent_in-infty or Intg is divergent_in-infty_to+infty or Intg is divergent_in-infty_to-infty ) by A4;
A62: dom (Intf + Intg) = (left_closed_halfline b) /\ (left_closed_halfline b) by A60, A58, VALUED_1:def 1
.= left_closed_halfline b ;
A63: 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 A64: x in dom (Intf + Intg) ; :: thesis:
then A65: x <= b by A62, XXREAL_1:2;
[.x,b.] c= left_closed_halfline b by XXREAL_1:265;
then A66: ( [.x,b.] c= dom f & [.x,b.] c= dom g ) by A1, A2;
A67: ['x,b'] = [.x,b.] by A65, 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 A3, A4, A65;
then integral ((f + g),['x,b']) = (integral (f,['x,b'])) + (integral (g,['x,b'])) by A66, A67, INTEGRA6:11;
then A68: integral ((f + g),x,b) = (integral (f,['x,b'])) + (integral (g,['x,b'])) by A65, INTEGRA5:def 4
.= (integral (f,x,b)) + (integral (g,['x,b'])) by A65, INTEGRA5:def 4
.= (integral (f,x,b)) + (integral (g,x,b)) by A65, INTEGRA5:def 4 ;
(Intf + Intg) . x = (Intf . x) + (Intg . x) by A64, VALUED_1:def 1
.= (integral (f,x,b)) + (Intg . x) by A64, A62, A58, A59
.= (integral (f,x,b)) + (integral (g,x,b)) by A64, A62, A60, A61 ;
hence (Intf + Intg) . x = integral ((f + g),x,b) by A68; :: thesis:

end;

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

proof

let r be Real; :: thesis:
consider g being Real such that
A70: g < min (b,r) by XREAL_1:2;
take g ; :: thesis:
( min (b,r) <= b & min (b,r) <= r ) by XXREAL_0:17;
hence ( g < r & g in dom (Intf + Intg) ) by A62, A70, XXREAL_0:2, XXREAL_1:234; :: thesis:

end;

per cases by A3, A57, Th22;

suppose A71: improper_integral_-infty (f,b) = +infty ; :: thesis:

then A72: Intf is divergent_in-infty_to+infty by A3, A58, A59, Th37;
improper_integral_-infty (g,b) = +infty by A71, A4, A57, A5, Th22;
then A73: ex r being Real st Intg | (left_open_halfline r) is bounded_below by A4, A60, A61, Th37, Th7;
then A74: Intf + Intg is divergent_in-infty_to+infty by A69, A71, A3, A58, A59, Th37, LIMFUNC1:56;
thus f + g is_-infty_improper_integrable_on b by A7, A62, A63, A73, A72, A69, LIMFUNC1:56; :: thesis:
then improper_integral_-infty ((f + g),b) = +infty by A62, A63, A74, Def3;
hence improper_integral_-infty ((f + g),b) = (improper_integral_-infty (f,b)) + (improper_integral_-infty (g,b)) by A5, A71, XXREAL_3:def 2; :: thesis:

end;

suppose A75: improper_integral_-infty (f,b) = -infty ; :: thesis:

then A76: Intf is divergent_in-infty_to-infty by A3, A58, A59, Th38;
improper_integral_-infty (g,b) = -infty by A75, A4, A57, A6, Th22;
then A77: ex r being Real st Intg | (left_open_halfline r) is bounded_above by A4, A60, A61, Th38, Th8;
then A78: Intf + Intg is divergent_in-infty_to-infty by A75, A69, A3, A58, A59, Th38, Th11;
thus f + g is_-infty_improper_integrable_on b by A7, A62, A63, A76, A69, A77, Th11; :: thesis:
then improper_integral_-infty ((f + g),b) = -infty by A62, A63, A78, Def3;
hence improper_integral_-infty ((f + g),b) = (improper_integral_-infty (f,b)) + (improper_integral_-infty (g,b)) by A6, A75, XXREAL_3:def 2; :: thesis:

end;