:: deftheorem Def1 defines *' MATRIXC1:def 1 :
for M, b₂ being Matrix of COMPLEX holds
( b₂ = 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) = (M * (i,j)) *' ) ) );