for a being Complex
for X being ComplexUnitarySpace
for seq1, seq2 being sequence of X holds a * (seq1 - seq2) = (a * seq1) - (a * seq2)