let n be Nat; :: thesis: for K being Field
for M being Matrix of K
for nt, nt1, nt9, nt19 being Element of n -tuples_on NAT st rng nt = rng nt9 & rng nt1 = rng nt19 & not Det (Segm M,nt,nt1) = Det (Segm M,nt9,nt19) holds
Det (Segm M,nt,nt1) = - (Det (Segm M,nt9,nt19))
let K be Field; :: thesis: for M being Matrix of K
for nt, nt1, nt9, nt19 being Element of n -tuples_on NAT st rng nt = rng nt9 & rng nt1 = rng nt19 & not Det (Segm M,nt,nt1) = Det (Segm M,nt9,nt19) holds
Det (Segm M,nt,nt1) = - (Det (Segm M,nt9,nt19))
let M be Matrix of K; :: thesis: for nt, nt1, nt9, nt19 being Element of n -tuples_on NAT st rng nt = rng nt9 & rng nt1 = rng nt19 & not Det (Segm M,nt,nt1) = Det (Segm M,nt9,nt19) holds
Det (Segm M,nt,nt1) = - (Det (Segm M,nt9,nt19))
let nt, nt1, nt9, nt19 be Element of n -tuples_on NAT ; :: thesis: ( rng nt = rng nt9 & rng nt1 = rng nt19 & not Det (Segm M,nt,nt1) = Det (Segm M,nt9,nt19) implies Det (Segm M,nt,nt1) = - (Det (Segm M,nt9,nt19)) )
assume that
A1: rng nt = rng nt9 and
A2: rng nt1 = rng nt19 ; :: thesis: ( Det (Segm M,nt,nt1) = Det (Segm M,nt9,nt19) or Det (Segm M,nt,nt1) = - (Det (Segm M,nt9,nt19)) )
set S19 = Segm M,nt,nt19;
set S9 = Segm M,nt9,nt19;
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,nt9,nt19) or Det (Segm M,nt,nt1) = - (Det (Segm M,nt9,nt19)) )

then A4: Det (Segm M,nt,nt1) = 0. K by Th27, Th31;
( not nt9 is without_repeated_line or not nt19 is without_repeated_line ) by A1, A2, A3, Lm1;
hence ( Det (Segm M,nt,nt1) = Det (Segm M,nt9,nt19) or Det (Segm M,nt,nt1) = - (Det (Segm M,nt9,nt19)) ) 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,nt9,nt19) or Det (Segm M,nt,nt1) = - (Det (Segm M,nt9,nt19)) )

then nt19 is without_repeated_line by A2, Lm1;
then consider perm1 being Permutation of (Seg n) such that
A6: nt1 = nt19 * perm1 by A2, A5, Th32;
nt9 is without_repeated_line by A1, A5, Lm1;
then consider perm being Permutation of (Seg n) such that
A7: nt = nt9 * 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,nt9,nt19) or Det (Segm M,nt,nt1) = - (Det (Segm M,nt9,nt19)) )

Det (Segm M,nt,nt1) = - (Det (Segm M,nt,nt19)),perm1 by A6, Th35;
then A9: Det (Segm M,nt,nt1) = Det (Segm M,nt,nt19) by A8, MATRIX_2:def 16;
Det (Segm M,nt,nt19) = - (Det (Segm M,nt9,nt19)),perm by A7, Th35;
hence ( Det (Segm M,nt,nt1) = Det (Segm M,nt9,nt19) or Det (Segm M,nt,nt1) = - (Det (Segm M,nt9,nt19)) ) by A9, MATRIX_2:def 16; :: thesis: verum

end;

suppose A10: not perm1 is even ; :: thesis: ( Det (Segm M,nt,nt1) = Det (Segm M,nt9,nt19) or Det (Segm M,nt,nt1) = - (Det (Segm M,nt9,nt19)) )

Det (Segm M,nt,nt19) = - (Det (Segm M,nt9,nt19)),perm by A7, Th35;
then A11: ( Det (Segm M,nt,nt19) = Det (Segm M,nt9,nt19) or Det (Segm M,nt,nt19) = - (Det (Segm M,nt9,nt19)) ) by MATRIX_2:def 16;
Det (Segm M,nt,nt1) = - (Det (Segm M,nt,nt19)),perm1 by A6, Th35;
then Det (Segm M,nt,nt1) = - (Det (Segm M,nt,nt19)) by A10, MATRIX_2:def 16;
then ( Det (Segm M,nt,nt1) = - (Det (Segm M,nt9,nt19)) or Det (Segm M,nt,nt1) = (0. K) + (- (- (Det (Segm M,nt9,nt19)))) ) by A11, RLVECT_1:def 7;
then ( Det (Segm M,nt,nt1) = - (Det (Segm M,nt9,nt19)) or Det (Segm M,nt,nt1) = (0. K) - (- (Det (Segm M,nt9,nt19))) ) ;
then ( Det (Segm M,nt,nt1) = - (Det (Segm M,nt9,nt19)) or (Det (Segm M,nt,nt1)) + (- (Det (Segm M,nt9,nt19))) = 0. K ) by VECTSP_2:22;
hence ( Det (Segm M,nt,nt1) = Det (Segm M,nt9,nt19) or Det (Segm M,nt,nt1) = - (Det (Segm M,nt9,nt19)) ) by VECTSP_1:66; :: thesis: verum

end;

end;

end;

end;