:: deftheorem defines * MATRIXR1:def 12 :
for M being Matrix of REAL
for x being FinSequence of REAL holds x * M = Line (((LineVec2Mx x) * M),1);