theorem Th7: :: MATRIX13:7
for n being Nat
for K being Field
for M being upper_triangular Matrix of n,K holds Det M = the multF of K $$ (diagonal_of_Matrix M)