theorem Th13: :: MATRIX13:13

for n being Nat
for K being Field
for M being Matrix of n,K
for R being Permutation of (Seg n) st R = Rev (idseq n) & ( 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
M * R is lower_triangular Matrix of n,K