let n be Nat; :: thesis: for K being Field
for M being Matrix of n,K st ex i being Element of NAT st
( i in Seg n & ( for k being Element of NAT st k in Seg n holds
(Col (M,i)) . k = 0. K ) ) holds
for p being Element of Permutations n ex l being Element of NAT st
( l in Seg n & (Path_matrix (p,M)) . l = 0. K )
let K be Field; :: thesis: for M being Matrix of n,K st ex i being Element of NAT st
( i in Seg n & ( for k being Element of NAT st k in Seg n holds
(Col (M,i)) . k = 0. K ) ) holds
for p being Element of Permutations n ex l being Element of NAT st
( l in Seg n & (Path_matrix (p,M)) . l = 0. K )
let M be Matrix of n,K; :: thesis: ( ex i being Element of NAT st
( i in Seg n & ( for k being Element of NAT st k in Seg n holds
(Col (M,i)) . k = 0. K ) ) implies for p being Element of Permutations n ex l being Element of NAT st
( l in Seg n & (Path_matrix (p,M)) . l = 0. K ) )
assume ex i being Element of NAT st
( i in Seg n & ( for k being Element of NAT st k in Seg n holds
(Col (M,i)) . k = 0. K ) ) ; :: thesis: for p being Element of Permutations n ex l being Element of NAT st
( l in Seg n & (Path_matrix (p,M)) . l = 0. K )
then consider i being Element of NAT such that
A1: i in Seg n and
A2: for k being Element of NAT st k in Seg n holds
(Col (M,i)) . k = 0. K ;
let p be Element of Permutations n; :: thesis: ex l being Element of NAT st
( l in Seg n & (Path_matrix (p,M)) . l = 0. K )
n in NAT by ORDINAL1:def 12;
then consider k being Element of NAT such that
A3: k in Seg n and
A4: i = p . k by A1, Th48;
A5: 1 <= k by A3, FINSEQ_1:1;
len M = n by MATRIX_0:def 2;
then k <= len M by A3, FINSEQ_1:1;
then A6: k in dom M by A5, FINSEQ_3:25;
take k ; :: thesis: ( k in Seg n & (Path_matrix (p,M)) . k = 0. K )
len (Path_matrix (p,M)) = n by MATRIX_3:def 7;
then dom (Path_matrix (p,M)) = Seg n by FINSEQ_1:def 3;
then (Path_matrix (p,M)) . k = M * (k,i) by A3, A4, MATRIX_3:def 7;
then (Path_matrix (p,M)) . k = (Col (M,i)) . k by A6, MATRIX_0:def 8;
hence ( k in Seg n & (Path_matrix (p,M)) . k = 0. K ) by A2, A3; :: thesis: verum