:: deftheorem Def5 defines * MATRIX_3:def 5 :
for K being non empty multMagma
for M being Matrix of K
for a being Element of K
for b₄ being Matrix of K holds
( b₄ = a * M iff ( len b₄ = len M & width b₄ = width M & ( for i, j being Nat st [i,j] in Indices M holds
b₄ * (i,j) = a * (M * (i,j)) ) ) );