theorem Th6: :: SEQ_2:6

for seq, seq9 being Real_Sequence st seq is convergent & seq9 is convergent holds
lim (seq + seq9) = (lim seq) + (lim seq9)