theorem Th12: :: MATRIX13:12

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 holds
M * (i,j) = 0. K ) holds
M * R is upper_triangular Matrix of n,K