for z being FinSequence of COMPLEX
for a, b being Complex holds (a + b) * z = (a * z) + (b * z)