for a, b being Complex
for X being ComplexUnitarySpace
for seq being sequence of X holds (a + b) * seq = (a * seq) + (b * seq)