theorem Th10: :: CLVECT_2:10

for X being ComplexUnitarySpace
for x being Point of X
for seq being sequence of X st seq is constant & x in rng seq holds
lim seq = x