let seq, seq1, seq2 be ExtREAL_sequence; :: thesis: ( seq1 is convergent & seq2 is convergent & seq1 is nonnegative & seq2 is nonnegative & ( for k being Nat holds seq . k = (seq1 . k) + (seq2 . k) ) implies ( seq is nonnegative & seq is convergent & lim seq = (lim seq1) + (lim seq2) ) )
assume that
A1: seq1 is convergent and
A2: seq2 is convergent and
A3: seq1 is nonnegative and
A4: seq2 is nonnegative and
A5: for k being Nat holds seq . k = (seq1 . k) + (seq2 . k) ; :: thesis: ( seq is nonnegative & seq is convergent & lim seq = (lim seq1) + (lim seq2) )
A6: not seq2 is convergent_to_-infty by A4, Th8;
for n being object st n in dom seq holds
0. <= seq . n

proof

let n be object ; :: thesis: ( n in dom seq implies 0. <= seq . n )
assume n in dom seq ; :: thesis: 0. <= seq . n
then reconsider n1 = n as Nat ;
A7: 0 <= seq2 . n1 by A4, SUPINF_2:51;
A8: seq . n1 = (seq1 . n1) + (seq2 . n1) by A5;
0 <= seq1 . n1 by A3, SUPINF_2:51;
hence 0. <= seq . n by A7, A8; :: thesis: verum

end;

hence seq is nonnegative by SUPINF_2:52; :: thesis: ( seq is convergent & lim seq = (lim seq1) + (lim seq2) )
A9: not seq1 is convergent_to_-infty by A3, Th8;
for n being Nat holds 0 <= seq2 . n by A4, SUPINF_2:51;
then A10: lim seq2 <> -infty by A2, Th10;

per cases ( seq1 is convergent_to_+infty or seq1 is convergent_to_finite_number ) by A1, A9;

suppose A11: seq1 is convergent_to_+infty ; :: thesis: ( seq is convergent & lim seq = (lim seq1) + (lim seq2) )

for g being Real st 0 < g holds
ex n being Nat st
for m being Nat st n <= m holds
g <= seq . m

proof

let g be Real; :: thesis: ( 0 < g implies ex n being Nat st
for m being Nat st n <= m holds
g <= seq . m )
assume 0 < g ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
g <= seq . m
then consider n being Nat such that
A12: for m being Nat st n <= m holds
g <= seq1 . m by A11;
take n ; :: thesis: for m being Nat st n <= m holds
g <= seq . m
let m be Nat; :: thesis: ( n <= m implies g <= seq . m )
assume n <= m ; :: thesis: g <= seq . m
then A13: g <= seq1 . m by A12;
0 <= seq2 . m by A4, SUPINF_2:51;
then g + zz <= (seq1 . m) + (seq2 . m) by A13, XXREAL_3:36;
then g <= (seq1 . m) + (seq2 . m) by XXREAL_3:4;
hence g <= seq . m by A5; :: thesis: verum

end;

then A14: seq is convergent_to_+infty ;
hence seq is convergent ; :: thesis: lim seq = (lim seq1) + (lim seq2)
then A15: lim seq = +infty by A14, MESFUNC5:def 12;
lim seq1 = +infty by A1, A11, MESFUNC5:def 12;
hence lim seq = (lim seq1) + (lim seq2) by A10, A15, XXREAL_3:def 2; :: thesis: verum

end;

suppose A16: seq1 is convergent_to_finite_number ; :: thesis: ( seq is convergent & lim seq = (lim seq1) + (lim seq2) )

then A17: not seq1 is convergent_to_-infty by MESFUNC5:51;
not seq1 is convergent_to_+infty by A16, MESFUNC5:50;
then consider g being Real such that
A18: lim seq1 = g and
A19: for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.((seq1 . m) - (lim seq1)).| < p and
seq1 is convergent_to_finite_number by A1, A17, MESFUNC5:def 12;

per cases ( seq2 is convergent_to_+infty or seq2 is convergent_to_finite_number ) by A2, A6;

suppose A20: seq2 is convergent_to_+infty ; :: thesis: ( seq is convergent & lim seq = (lim seq1) + (lim seq2) )

for g being Real st 0 < g holds
ex n being Nat st
for m being Nat st n <= m holds
g <= seq . m

proof

let g be Real; :: thesis: ( 0 < g implies ex n being Nat st
for m being Nat st n <= m holds
g <= seq . m )
assume 0 < g ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
g <= seq . m
then consider n being Nat such that
A21: for m being Nat st n <= m holds
g <= seq2 . m by A20;
take n ; :: thesis: for m being Nat st n <= m holds
g <= seq . m
let m be Nat; :: thesis: ( n <= m implies g <= seq . m )
assume n <= m ; :: thesis: g <= seq . m
then A22: g <= seq2 . m by A21;
0 <= seq1 . m by A3, SUPINF_2:51;
then g + zz <= (seq1 . m) + (seq2 . m) by A22, XXREAL_3:36;
then g <= (seq1 . m) + (seq2 . m) by XXREAL_3:4;
hence g <= seq . m by A5; :: thesis: verum

end;

then A23: seq is convergent_to_+infty ;
hence seq is convergent ; :: thesis: lim seq = (lim seq1) + (lim seq2)
then A24: lim seq = +infty by A23, MESFUNC5:def 12;
lim seq2 = +infty by A2, A20, MESFUNC5:def 12;
hence lim seq = (lim seq1) + (lim seq2) by A18, A24, XXREAL_3:def 2; :: thesis: verum

end;

suppose A25: seq2 is convergent_to_finite_number ; :: thesis: ( seq is convergent & lim seq = (lim seq1) + (lim seq2) )

then A26: not seq2 is convergent_to_-infty by MESFUNC5:51;
not seq2 is convergent_to_+infty by A25, MESFUNC5:50;
then consider h being Real such that
A27: lim seq2 = h and
A28: for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.((seq2 . m) - (lim seq2)).| < p and
seq2 is convergent_to_finite_number by A2, A26, MESFUNC5:def 12;
reconsider h9 = h, g9 = g as Real ;
reconsider gh = g + h as R_eal by XXREAL_0:def 1;
A29: for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.((seq . m) - (g + h)).| < p

proof

let p be Real; :: thesis: ( 0 < p implies ex n being Nat st
for m being Nat st n <= m holds
|.((seq . m) - (g + h)).| < p )
reconsider pp = p as Element of REAL by XREAL_0:def 1;
assume A30: 0 < p ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
|.((seq . m) - (g + h)).| < p
then consider n1 being Nat such that
A31: for m being Nat st n1 <= m holds
|.((seq1 . m) - (lim seq1)).| < p / 2 by A19;
consider n2 being Nat such that
A32: for m being Nat st n2 <= m holds
|.((seq2 . m) - (lim seq2)).| < p / 2 by A28, A30;
reconsider n19 = n1, n29 = n2 as Element of NAT by ORDINAL1:def 12;
reconsider n = max (n19,n29) as Nat ;
take n ; :: thesis: for m being Nat st n <= m holds
|.((seq . m) - (g + h)).| < p
let m be Nat; :: thesis: ( n <= m implies |.((seq . m) - (g + h)).| < p )
assume A33: n <= m ; :: thesis: |.((seq . m) - (g + h)).| < p
A34: pp / 2 in REAL by XREAL_0:def 1;
n2 <= n by XXREAL_0:25;
then n2 <= m by A33, XXREAL_0:2;
then A35: |.((seq2 . m) - (lim seq2)).| < pp / 2 by A32;
then |.((seq2 . m) - (lim seq2)).| < +infty by XXREAL_0:2, XXREAL_0:9, A34;
then A36: (seq2 . m) - h in REAL by A27, EXTREAL1:41;
n1 <= n by XXREAL_0:25;
then n1 <= m by A33, XXREAL_0:2;
then A37: |.((seq1 . m) - (lim seq1)).| < pp / 2 by A31;
then |.((seq1 . m) - (lim seq1)).| < +infty by XXREAL_0:2, XXREAL_0:9, A34;
then (seq1 . m) - g in REAL by A18, EXTREAL1:41;
then consider e1, e2 being Real such that
A38: e1 = (seq1 . m) - g and
A39: e2 = (seq2 . m) - h by A36;
A40: |.((seq2 . m) - h).| = |.e2.| by A39, EXTREAL1:12;
A41: 0 <= seq2 . m by A4, SUPINF_2:51;
then A42: (seq2 . m) - h <> -infty by XXREAL_3:19;
A43: 0 <= seq1 . m by A3, SUPINF_2:51;
A44: |.((seq1 . m) - g).| = |.e1.| by A38, EXTREAL1:12;
then A45: |.((seq2 . m) - h).| + |.((seq1 . m) - g).| = |.e1.| + |.e2.| by A40, SUPINF_2:1;
g + h = g + h ;
then (seq . m) - (g + h) = ((seq . m) - h) - g by XXREAL_3:31
.= (((seq1 . m) + (seq2 . m)) - h) - g by A5
.= ((seq1 . m) + ((seq2 . m) - h)) - g by A43, A41, XXREAL_3:30
.= ((seq2 . m) - h) + ((seq1 . m) - g) by A43, A42, XXREAL_3:30 ;
then A46: |.((seq . m) - (g + h)).| <= |.((seq2 . m) - h).| + |.((seq1 . m) - g).| by EXTREAL1:24;
|.e1.| + |.e2.| < (p / 2) + (p / 2) by A18, A27, A37, A35, A44, A40, XREAL_1:8;
hence |.((seq . m) - (g + h)).| < p by A46, A45, XXREAL_0:2; :: thesis: verum

end;

then A47: seq is convergent_to_finite_number ;
hence seq is convergent ; :: thesis: lim seq = (lim seq1) + (lim seq2)
then lim seq = gh by A29, A47, MESFUNC5:def 12;
hence lim seq = (lim seq1) + (lim seq2) by A18, A27, SUPINF_2:1; :: thesis: verum

end;

end;

end;

end;