theorem Th36: :: TOPRNS_1:36

for N being Nat
for seq, seq9 being Real_Sequence of N st seq is convergent & seq9 is convergent holds
seq + seq9 is convergent