:: deftheorem defines * MATRIXC1:def 7 :
for M being Matrix of COMPLEX
for a being Complex holds M * a = a * M;