let n be Nat; :: thesis:
let K be Field; :: thesis:
let M be Matrix of n,K; :: thesis:
reconsider N = n as Element of NAT by ORDINAL1:def 12;
let M1, M2 be Upper_Triangular_Matrix of n,K; :: thesis:
assume A1: M = M1 * M2 ; :: thesis:
set SS = [:(Seg n),(Seg n):];
set KK = the carrier of K;
A2: len M2 = n by MATRIX_1:24;
A3: width M1 = n by MATRIX_1:24;

set n0 = n |-> (0. K);
let i, j be Nat; :: thesis:
assume that
A4: [i,j] in Indices M and
A5: i > j ; :: thesis:
set C = Col (M2,j);
set L = Line (M1,i);
reconsider L9 = Line (M1,i), C9 = Col (M2,j) as Element of N -tuples_on the carrier of K by MATRIX_1:24;
set m = mlt (L9,C9);
A6: len (mlt (L9,C9)) = n by CARD_1:def 7;

A7: now

let k be Nat; :: thesis:
assume that
A8: 1 <= k and
A9: k <= n ; :: thesis:
A10: k in NAT by ORDINAL1:def 12;
then A11: k in Seg n by A8, A9;
then A12: (n |-> (0. K)) . k = 0. K by FINSEQ_2:57;
A13: Indices M2 = [:(Seg n),(Seg n):] by MATRIX_1:24;
A14: Indices M1 = [:(Seg n),(Seg n):] by MATRIX_1:24;
A15: (Line (M1,i)) . k = M1 * (i,k) by A3, A11, MATRIX_1:def 7;
A16: Indices M = [:(Seg n),(Seg n):] by MATRIX_1:24;
then i in Seg n by A4, ZFMISC_1:87;
then A17: [i,k] in Indices M1 by A11, A14, ZFMISC_1:87;
j in Seg n by A4, A16, ZFMISC_1:87;
then A18: [k,j] in Indices M2 by A11, A13, ZFMISC_1:87;
A19: dom (mlt (L9,C9)) = Seg n by A6, FINSEQ_1:def 3;
A20: k in Seg n by A8, A9, A10;
dom M2 = Seg n by A2, FINSEQ_1:def 3;
then A21: (Col (M2,j)) . k = M2 * (k,j) by A11, MATRIX_1:def 8;

per cases ;

suppose k <= j ; :: thesis:

then k (0. K)) . k by A12, A22, VECTSP_1:12; :: thesis:

end;

suppose k > j ; :: thesis:

then A23: M2 * (k,j) = 0. K by A18, MATRIX_2:def 3;
(mlt (L9,C9)) . k = (M1 * (i,k)) * (M2 * (k,j)) by A15, A21, A19, A20, FVSUM_1:60;
hence (mlt (L9,C9)) . k = (n |-> (0. K)) . k by A12, A23, VECTSP_1:12; :: thesis:

end;

len (n |-> (0. K)) = n by CARD_1:def 7;
then mlt (L9,C9) = n |-> (0. K) by A6, A7, FINSEQ_1:14;
hence 0. K = (Line (M1,i)) "*" (Col (M2,j)) by MATRIX_3:11
.= M * (i,j) by A1, A3, A2, A4, MATRIX_3:def 4 ;
:: thesis:

end;

hence M is Upper_Triangular_Matrix of n,K by MATRIX_2:def 3; :: thesis:
set D2 = diagonal_of_Matrix M2;
set D1 = diagonal_of_Matrix M1;
set DM = diagonal_of_Matrix M;
A24: len (diagonal_of_Matrix M2) = n by MATRIX_3:def 10;
len (diagonal_of_Matrix M1) = n by MATRIX_3:def 10;
then reconsider D19 = diagonal_of_Matrix M1, D29 = diagonal_of_Matrix M2 as Element of N -tuples_on the carrier of K by A24, FINSEQ_2:92;
set m = mlt (D19,D29);
A25: len (mlt (D19,D29)) = n by CARD_1:def 7;

A26: now

set aa = the addF of K;
let i be Nat; :: thesis:
assume that
A27: 1 <= i and
A28: i <= n ; :: thesis:
i in NAT by ORDINAL1:def 12;
then A29: i in Seg n by A27, A28;
then A30: (diagonal_of_Matrix M) . i = M * (i,i) by MATRIX_3:def 10;
set C = Col (M2,i);
set L = Line (M1,i);
reconsider L9 = Line (M1,i), C9 = Col (M2,i) as Element of N -tuples_on the carrier of K by MATRIX_1:24;
set mLC = mlt (L9,C9);
A31: the addF of K is having_a_unity by FVSUM_1:8;
Indices M = [:(Seg n),(Seg n):] by MATRIX_1:24;
then [i,i] in Indices M by A29, ZFMISC_1:87;
then A32: (diagonal_of_Matrix M) . i = (Line (M1,i)) "*" (Col (M2,i)) by A1, A3, A2, A30, MATRIX_3:def 4;
A33: (diagonal_of_Matrix M2) . i = M2 * (i,i) by A29, MATRIX_3:def 10;
A34: (diagonal_of_Matrix M1) . i = M1 * (i,i) by A29, MATRIX_3:def 10;
len (mlt (L9,C9)) = n by CARD_1:def 7;
then consider f being Function of NAT, the carrier of K such that
A35: f . 1 = (mlt (L9,C9)) . 1 and
A36: for k being Element of NAT st 0 <> k & k < n holds
f . (k + 1) = the addF of K . ((f . k),((mlt (L9,C9)) . (k + 1))) and
A37: (diagonal_of_Matrix M) . i = f . n by A27, A28, A32, A31, FINSOP_1:def 1;
defpred S₁[ Nat] means ( 1 <= $1 & $1 <= n implies ( ( $1 = i implies f . $1 = (mlt (D19,D29)) . i ) ) );
i in dom (mlt (D19,D29)) by A25, A29, FINSEQ_1:def 3;
then A38: (mlt (D19,D29)) . i = (M1 * (i,i)) * (M2 * (i,i)) by A34, A33, FVSUM_1:60;
A39: for j being Nat st j in Seg n holds
( ( j <> i implies (mlt (L9,C9)) . j = 0. K ) & ( j = i implies (mlt (L9,C9)) . j = (mlt (D19,D29)) . i ) )

proof

i in NAT by ORDINAL1:def 12;
then A40: i in Seg n by A27, A28;
let j be Nat; :: thesis:
assume A41: j in Seg n ; :: thesis:
A42: (Line (M1,i)) . j = M1 * (i,j) by A3, A41, MATRIX_1:def 7;
Indices M1 = [:(Seg n),(Seg n):] by MATRIX_1:24;
then A43: [i,j] in Indices M1 by A41, A40, ZFMISC_1:87;
dom M2 = Seg n by A2, FINSEQ_1:def 3;
then A44: (Col (M2,i)) . j = M2 * (j,i) by A41, MATRIX_1:def 8;
Indices M2 = [:(Seg n),(Seg n):] by MATRIX_1:24;
then A45: [j,i] in Indices M2 by A41, A40, ZFMISC_1:87;

per cases ;

suppose A46: i <> j ; :: thesis:

then ( i < j or j i implies (mlt (L9,C9)) . j = 0. K ) & ( j = i implies (mlt (L9,C9)) . j = (mlt (D19,D29)) . i ) ) by A46, A47, VECTSP_1:12; :: thesis:

end;

suppose i = j ; :: thesis:

hence ( ( j <> i implies (mlt (L9,C9)) . j = 0. K ) & ( j = i implies (mlt (L9,C9)) . j = (mlt (D19,D29)) . i ) ) by A38, A41, A42, A44, FVSUM_1:61; :: thesis:

end;

A48: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis:
assume A49: S₁[k] ; :: thesis:
set k1 = k + 1;
assume that
A50: 1 <= k + 1 and
A51: k + 1 <= n ; :: thesis:
A52: k + 1 in Seg n by A50, A51;

per cases ;

suppose k = 0 ; :: thesis:

then ( ( f . (k + 1) = 0. K & k + 1 = i implies f . (k + 1) = (mlt (D19,D29)) . i ) ) by A39, A52; :: thesis:

end;

suppose A53: k > 0 ; :: thesis:

A54: k in NAT by ORDINAL1:def 12;
k < n by A51, NAT_1:13;
then A55: f . (k + 1) = the addF of K . ((f . k),((mlt (L9,C9)) . (k + 1))) by A36, A53, A54;

per cases by XXREAL_0:1;

suppose A56: k + 1 < i ; :: thesis:

then f . (k + 1) = (0. K) + (0. K) by A39, A49, A51, A52, A53, A55, NAT_1:13, NAT_1:14;
hence ( ( k + 1 = i implies f . (k + 1) = (mlt (D19,D29)) . i ) ) by A56, RLVECT_1:def 4; :: thesis:

end;

suppose A57: k + 1 = i ; :: thesis:

then f . (k + 1) = (0. K) + ((M1 * (i,i)) * (M2 * (i,i))) by A38, A39, A49, A51, A52, A53, A55, NAT_1:13, NAT_1:14;
hence ( ( k + 1 = i implies f . (k + 1) = (mlt (D19,D29)) . i ) ) by A38, A57, RLVECT_1:def 4; :: thesis:

end;

suppose A58: k + 1 > i ; :: thesis:

then f . (k + 1) = ((M1 * (i,i)) * (M2 * (i,i))) + (0. K) by A38, A39, A49, A51, A52, A53, A55, NAT_1:13, NAT_1:14;
hence ( ( k + 1 = i implies f . (k + 1) = (mlt (D19,D29)) . i ) ) by A38, A58, RLVECT_1:def 4; :: thesis:

end;

A59: 1 <= n by A27, A28, NAT_1:14;
A60: S₁[ 0 ] ;
for k being Nat holds S₁[k] from NAT_1:sch 2(A60, A48);
hence (mlt (D19,D29)) . i = (diagonal_of_Matrix M) . i by A28, A37, A59; :: thesis:

end;

len (diagonal_of_Matrix M) = n by MATRIX_3:def 10;
hence diagonal_of_Matrix M = mlt ((diagonal_of_Matrix M1),(diagonal_of_Matrix M2)) by A25, A26, FINSEQ_1:14; :: thesis: