for n being Nat
for K being commutative Ring st not K is degenerated & K is well-unital & K is domRing-like holds
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)