theorem :: CLVECT_2:57

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