let n be Nat; :: thesis: for K being Field
for M being Matrix of n,K
for perm being Element of Permutations n
for Perm being Permutation of (Seg n) st perm = Perm holds
Det (M * Perm) = - (Det M),perm
let K be Field; :: thesis: for M being Matrix of n,K
for perm being Element of Permutations n
for Perm being Permutation of (Seg n) st perm = Perm holds
Det (M * Perm) = - (Det M),perm
let M be Matrix of n,K; :: thesis: for perm being Element of Permutations n
for Perm being Permutation of (Seg n) st perm = Perm holds
Det (M * Perm) = - (Det M),perm
let perm be Element of Permutations n; :: thesis: for Perm being Permutation of (Seg n) st perm = Perm holds
Det (M * Perm) = - (Det M),perm
let Perm be Permutation of (Seg n); :: thesis: ( perm = Perm implies Det (M * Perm) = - (Det M),perm )
assume A1: Perm = perm ; :: thesis: Det (M * Perm) = - (Det M),perm

per cases ( n < 2 or n >= 2 ) ;

suppose A2: n < 2 ; :: thesis: Det (M * Perm) = - (Det M),perm

then perm = idseq n by Lm3;
then A3: M * perm = M by Th39;
perm is even by A2, Lm3;
hence Det (M * Perm) = - (Det M),perm by A1, A3, MATRIX_2:def 16; :: thesis: verum

end;

suppose n >= 2 ; :: thesis: Det (M * Perm) = - (Det M),perm

then reconsider n2 = n - 2 as Nat by NAT_1:21;
reconsider M9 = M as Matrix of n2 + 2,K ;
reconsider Perm2 = Perm as Permutation of (Seg (n2 + 2)) ;
reconsider perm2 = perm as Element of Permutations (n2 + 2) ;
Det (M9 * Perm2) = (sgn perm2,K) * (Det M9) by A1, Th45;
hence Det (M * Perm) = - (Det M),perm by Th26; :: thesis: verum

end;

end;