:: deftheorem defines * MATRIXR1:def 11 :
for M being Matrix of REAL
for x being FinSequence of REAL holds M * x = Col ((M * (ColVec2Mx x)),1);