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 A1, Th48;

len (Path_matrix (p,N)) = n by MATRIX_3:def 7;

then A4: k in dom (Path_matrix (p,N)) by A2, FINSEQ_1:def 3;

then (Path_matrix (p,N)) . k = N * (k,i) by A3, MATRIX_3:def 7;

then A5: (Path_matrix (p,N)) /. k = N * (k,i) by A4, PARTFUN1:def 6;

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 A2, FINSEQ_1:def 3;

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 A2, A6, FINSEQ_1:def 3;

hence ( k in Seg n & i = p . k & (Col (N,i)) /. k = (Path_matrix (p,N)) /. k ) by A2, A3, A5, A7, PARTFUN1:def 6; :: thesis: verum

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 A1, Th48;

len (Path_matrix (p,N)) = n by MATRIX_3:def 7;

then A4: k in dom (Path_matrix (p,N)) by A2, FINSEQ_1:def 3;

then (Path_matrix (p,N)) . k = N * (k,i) by A3, MATRIX_3:def 7;

then A5: (Path_matrix (p,N)) /. k = N * (k,i) by A4, PARTFUN1:def 6;

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 A2, FINSEQ_1:def 3;

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 A2, A6, FINSEQ_1:def 3;

hence ( k in Seg n & i = p . k & (Col (N,i)) /. k = (Path_matrix (p,N)) /. k ) by A2, A3, A5, A7, PARTFUN1:def 6; :: thesis: verum