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

proof

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

end;

per cases ;

suppose A10: ( f is_+infty_ext_Riemann_integrable_on a & g is_+infty_ext_Riemann_integrable_on a ) ; :: thesis:

then A11: ( improper_integral_+infty (f,a) = infty_ext_right_integral (f,a) & improper_integral_+infty (g,a) = infty_ext_right_integral (g,a) ) by A3, A4, Th27;
A12: ( f + g is_+infty_ext_Riemann_integrable_on a & infty_ext_right_integral ((f + g),a) = (infty_ext_right_integral (f,a)) + (infty_ext_right_integral (g,a)) ) by A1, A2, A10, INTEGR10:8;
thus f + g is_+infty_improper_integrable_on a by A1, A2, A10, Th21, INTEGR10:8; :: thesis:
then improper_integral_+infty ((f + g),a) = infty_ext_right_integral ((f + g),a) by A12, Th27;
hence improper_integral_+infty ((f + g),a) = (improper_integral_+infty (f,a)) + (improper_integral_+infty (g,a)) by A11, A12, XXREAL_3:def 2; :: thesis:

end;

suppose A13: ( f is_+infty_ext_Riemann_integrable_on a & not g is_+infty_ext_Riemann_integrable_on a ) ; :: thesis:

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

end;

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

proof

let r be Real; :: thesis:
consider g being Real such that
A28: max (a,r) < g by XREAL_1:1;
take g ; :: thesis:
( max (a,r) >= a & max (a,r) >= r ) by XXREAL_0:25;
hence ( r < g & g in dom (Intf + Intg) ) by A20, A28, XXREAL_0:2, XXREAL_1:236; :: thesis:

end;

A29: ( ex r being Real st Intf | (right_open_halfline r) is bounded_below & ex r being Real st Intf | (right_open_halfline r) is bounded_above ) by A17, Th6;

per cases by A4, A13, Th27;

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

then A31: Intf + Intg is divergent_in+infty_to+infty by A27, A4, A18, A19, A29, Th39, LIMFUNC1:54;
hence f + g is_+infty_improper_integrable_on a by A7, A20, A21; :: thesis:
then improper_integral_+infty ((f + g),a) = +infty by A20, A21, A31, Def4;
hence improper_integral_+infty ((f + g),a) = (improper_integral_+infty (f,a)) + (improper_integral_+infty (g,a)) by A14, A30, XXREAL_3:def 2; :: thesis:

end;

suppose A32: improper_integral_+infty (g,a) = -infty ; :: thesis:

then A33: Intf + Intg is divergent_in+infty_to-infty by A27, A4, A18, A19, A29, Th40, Th12;
hence f + g is_+infty_improper_integrable_on a by A7, A20, A21; :: thesis:
then improper_integral_+infty ((f + g),a) = -infty by A20, A21, A33, Def4;
hence improper_integral_+infty ((f + g),a) = (improper_integral_+infty (f,a)) + (improper_integral_+infty (g,a)) by A14, A32, XXREAL_3:def 2; :: thesis:

end;

suppose A34: ( not f is_+infty_ext_Riemann_integrable_on a & g is_+infty_ext_Riemann_integrable_on a ) ; :: thesis:

then A35: improper_integral_+infty (g,a) = infty_ext_right_integral (g,a) by A4, Th27;
consider Intg being PartFunc of REAL,REAL such that
A36: dom Intg = right_closed_halfline a and
A37: for x being Real st x in dom Intg holds
Intg . x = integral (g,a,x) and
A38: Intg is convergent_in+infty by A34, INTEGR10:def 5;
consider Intf being PartFunc of REAL,REAL such that
A39: dom Intf = right_closed_halfline a and
A40: for x being Real st x in dom Intf holds
Intf . x = integral (f,a,x) and
( Intf is convergent_in+infty or Intf is divergent_in+infty_to+infty or Intf is divergent_in+infty_to-infty ) by A3;
A41: dom (Intf + Intg) = (right_closed_halfline a) /\ (right_closed_halfline a) by A36, A39, VALUED_1:def 1
.= right_closed_halfline a ;
A42: 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 A43: x in dom (Intf + Intg) ; :: thesis:
then A44: a <= x by A41, XXREAL_1:3;
[.a,x.] c= [.a,+infty.[ by XXREAL_1:251;
then A45: ( [.a,x.] c= dom f & [.a,x.] c= dom g ) by A1, A2;
A46: ['a,x'] = [.a,x.] by A44, 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 A3, A4, A44;
then integral ((f + g),['a,x']) = (integral (f,['a,x'])) + (integral (g,['a,x'])) by A45, A46, INTEGRA6:11;
then A47: integral ((f + g),a,x) = (integral (f,['a,x'])) + (integral (g,['a,x'])) by A44, INTEGRA5:def 4
.= (integral (f,a,x)) + (integral (g,['a,x'])) by A44, INTEGRA5:def 4
.= (integral (f,a,x)) + (integral (g,a,x)) by A44, INTEGRA5:def 4 ;
(Intf + Intg) . x = (Intf . x) + (Intg . x) by A43, VALUED_1:def 1
.= (integral (f,a,x)) + (Intg . x) by A43, A41, A39, A40
.= (integral (f,a,x)) + (integral (g,a,x)) by A43, A41, A36, A37 ;
hence (Intf + Intg) . x = integral ((f + g),a,x) by A47; :: thesis:

end;

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

proof

let r be Real; :: thesis:
consider g being Real such that
A49: max (a,r) < g by XREAL_1:1;
take g ; :: thesis:
( max (a,r) >= a & max (a,r) >= r ) by XXREAL_0:25;
hence ( r < g & g in dom (Intf + Intg) ) by A41, A49, XXREAL_0:2, XXREAL_1:236; :: thesis:

end;

A50: ( ex r being Real st Intg | (right_open_halfline r) is bounded_below & ex r being Real st Intg | (right_open_halfline r) is bounded_above ) by A38, Th6;

per cases by A3, A34, Th27;

suppose A51: improper_integral_+infty (f,a) = +infty ; :: thesis:

then A52: Intf + Intg is divergent_in+infty_to+infty by A48, A3, A39, A40, A50, Th39, LIMFUNC1:54;
hence f + g is_+infty_improper_integrable_on a by A7, A41, A42; :: thesis:
then improper_integral_+infty ((f + g),a) = +infty by A41, A42, A52, Def4;
hence improper_integral_+infty ((f + g),a) = (improper_integral_+infty (f,a)) + (improper_integral_+infty (g,a)) by A35, A51, XXREAL_3:def 2; :: thesis:

end;

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

then A54: Intf + Intg is divergent_in+infty_to-infty by A48, A3, A39, A40, A50, Th40, Th12;
hence f + g is_+infty_improper_integrable_on a by A7, A41, A42; :: thesis:
then improper_integral_+infty ((f + g),a) = -infty by A41, A42, A54, Def4;
hence improper_integral_+infty ((f + g),a) = (improper_integral_+infty (f,a)) + (improper_integral_+infty (g,a)) by A35, A53, XXREAL_3:def 2; :: thesis:

end;

suppose A55: ( not f is_+infty_ext_Riemann_integrable_on a & not g is_+infty_ext_Riemann_integrable_on a ) ; :: thesis:

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

end;

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

proof

let r be Real; :: thesis:
consider g being Real such that
A68: max (a,r) < g by XREAL_1:1;
take g ; :: thesis:
( max (a,r) >= a & max (a,r) >= r ) by XXREAL_0:25;
hence ( r < g & g in dom (Intf + Intg) ) by A60, A68, XXREAL_0:2, XXREAL_1:236; :: thesis:

end;

per cases by A3, A55, Th27;

suppose A69: improper_integral_+infty (f,a) = +infty ; :: thesis:

then improper_integral_+infty (g,a) = +infty by A4, A55, Th27, A5;
then ex r being Real st Intg | (right_open_halfline r) is bounded_below by A4, A58, A59, Th39, Th9;
then A70: Intf + Intg is divergent_in+infty_to+infty by A69, A67, A3, A56, A57, Th39, LIMFUNC1:54;
hence f + g is_+infty_improper_integrable_on a by A7, A60, A61; :: thesis:
then improper_integral_+infty ((f + g),a) = +infty by A60, A61, A70, Def4;
hence improper_integral_+infty ((f + g),a) = (improper_integral_+infty (f,a)) + (improper_integral_+infty (g,a)) by A69, A5, XXREAL_3:def 2; :: thesis:

end;

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

then improper_integral_+infty (g,a) = -infty by A4, A55, Th27, A6;
then ex r being Real st Intg | (right_open_halfline r) is bounded_above by A4, A58, A59, Th40, Th10;
then A72: Intf + Intg is divergent_in+infty_to-infty by A71, A67, A3, A56, A57, Th40, Th12;
hence f + g is_+infty_improper_integrable_on a by A7, A60, A61; :: thesis:
then improper_integral_+infty ((f + g),a) = -infty by A60, A61, A72, Def4;
hence improper_integral_+infty ((f + g),a) = (improper_integral_+infty (f,a)) + (improper_integral_+infty (g,a)) by A71, A6, XXREAL_3:def 2; :: thesis:

end;