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

Det M = 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

Det M = 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 Det M = 0. K )

assume A1: 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: Det M = 0. K

set f = Path_product M;

set F = the addF of K;

Det M = the addF of K $$ ((In ((Permutations n),(Fin (Permutations n)))),(Path_product M)) by MATRIX_3:def 9

.= 0. K by A1, Th51 ;

hence Det M = 0. K ; :: thesis: verum

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

Det M = 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

Det M = 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 Det M = 0. K )

assume A1: 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: Det M = 0. K

set f = Path_product M;

set F = the addF of K;

Det M = the addF of K $$ ((In ((Permutations n),(Fin (Permutations n)))),(Path_product M)) by MATRIX_3:def 9

.= 0. K by A1, Th51 ;

hence Det M = 0. K ; :: thesis: verum