for seq1, seq2 being V183() ExtREAL_sequence st seq1 is convergent_to_finite_number & seq2 is convergent_to_finite_number holds
( seq1 + seq2 is convergent_to_finite_number & seq1 + seq2 is convergent & lim (seq1 + seq2) = (lim seq1) + (lim seq2) )