let seq1, seq2 be without-infty ExtREAL_sequence; :: thesis: ( seq1 is convergent_to_finite_number & seq2 is convergent_to_finite_number implies ( seq1 + seq2 is convergent_to_finite_number & seq1 + seq2 is convergent & lim (seq1 + seq2) = (lim seq1) + (lim seq2) ) )
assume A1: ( seq1 is convergent_to_finite_number & seq2 is convergent_to_finite_number ) ; :: thesis: ( seq1 + seq2 is convergent_to_finite_number & seq1 + seq2 is convergent & lim (seq1 + seq2) = (lim seq1) + (lim seq2) )
B2: ( not seq1 is convergent_to_-infty & not seq1 is convergent_to_+infty & not seq2 is convergent_to_-infty & not seq2 is convergent_to_+infty ) by A1, MESFUNC5:50, MESFUNC5:51;
consider S1 being Real such that
A2: ( lim seq1 = S1 & ( 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 ) & seq1 is convergent_to_finite_number ) by A1, B2, MESFUNC5:def 12;
consider S2 being Real such that
A3: ( lim seq2 = S2 & ( 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 ) & seq2 is convergent_to_finite_number ) by A1, B2, MESFUNC5:def 12;

B3: now :: thesis: for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.(((seq1 + seq2) . m) - (S1 + S2)).| < p

let p be Real; :: thesis: ( 0 < p implies ex n being Nat st
for m being Nat st n <= m holds
|.(((seq1 + seq2) . m) - (S1 + S2)).| < p )
assume A4: 0 < p ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
|.(((seq1 + seq2) . m) - (S1 + S2)).| < p
then consider n1 being Nat such that
A5: for m being Nat st n1 <= m holds
|.((seq1 . m) - S1).| < p / 2 by A2;
consider n2 being Nat such that
A6: for m being Nat st n2 <= m holds
|.((seq2 . m) - S2).| < p / 2 by A3, A4;
reconsider N1 = n1, N2 = n2 as Element of NAT by ORDINAL1:def 12;
reconsider n = max (N1,N2) as Nat ;
A7: ( n1 <= n & n2 <= n ) by XXREAL_0:25;

now :: thesis: for m being Nat st n <= m holds
|.(((seq1 + seq2) . m) - (S1 + S2)).| < p

let m be Nat; :: thesis: ( n <= m implies |.(((seq1 + seq2) . m) - (S1 + S2)).| < p )
assume n <= m ; :: thesis: |.(((seq1 + seq2) . m) - (S1 + S2)).| < p
then ( n1 <= m & n2 <= m ) by A7, XXREAL_0:2;
then A8: ( |.((seq1 . m) - S1).| < p / 2 & |.((seq2 . m) - S2).| < p / 2 ) by A5, A6;
then A9: |.((seq1 . m) - S1).| + |.((seq2 . m) - S2).| < (p / 2) + (p / 2) by XXREAL_3:64;
|.((seq1 . m) - S1).| < +infty by A8, XXREAL_0:2, XXREAL_0:4;
then A10: (seq1 . m) - S1 in REAL by EXTREAL1:41;
A12: ( seq1 . m <> -infty & seq2 . m <> -infty & (seq1 + seq2) . m <> -infty ) by MESFUNC5:def 5;
A13: m is Element of NAT by ORDINAL1:def 12;
((seq1 . m) - S1) + ((seq2 . m) - S2) = (((seq1 . m) - S1) + (seq2 . m)) - S2 by A10, XXREAL_3:30
.= ((- S1) + ((seq1 . m) + (seq2 . m))) - S2 by A12, XXREAL_3:29
.= (((seq1 + seq2) . m) - S1) - S2 by A13, Th7
.= ((seq1 + seq2) . m) - (S1 + S2) by XXREAL_3:31 ;
then |.(((seq1 + seq2) . m) - (S1 + S2)).| <= |.((seq1 . m) - S1).| + |.((seq2 . m) - S2).| by EXTREAL1:24;
hence |.(((seq1 + seq2) . m) - (S1 + S2)).| < p by A9, XXREAL_0:2; :: thesis: verum

end;

hence ex n being Nat st
for m being Nat st n <= m holds
|.(((seq1 + seq2) . m) - (S1 + S2)).| < p ; :: thesis: verum

end;

hence A14: seq1 + seq2 is convergent_to_finite_number by MESFUNC5:def 8; :: thesis: ( seq1 + seq2 is convergent & lim (seq1 + seq2) = (lim seq1) + (lim seq2) )
hence seq1 + seq2 is convergent ; :: thesis: lim (seq1 + seq2) = (lim seq1) + (lim seq2)
for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.(((seq1 + seq2) . m) - ((lim seq1) + (lim seq2))).| < p

proof

let p be Real; :: thesis: ( 0 < p implies ex n being Nat st
for m being Nat st n <= m holds
|.(((seq1 + seq2) . m) - ((lim seq1) + (lim seq2))).| < p )
assume 0 < p ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
|.(((seq1 + seq2) . m) - ((lim seq1) + (lim seq2))).| < p
then consider n being Nat such that
A17: for m being Nat st n <= m holds
|.(((seq1 + seq2) . m) - (S1 + S2)).| < p by B3;
take n ; :: thesis: for m being Nat st n <= m holds
|.(((seq1 + seq2) . m) - ((lim seq1) + (lim seq2))).| < p

hereby :: thesis: verum

let m be Nat; :: thesis: ( n <= m implies |.(((seq1 + seq2) . m) - ((lim seq1) + (lim seq2))).| < p )
assume n <= m ; :: thesis: |.(((seq1 + seq2) . m) - ((lim seq1) + (lim seq2))).| < p
then |.(((seq1 + seq2) . m) - (S1 + S2)).| < p by A17;
hence |.(((seq1 + seq2) . m) - ((lim seq1) + (lim seq2))).| < p by A2, A3, XXREAL_3:def 2; :: thesis: verum

end;

end;

hence lim (seq1 + seq2) = (lim seq1) + (lim seq2) by A2, A3, A14, MESFUNC5:def 12; :: thesis: verum