let n be Nat; :: thesis: for K being Field
for M being Matrix of K
for nt, nt1, nt', nt1' being Element of n -tuples_on NAT st rng nt = rng nt' & rng nt1 = rng nt1' & not Det (Segm M,nt,nt1) = Det (Segm M,nt',nt1') holds
Det (Segm M,nt,nt1) = - (Det (Segm M,nt',nt1'))
let K be Field; :: thesis: for M being Matrix of K
for nt, nt1, nt', nt1' being Element of n -tuples_on NAT st rng nt = rng nt' & rng nt1 = rng nt1' & not Det (Segm M,nt,nt1) = Det (Segm M,nt',nt1') holds
Det (Segm M,nt,nt1) = - (Det (Segm M,nt',nt1'))
let M be Matrix of K; :: thesis: for nt, nt1, nt', nt1' being Element of n -tuples_on NAT st rng nt = rng nt' & rng nt1 = rng nt1' & not Det (Segm M,nt,nt1) = Det (Segm M,nt',nt1') holds
Det (Segm M,nt,nt1) = - (Det (Segm M,nt',nt1'))
let nt, nt1, nt', nt1' be Element of n -tuples_on NAT ; :: thesis: ( rng nt = rng nt' & rng nt1 = rng nt1' & not Det (Segm M,nt,nt1) = Det (Segm M,nt',nt1') implies Det (Segm M,nt,nt1) = - (Det (Segm M,nt',nt1')) )
assume A1: ( rng nt = rng nt' & rng nt1 = rng nt1' ) ; :: thesis: ( Det (Segm M,nt,nt1) = Det (Segm M,nt',nt1') or Det (Segm M,nt,nt1) = - (Det (Segm M,nt',nt1')) )
set S = Segm M,nt,nt1;
set S' = Segm M,nt',nt1';
set S1' = Segm M,nt,nt1';

per cases ( not nt is without_repeated_line or not nt1 is without_repeated_line or ( nt is without_repeated_line & nt1 is without_repeated_line ) ) ;

suppose A2: ( not nt is without_repeated_line or not nt1 is without_repeated_line ) ; :: thesis: ( Det (Segm M,nt,nt1) = Det (Segm M,nt',nt1') or Det (Segm M,nt,nt1) = - (Det (Segm M,nt',nt1')) )

then ( not nt' is without_repeated_line or not nt1' is without_repeated_line ) by A1, Lm1;
then ( Det (Segm M,nt,nt1) = 0. K & Det (Segm M,nt',nt1') = 0. K ) by A2, Th27, Th31;
hence ( Det (Segm M,nt,nt1) = Det (Segm M,nt',nt1') or Det (Segm M,nt,nt1) = - (Det (Segm M,nt',nt1')) ) ; :: thesis: verum

end;

suppose A3: ( nt is without_repeated_line & nt1 is without_repeated_line ) ; :: thesis: ( Det (Segm M,nt,nt1) = Det (Segm M,nt',nt1') or Det (Segm M,nt,nt1) = - (Det (Segm M,nt',nt1')) )

then nt' is without_repeated_line by A1, Lm1;
then consider perm being Permutation of (Seg n) such that
A4: nt = nt' * perm by A1, A3, Th32;
nt1' is without_repeated_line by A1, A3, Lm1;
then consider perm1 being Permutation of (Seg n) such that
A5: nt1 = nt1' * perm1 by A1, A3, Th32;
reconsider perm = perm, perm1 = perm1 as Element of Permutations n by MATRIX_2:def 11;

per cases ( perm1 is even or not perm1 is even ) ;

suppose A6: perm1 is even ; :: thesis: ( Det (Segm M,nt,nt1) = Det (Segm M,nt',nt1') or Det (Segm M,nt,nt1) = - (Det (Segm M,nt',nt1')) )

( Det (Segm M,nt,nt1) = - (Det (Segm M,nt,nt1')),perm1 & ( perm is even or not perm is even ) & Det (Segm M,nt,nt1') = - (Det (Segm M,nt',nt1')),perm ) by A4, A5, Th35;
then ( Det (Segm M,nt,nt1) = Det (Segm M,nt,nt1') & ( Det (Segm M,nt,nt1') = Det (Segm M,nt',nt1') or Det (Segm M,nt,nt1') = - (Det (Segm M,nt',nt1')) ) ) by A6, MATRIX_2:def 16;
hence ( Det (Segm M,nt,nt1) = Det (Segm M,nt',nt1') or Det (Segm M,nt,nt1) = - (Det (Segm M,nt',nt1')) ) ; :: thesis: verum

end;

suppose A7: not perm1 is even ; :: thesis: ( Det (Segm M,nt,nt1) = Det (Segm M,nt',nt1') or Det (Segm M,nt,nt1) = - (Det (Segm M,nt',nt1')) )

( Det (Segm M,nt,nt1) = - (Det (Segm M,nt,nt1')),perm1 & ( perm is even or not perm is even ) & Det (Segm M,nt,nt1') = - (Det (Segm M,nt',nt1')),perm ) by A4, A5, Th35;
then ( Det (Segm M,nt,nt1) = - (Det (Segm M,nt,nt1')) & ( Det (Segm M,nt,nt1') = Det (Segm M,nt',nt1') or Det (Segm M,nt,nt1') = - (Det (Segm M,nt',nt1')) ) ) by A7, MATRIX_2:def 16;
then ( Det (Segm M,nt,nt1) = - (Det (Segm M,nt',nt1')) or Det (Segm M,nt,nt1) = (0. K) + (- (- (Det (Segm M,nt',nt1')))) ) by RLVECT_1:def 7;
then ( Det (Segm M,nt,nt1) = - (Det (Segm M,nt',nt1')) or Det (Segm M,nt,nt1) = (0. K) - (- (Det (Segm M,nt',nt1'))) ) ;
then ( Det (Segm M,nt,nt1) = - (Det (Segm M,nt',nt1')) or (Det (Segm M,nt,nt1)) + (- (Det (Segm M,nt',nt1'))) = 0. K ) by VECTSP_2:22;
hence ( Det (Segm M,nt,nt1) = Det (Segm M,nt',nt1') or Det (Segm M,nt,nt1) = - (Det (Segm M,nt',nt1')) ) by VECTSP_1:66; :: thesis: verum

end;

end;

end;

end;