for x being FinSequence of COMPLEX
for a being Complex holds (a * x) *' = (a *') * (x *')