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