theorem :: CLVECT_2:11

for X being ComplexUnitarySpace
for x being Point of X
for seq being sequence of X st seq is constant & ex n being Nat st seq . n = x holds
lim seq = x