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
() . 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
() . 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
() . 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 () . p = 0. K )

A1: () . 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 2 ;
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: () . p = 0. K
then consider l being Element of NAT such that
A2: l in Seg n and
A3: (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 ;
then A4: Product (Path_matrix (p,M)) = 0. K by ;
per cases ( p is even or p is odd ) ;
suppose p is even ; :: thesis: () . p = 0. K
hence (Path_product M) . p = 0. K by ; :: thesis: verum
end;
suppose p is odd ; :: thesis: () . p = 0. K
then - ((Product (Path_matrix (p,M))),p) = - (Product (Path_matrix (p,M))) by MATRIX_1:def 16
.= 0. K by ;
hence (Path_product M) . p = 0. K by A1; :: thesis: verum
end;
end;