let n, i 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 13;
then consider k being Element of NAT such that
A2: k in Seg n and
A3: i = p . k by A1, Th48;
A4: len N = n by MATRIX_1:def 3;
then A5: k in dom N by A2, FINSEQ_1:def 3;
take k ; :: thesis: ( k in Seg n & i = p . k & (Col N,i) /. k = (Path_matrix p,N) /. k )
len (Path_matrix p,N) = n by MATRIX_3:def 7;
then A6: 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 A7: (Path_matrix p,N) /. k = N * k,i by A6, PARTFUN1:def 8;
len (Col N,i) = len N by MATRIX_1:def 9;
then A8: k in dom (Col N,i) by A2, A4, FINSEQ_1:def 3;
(Col N,i) . k = N * k,i by A5, MATRIX_1:def 9;
hence ( k in Seg n & i = p . k & (Col N,i) /. k = (Path_matrix p,N) /. k ) by A2, A3, A7, A8, PARTFUN1:def 8; :: thesis: verum