theorem Th8: :: MATRIX14:8

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