theorem :: MATRIX_9:55

for i, n being Nat
for K being Field
for M, N being Matrix of n,K st i in Seg n holds
for p being Element of Permutations n ex k being Element of NAT st
( k in Seg n & i = p . k & (Col (N,i)) /. k = (Path_matrix (p,N)) /. k )