theorem Th8: :: CLVECT_2:8

for X being ComplexUnitarySpace
for x being Point of X
for seq being sequence of X st seq is convergent holds
seq - x is convergent