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