:: deftheorem Def6 defines @ MATRIX_0:def 6 :
for D being non empty set
for M, b₃ being Matrix of D holds
( b₃ = M @ iff ( len b₃ = width M & ( for i, j being Nat holds
( [i,j] in Indices b₃ iff [j,i] in Indices M ) ) & ( for i, j being Nat st [j,i] in Indices M holds
b₃ * (i,j) = M * (j,i) ) ) );