let n be Nat; :: thesis: for K being Field
for M being Matrix of n,K
for M1, M2 being Lower_Triangular_Matrix of n,K st M = M1 * M2 holds
( M is Lower_Triangular_Matrix of n,K & diagonal_of_Matrix M = mlt (diagonal_of_Matrix M1),(diagonal_of_Matrix M2) )
let K be Field; :: thesis: for M being Matrix of n,K
for M1, M2 being Lower_Triangular_Matrix of n,K st M = M1 * M2 holds
( M is Lower_Triangular_Matrix of n,K & diagonal_of_Matrix M = mlt (diagonal_of_Matrix M1),(diagonal_of_Matrix M2) )
let M be Matrix of n,K; :: thesis: for M1, M2 being Lower_Triangular_Matrix of n,K st M = M1 * M2 holds
( M is Lower_Triangular_Matrix of n,K & diagonal_of_Matrix M = mlt (diagonal_of_Matrix M1),(diagonal_of_Matrix M2) )
reconsider N = n as Element of NAT by ORDINAL1:def 13;
let M1, M2 be Lower_Triangular_Matrix of n,K; :: thesis: ( M = M1 * M2 implies ( M is Lower_Triangular_Matrix of n,K & diagonal_of_Matrix M = mlt (diagonal_of_Matrix M1),(diagonal_of_Matrix M2) ) )
assume A1: M = M1 * M2 ; :: thesis: ( M is Lower_Triangular_Matrix of n,K & diagonal_of_Matrix M = mlt (diagonal_of_Matrix M1),(diagonal_of_Matrix M2) )
A2: width M2 = n by MATRIX_1:25;
A3: len M2 = n by MATRIX_1:25;
A4: width M1 = n by MATRIX_1:25;

A5: now

per cases ( n = 0 or n > 0 ) ;

suppose A6: n = 0 ; :: thesis: M @ = (M2 @ ) * (M1 @ )

then len ((M2 @ ) * (M1 @ )) = 0 by MATRIX_1:25;
then A7: (M2 @ ) * (M1 @ ) = {} ;
len (M @ ) = 0 by A6, MATRIX_1:25;
hence M @ = (M2 @ ) * (M1 @ ) by A7; :: thesis: verum

end;

suppose n > 0 ; :: thesis: M @ = (M2 @ ) * (M1 @ )

hence M @ = (M2 @ ) * (M1 @ ) by A1, A4, A2, A3, MATRIX_3:24; :: thesis: verum

end;

end;

end;

set D29 = diagonal_of_Matrix (M2 @ );
set D2 = diagonal_of_Matrix M2;
set D19 = diagonal_of_Matrix (M1 @ );
set D1 = diagonal_of_Matrix M1;
A8: len (diagonal_of_Matrix M2) = n by MATRIX_3:def 10;
len (diagonal_of_Matrix M1) = n by MATRIX_3:def 10;
then reconsider d1 = diagonal_of_Matrix M1, d2 = diagonal_of_Matrix M2 as Element of N -tuples_on the carrier of K by A8, FINSEQ_2:110;
A9: M2 @ is Upper_Triangular_Matrix of n,K by Th2;
A10: M1 @ is Upper_Triangular_Matrix of n,K by Th2;
then diagonal_of_Matrix (M @ ) = mlt (diagonal_of_Matrix (M2 @ )),(diagonal_of_Matrix (M1 @ )) by A5, A9, Th15;
then A11: diagonal_of_Matrix M = mlt (diagonal_of_Matrix (M2 @ )),(diagonal_of_Matrix (M1 @ )) by Th3
.= mlt (diagonal_of_Matrix M2),(diagonal_of_Matrix (M1 @ )) by Th3
.= mlt d2,d1 by Th3
.= mlt (diagonal_of_Matrix M1),(diagonal_of_Matrix M2) by FVSUM_1:77 ;
M @ is Upper_Triangular_Matrix of n,K by A5, A10, A9, Th15;
hence ( M is Lower_Triangular_Matrix of n,K & diagonal_of_Matrix M = mlt (diagonal_of_Matrix M1),(diagonal_of_Matrix M2) ) by A11, Th2; :: thesis: verum