:: deftheorem Def4 defines * MATRIX_3:def 4 :
for K being Ring
for A, B being Matrix of K st width A = len B holds
for b₄ being Matrix of K holds
( b₄ = A * B iff ( len b₄ = len A & width b₄ = width B & ( for i, j being Nat st [i,j] in Indices b₄ holds
b₄ * (i,j) = (Line (A,i)) "*" (Col (B,j)) ) ) );