:: deftheorem Def7 defines |: MATRIX10:def 7 :
for M, b₂ being Matrix of REAL 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)).| ) ) );