let n be Nat; :: thesis: for K being Field
for p being Element of Permutations n
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
(Path_product M) . p = 0. K
let K be Field; :: thesis: for p being Element of Permutations n
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
(Path_product M) . p = 0. K
let p be Element of Permutations n; :: 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
(Path_product M) . p = 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 (Path_product M) . p = 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: (Path_product M) . p = 0. K
then consider l being Element of NAT such that
A1: ( l in Seg n & (Path_matrix p,M) . l = 0. K ) by Th49;
set k = l;
len (Path_matrix p,M) = n by MATRIX_3:def 7;
then l in dom (Path_matrix p,M) by A1, FINSEQ_1:def 3;
then A2: Product (Path_matrix p,M) = 0. K by A1, FVSUM_1:107;
A3: (Path_product M) . p = - (the multF of K $$ (Path_matrix p,M)),p by MATRIX_3:def 8
.= - (Product (Path_matrix p,M)),p by GROUP_4:def 3 ;

per cases ( p is even or not p is even ) ;

suppose p is even ; :: thesis: (Path_product M) . p = 0. K

hence (Path_product M) . p = 0. K by A2, A3, MATRIX_2:def 16; :: thesis: verum

end;

suppose not p is even ; :: thesis: (Path_product M) . p = 0. K

then - (Product (Path_matrix p,M)),p = - (Product (Path_matrix p,M)) by MATRIX_2:def 16
.= 0. K by A2, RLVECT_1:25 ;
hence (Path_product M) . p = 0. K by A3; :: thesis: verum

end;

end;