:: deftheorem Def3 defines 1. MATRIX_1:def 3 :
for K being non empty doubleLoopStr
for n being Nat
for b₃ being Matrix of n,K holds
( b₃ = 1. (K,n) iff ( ( for i being Nat st [i,i] in Indices b₃ holds
b₃ * (i,i) = 1. K ) & ( for i, j being Nat st [i,j] in Indices b₃ & i <> j holds
b₃ * (i,j) = 0. K ) ) );