theorem Th30: :: MATRIX15:30

for K being Field
for a being Element of K
for f being FinSequence of K holds a * (ColVec2Mx f) = ColVec2Mx (a * f)