let n be Nat; :: thesis: for K being Field
for M being Matrix of
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
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 ; :: 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 that
A1: rng nt = rng nt' and
A2: 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 S1' = Segm M,nt,nt1';
set S' = Segm M,nt',nt1';
set S = 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 A3: ( 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 A4: Det (Segm M,nt,nt1) = 0. K by Th27, Th31;
( not nt' is without_repeated_line or not nt1' is without_repeated_line ) by A1, A2, A3, Lm1;
hence ( Det (Segm M,nt,nt1) = Det (Segm M,nt',nt1') or Det (Segm M,nt,nt1) = - (Det (Segm M,nt',nt1')) ) by A4, Th27, Th31; :: thesis: verum

end;

suppose A5: ( 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 nt1' is without_repeated_line by A2, Lm1;
then consider perm1 being Permutation of Seg n such that
A6: nt1 = nt1' * perm1 by A2, A5, Th32;
nt' is without_repeated_line by A1, A5, Lm1;
then consider perm being Permutation of Seg n such that
A7: nt = nt' * perm by A1, A5, 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 A8: 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 by A6, Th35;
then A9: Det (Segm M,nt,nt1) = Det (Segm M,nt,nt1') by A8, MATRIX_2:def 16;
Det (Segm M,nt,nt1') = - (Det (Segm M,nt',nt1')),perm by A7, Th35;
hence ( Det (Segm M,nt,nt1) = Det (Segm M,nt',nt1') or Det (Segm M,nt,nt1) = - (Det (Segm M,nt',nt1')) ) by A9, MATRIX_2:def 16; :: thesis: verum

end;

suppose A10: 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')),perm by A7, Th35;
then A11: ( Det (Segm M,nt,nt1') = Det (Segm M,nt',nt1') or Det (Segm M,nt,nt1') = - (Det (Segm M,nt',nt1')) ) by MATRIX_2:def 16;
Det (Segm M,nt,nt1) = - (Det (Segm M,nt,nt1')),perm1 by A6, Th35;
then Det (Segm M,nt,nt1) = - (Det (Segm M,nt,nt1')) by A10, 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 A11, 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;