let n be Nat; :: thesis:
let K be Field; :: thesis:
let M be Matrix of n,K; :: thesis:
let R be Element of Permutations n; :: thesis:
assume that
A1: R = Rev (idseq n) and
A2: ( for i, j being Nat st i in Seg n & j in Seg n & i + j <= n holds
M * (i,j) = 0. K or for i, j being Nat st i in Seg n & j in Seg n & i + j > n + 1 holds
M * (i,j) = 0. K ) ; :: thesis:
set mm = the multF of K;
idseq n is Element of (Group_of_Perm n) by MATRIX_1:11;
then reconsider I = idseq n as Element of Permutations n by MATRIX_1:def 13;
set X = Seg n;
reconsider r = Rev (idseq n) as Permutation of (Seg n) by A1, MATRIX_1:def 12;
set Mr = M * r;
set PR = Path_matrix (R,M);
set PI = Path_matrix (I,(M * r));
A3: len (Path_matrix (R,M)) = n by MATRIX_3:def 7;
A4: len (Path_matrix (I,(M * r))) = n by MATRIX_3:def 7;

A5: now :: thesis:

per cases ;

suppose A6: n < 1 ; :: thesis:

then A7: Path_matrix (R,M) = {} by A3, NAT_1:14;
Path_matrix (I,(M * r)) = {} by A4, A6, NAT_1:14;
hence the multF of K "**" (Path_matrix (I,(M * r))) = the multF of K "**" (Path_matrix (R,M)) by A7; :: thesis:

end;

suppose A8: n >= 1 ; :: thesis:

rng I = Seg n ;
then A9: rng (Rev (idseq n)) = Seg n by FINSEQ_5:57;
reconsider PRR = (Path_matrix (R,M)) * R as FinSequence of K by A3, A8, MATRIX_7:34;
A10: dom r = Seg n by FUNCT_2:52;
dom (Path_matrix (R,M)) = Seg n by A3, FINSEQ_1:def 3;
then A11: dom PRR = dom R by A1, A9, RELAT_1:27;

A12: now :: thesis:

A13: dom (Path_matrix (R,M)) = Seg n by A3, FINSEQ_1:def 3;
A14: dom (Path_matrix (I,(M * r))) = Seg n by A4, FINSEQ_1:def 3;
let k be Nat; :: thesis:
assume that
A15: 1 <= k and
A16: k <= len (Path_matrix (I,(M * r))) ; :: thesis:
A17: k in Seg n by A4, A15, A16;
then A18: (n - k) + 1 in Seg n by FINSEQ_5:2;
I . k = k by A17, FUNCT_1:17;
then A19: (Path_matrix (I,(M * r))) . k = (M * r) * (k,k) by A17, A14, MATRIX_3:def 7;
A20: len (idseq n) = n by CARD_1:def 7;
then r . k = I . ((n - k) + 1) by A10, A17, FINSEQ_5:def 3;
then A21: r . k = (n - k) + 1 by A18, FUNCT_1:17;
A22: Indices M = [:(Seg n),(Seg n):] by MATRIX_0:24;
then [k,k] in Indices M by A17, ZFMISC_1:87;
then consider m being Nat such that
A23: r . k = m and
A24: [m,k] in Indices M and
A25: (M * r) * (k,k) = M * (m,k) by MATRIX11:37;
A26: m in Seg n by A22, A24, ZFMISC_1:87;
then A27: (n - m) + 1 in Seg n by FINSEQ_5:2;
r . m = I . ((n - m) + 1) by A10, A20, A26, FINSEQ_5:def 3;
then A28: R . m = k by A1, A23, A27, A21, FUNCT_1:17;
m in Seg n by A22, A24, ZFMISC_1:87;
then (Path_matrix (R,M)) . m = M * (m,k) by A13, A28, MATRIX_3:def 7;
hence (Path_matrix (I,(M * r))) . k = PRR . k by A1, A11, A10, A17, A23, A25, A19, FUNCT_1:12; :: thesis:

end;

n is Element of NAT by ORDINAL1:def 12;
then len PRR = n by A1, A11, A10, FINSEQ_1:def 3;
hence the multF of K "**" (Path_matrix (I,(M * r))) = the multF of K "**" (Path_matrix (R,M)) by A4, A3, A8, A12, FINSEQ_1:14, MATRIX_7:33; :: thesis:

end;

end;

end;

( M * r is upper_triangular Matrix of n,K or M * r is lower_triangular Matrix of n,K ) by A2, Th12, Th13;
then A29: the multF of K $$ (diagonal_of_Matrix (M * r)) = Det (M * r) by Th7, Th8
.= - ((Det M),R) by A1, MATRIX11:46 ;
then A30: - ((Det M),R) = the multF of K $$ (Path_matrix (R,M)) by A5, Th6;

per cases ;

suppose R is even ; :: thesis:

then - ((Det M),R) = Det M by MATRIX_1:def 16;
hence Det M = - (( the multF of K "**" (Path_matrix (R,M))),R) by A5, A29, Th6; :: thesis:

end;

suppose A31: R is odd ; :: thesis:

then A32: - (( the multF of K "**" (Path_matrix (R,M))),R) = - ( the multF of K "**" (Path_matrix (R,M))) by MATRIX_1:def 16;
- ((Det M),R) = - (Det M) by A31, MATRIX_1:def 16;
then (- (( the multF of K "**" (Path_matrix (R,M))),R)) + (- (Det M)) = 0. K by A30, A32, VECTSP_1:19;
hence Det M = - (( the multF of K "**" (Path_matrix (R,M))),R) by VECTSP_1:19; :: thesis:

end;

end;