let seq1, seq2, seq 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 set st n in dom seq holds
0. <= seq . n

proof

let n be set ; :: 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:70;
A8: seq . n1 = (seq1 . n1) + (seq2 . n1) by A5;
0 <= seq1 . n1 by A3, SUPINF_2:70;
hence 0. <= seq . n by A7, A8; :: thesis: verum

end;

hence seq is nonnegative by SUPINF_2:71; :: 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:70;
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, MESFUNC5:def 11;

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

for g being real number 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 number ; :: 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, MESFUNC5:def 9;
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:70;
then (R_EAL g) + 0. <= (seq1 . m) + (seq2 . m) by A13, XXREAL_3:38;
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 by MESFUNC5:def 9;
hence seq is convergent by MESFUNC5:def 11; :: 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:57;
not seq1 is convergent_to_+infty by A16, MESFUNC5:56;
then consider g being real number such that
A18: lim seq1 = g and
A19: for p being real number 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, MESFUNC5:def 11;

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

for g being real number 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 number ; :: 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, MESFUNC5:def 9;
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:70;
then (R_EAL g) + 0. <= (seq1 . m) + (seq2 . m) by A22, XXREAL_3:38;
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 by MESFUNC5:def 9;
hence seq is convergent by MESFUNC5:def 11; :: 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:57;
not seq2 is convergent_to_+infty by A25, MESFUNC5:56;
then consider h being real number such that
A27: lim seq2 = h and
A28: for p being real number 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 by XREAL_0:def 1;
A29: for p being real number st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.((seq . m) - (R_EAL (g + h))).| < p

proof

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

end;

then A47: seq is convergent_to_finite_number by MESFUNC5:def 8;
hence seq is convergent by MESFUNC5:def 11; :: thesis: lim seq = (lim seq1) + (lim seq2)
then lim seq = g9 + h9 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;