theorem Th49: :: MATRIX_9:49

for n being Nat
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 )