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