theorem :: CSSPACE:68

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