theorem Th45: :: MATRIX11:45

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