theorem Th1: :: CLVECT_2:1

for X being ComplexUnitarySpace
for seq being sequence of X st seq is constant holds
seq is convergent