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;
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 8;
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_1:def 3;
then k in dom N by A2, FINSEQ_1:def 3;
then A7: (Col N,i) . k = N * k,i by MATRIX_1:def 9;
len (Col N,i) = len N by MATRIX_1:def 9;
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 8; :: thesis: verum