theorem Th47: :: MATRIXR1:47

for a being Real
for x being FinSequence of REAL st len x > 0 holds
ColVec2Mx (a * x) = a * (ColVec2Mx x)