for x being FinSequence of COMPLEX
for i being Nat
for a being Complex holds (a * x) . i = a * (x . i)