:: deftheorem defines * MATRIX_3:def 6 :
for K being Ring
for M being Matrix of K
for a being Element of K holds M * a = a * M;