for X being ComplexUnitarySpace
for z being Complex
for seq being sequence of X st seq is Cauchy holds
z * seq is Cauchy