for K being Field
for x, y, z being FinSequence of K st len x = len y & len y = len z holds
mlt (z,(x + y)) = (mlt (z,x)) + (mlt (z,y))