let i, n be Nat; :: thesis: 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 )

let K be Field; :: thesis: 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 )

let M, N be Matrix of n,K; :: thesis: ( i in Seg n implies 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 ) )

assume A1: i in Seg n ; :: thesis: 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 )

let p be Element of Permutations n; :: thesis: ex k being Element of NAT st
( k in Seg n & i = p . k & (Col (N,i)) /. k = (Path_matrix (p,N)) /. k )

n in NAT by ORDINAL1:def 12;
then consider k being Element of NAT such that
A2: k in Seg n and
A3: i = p . k by ;
len (Path_matrix (p,N)) = n by MATRIX_3:def 7;
then A4: k in dom (Path_matrix (p,N)) by ;
then (Path_matrix (p,N)) . k = N * (k,i) by ;
then A5: (Path_matrix (p,N)) /. k = N * (k,i) by ;
take k ; :: thesis: ( k in Seg n & i = p . k & (Col (N,i)) /. k = (Path_matrix (p,N)) /. k )
A6: len N = n by MATRIX_0:def 2;
then k in dom N by ;
then A7: (Col (N,i)) . k = N * (k,i) by MATRIX_0:def 8;
len (Col (N,i)) = len N by MATRIX_0:def 8;
then k in dom (Col (N,i)) by ;
hence ( k in Seg n & i = p . k & (Col (N,i)) /. k = (Path_matrix (p,N)) /. k ) by ; :: thesis: verum