for x, y being FinSequence of COMPLEX
for a being Element of COMPLEX st len x = len y holds
mlt ((a * x),y) = a * (mlt (x,y))