theorem Th11: :: MESFUNC9:11

for seq, seq1, seq2 being ExtREAL_sequence st seq1 is convergent & seq2 is convergent & seq1 is V115() & seq2 is V115() & ( for k being Nat holds seq . k = (seq1 . k) + (seq2 . k) ) holds
( seq is V115() & seq is convergent & lim seq = (lim seq1) + (lim seq2) )