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_2:23;
then reconsider I = idseq n as Element of Permutations n by MATRIX_2:def 13;
set X = Seg n;
reconsider r = Rev (idseq n) as Permutation of (Seg n) by A1, MATRIX_2:def 11;
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

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 by RELAT_1:71;
then A9: rng (Rev (idseq n)) = Seg n by FINSEQ_5:60;
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:67;
dom (Path_matrix R,M) = Seg n by A3, FINSEQ_1:def 3;
then A11: dom PRR = dom R by A1, A9, RELAT_1:46;

A12: now

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:
k in NAT by ORDINAL1:def 13;
then 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:34;
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 FINSEQ_1:def 18;
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:34;
A22: Indices M = [:(Seg n),(Seg n):] by MATRIX_1:25;
then [k,k] in Indices M by A17, ZFMISC_1:106;
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:106;
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:34;
m in Seg n by A22, A24, ZFMISC_1:106;
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:22; :: thesis:

end;

n is Element of NAT by ORDINAL1:def 13;
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:18, 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_2:def 16;
hence Det M = - (the multF of K "**" (Path_matrix R,M)),R by A5, A29, Th6; :: thesis:

end;

suppose A31: not R is even ; :: thesis:

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

end;

end;