theorem :: CLVECT_2:39

for X being ComplexUnitarySpace
for x, g being Point of X
for seq being sequence of X st seq is convergent & lim seq = g holds
( dist ((seq + x),(g + x)) is convergent & lim (dist ((seq + x),(g + x))) = 0 )