for X being ComplexUnitarySpace
for seq, seq1, seq2 being sequence of X st seq1 is constant & seq2 is constant & seq = seq1 - seq2 holds
seq is constant