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 12;
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_0:24;
A3: len M2 = n by MATRIX_0:24;
A4: width M1 = n by MATRIX_0:24;

A5: now :: thesis: M @ = (M2 @) * (M1 @)

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

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

then len ((M2 @) * (M1 @)) = 0 by MATRIX_0:24;
then A7: (M2 @) * (M1 @) = {} ;
len (M @) = 0 by A6, MATRIX_0:24;
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:22; :: 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:92;
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:63 ;
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