theorem Th2: :: CLVECT_2:2

for X being ComplexUnitarySpace
for seq1, seq2 being sequence of X st seq1 is convergent & ex k being Nat st
for n being Nat st k <= n holds
seq2 . n = seq1 . n holds
seq2 is convergent