for a being Complex
for X being ComplexUnitarySpace
for seq, seq1 being sequence of X st seq1 is constant & seq = a * seq1 holds
seq is constant