theorem Th2: :: BHSP_2:2

for X being RealUnitarySpace
for seq, seq9 being sequence of X st seq is convergent & ex k being Nat st
for n being Nat st k <= n holds
seq9 . n = seq . n holds
seq9 is convergent