:: deftheorem defines * MATRIX_3:def 11 :
for K being non empty commutative multMagma
for M being Matrix of K
for a being Element of K holds M * a = a * M;