theorem :: MATRIX13:14

for n being Nat
for K being Field
for M being Matrix of n,K
for R being Element of Permutations n st R = Rev (idseq n) & ( 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 ) holds
Det M = - (( the multF of K "**" (Path_matrix (R,M))),R)