theorem Th50: :: MATRIX_9:50

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