theorem :: MATRIX15:29
for K being Field
for a being Element of K
for f being FinSequence of K holds a * (LineVec2Mx f) = LineVec2Mx (a * f)