theorem Th43: :: MATRIX11:43

for n being Nat
for K being commutative Ring
for M being Matrix of n + 2,K
for perm2 being Element of Permutations (n + 2)
for Perm2 being Permutation of (Seg (n + 2)) st perm2 = Perm2 holds
for p2, q2 being Element of Permutations (n + 2) st q2 = p2 * (Perm2 ") holds
(Path_product M) . q2 = (sgn (perm2,K)) * ((Path_product (M * Perm2)) . p2)