theorem Th5: :: MATRIX13:5
for n being Nat
for K being Field
for M being Matrix of n,K
for perm being Element of Permutations n st perm <> idseq n & ( M is lower_triangular Matrix of n,K or M is upper_triangular Matrix of n,K ) holds
(Path_product M) . perm = 0. K