theorem Th18: :: SEQ_4:18

for seq, seq1 being Real_Sequence st seq is convergent & ex k being Nat st
for n being Nat st k <= n holds
seq1 . n = seq . n holds
seq1 is convergent