:: deftheorem Def4 defines * MATRIX11:def 4 :
for n, m being Nat
for D being non empty set
for F being Function of (Seg n),(Seg n)
for M, b₆ being Matrix of n,m,D holds
( b₆ = M * F iff ( len b₆ = len M & width b₆ = width M & ( for i, j, k being Nat st [i,j] in Indices M & F . i = k holds
b₆ * (i,j) = M * (k,j) ) ) );