let n be Nat; :: thesis: for K being Field
for M being Lower_Triangular_Matrix of n,K holds Det M = the multF of K $$ (diagonal_of_Matrix M)
let K be Field; :: thesis: for M being Lower_Triangular_Matrix of n,K holds Det M = the multF of K $$ (diagonal_of_Matrix M)
let M be Lower_Triangular_Matrix of n,K; :: thesis: Det M = the multF of K $$ (diagonal_of_Matrix M)
A1: Det M = Det (M @ ) by MATRIXR2:43;
M @ is Upper_Triangular_Matrix of n,K by Th2;
hence Det M = the multF of K $$ (diagonal_of_Matrix (M @ )) by A1, Th7
.= the multF of K $$ (diagonal_of_Matrix M) by Th3 ;
:: thesis: verum