theorem :: MATRIXR1:51

for a being Real
for x being FinSequence of REAL holds LineVec2Mx (a * x) = a * (LineVec2Mx x)