for n, m being Nat
for D being non empty set
for F being Function of (Seg n),(Seg n)
for M being Matrix of n,m,D holds
( Indices M = Indices (M * F) & ( for i, j being Nat st [i,j] in Indices M holds
ex k being Nat st
( F . i = k & [k,j] in Indices M & (M * F) * (i,j) = M * (k,j) ) ) )