:: deftheorem Def5 defines * MATRIX_0:def 5 :
for D being set
for M being Matrix of D
for i, j being Nat st [i,j] in Indices M holds
for b₅ being Element of D holds
( b₅ = M * (i,j) iff ex p being FinSequence of D st
( p = M . i & b₅ = p . j ) );