let n be Nat; :: thesis: for K being Field
for M being Matrix of n,K
for M1, M2 being upper_triangular Matrix of n,K st M = M1 * M2 holds
( M is upper_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 upper_triangular Matrix of n,K st M = M1 * M2 holds
( M is upper_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 upper_triangular Matrix of n,K st M = M1 * M2 holds
( M is upper_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 upper_triangular Matrix of n,K; :: thesis: ( M = M1 * M2 implies ( M is upper_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 upper_triangular Matrix of n,K & diagonal_of_Matrix M = mlt ((diagonal_of_Matrix M1),(diagonal_of_Matrix M2)) )
set SS = [:(Seg n),(Seg n):];
set KK = the carrier of K;
A2: len M2 = n by MATRIX_0:24;
A3: width M1 = n by MATRIX_0:24;

now :: thesis: for i, j being Nat st [i,j] in Indices M & i > j holds
0. K = M * (i,j)

set n0 = n |-> (0. K);
let i, j be Nat; :: thesis: ( [i,j] in Indices M & i > j implies 0. K = M * (i,j) )
assume that
A4: [i,j] in Indices M and
A5: i > j ; :: thesis: 0. K = M * (i,j)
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_0:24;
set m = mlt (L9,C9);
A6: len (mlt (L9,C9)) = n by CARD_1:def 7;

A7: now :: thesis: for k being Nat st 1 <= k & k <= n holds
(mlt (L9,C9)) . k = (n |-> (0. K)) . k

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

per cases ( k <= j or k > j ) ;

suppose k <= j ; :: thesis: (mlt (L9,C9)) . b₁ = (n |-> (0. K)) . b₁

then k < i by A5, XXREAL_0:2;
then A21: M1 * (i,k) = 0. K by A16, MATRIX_1:def 8;
(mlt (L9,C9)) . k = (M1 * (i,k)) * (M2 * (k,j)) by A14, A20, A18, A19, FVSUM_1:60;
hence (mlt (L9,C9)) . k = (n |-> (0. K)) . k by A11, A21; :: thesis: verum

end;

suppose k > j ; :: thesis: (mlt (L9,C9)) . b₁ = (n |-> (0. K)) . b₁

then A22: M2 * (k,j) = 0. K by A17, MATRIX_1:def 8;
(mlt (L9,C9)) . k = (M1 * (i,k)) * (M2 * (k,j)) by A14, A20, A18, A19, FVSUM_1:60;
hence (mlt (L9,C9)) . k = (n |-> (0. K)) . k by A11, A22; :: thesis: verum

end;

end;

end;

len (n |-> (0. K)) = n by CARD_1:def 7;
then mlt (L9,C9) = n |-> (0. K) by A6, A7;
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: verum

end;

hence M is upper_triangular Matrix of n,K by MATRIX_1:def 8; :: thesis: diagonal_of_Matrix M = mlt ((diagonal_of_Matrix M1),(diagonal_of_Matrix M2))
set D2 = diagonal_of_Matrix M2;
set D1 = diagonal_of_Matrix M1;
set DM = diagonal_of_Matrix M;
A23: 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 A23, FINSEQ_2:92;
set m = mlt (D19,D29);
A24: len (mlt (D19,D29)) = n by CARD_1:def 7;

A25: now :: thesis: for i being Nat st 1 <= i & i <= n holds
(mlt (D19,D29)) . i = (diagonal_of_Matrix M) . i

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

A39: i in Seg n by A26, A27;
let j be Nat; :: thesis: ( j in Seg n implies ( ( j <> i implies (mlt (L9,C9)) . j = 0. K ) & ( j = i implies (mlt (L9,C9)) . j = (mlt (D19,D29)) . i ) ) )
assume A40: j in Seg n ; :: thesis: ( ( j <> i implies (mlt (L9,C9)) . j = 0. K ) & ( j = i implies (mlt (L9,C9)) . j = (mlt (D19,D29)) . i ) )
A41: (Line (M1,i)) . j = M1 * (i,j) by A3, A40, MATRIX_0:def 7;
Indices M1 = [:(Seg n),(Seg n):] by MATRIX_0:24;
then A42: [i,j] in Indices M1 by A40, A39, ZFMISC_1:87;
dom M2 = Seg n by A2, FINSEQ_1:def 3;
then A43: (Col (M2,i)) . j = M2 * (j,i) by A40, MATRIX_0:def 8;
Indices M2 = [:(Seg n),(Seg n):] by MATRIX_0:24;
then A44: [j,i] in Indices M2 by A40, A39, ZFMISC_1:87;

per cases ( i <> j or i = j ) ;

suppose A45: i <> j ; :: thesis: ( ( j <> i implies (mlt (L9,C9)) . j = 0. K ) & ( j = i implies (mlt (L9,C9)) . j = (mlt (D19,D29)) . i ) )

then ( i < j or j < i ) by XXREAL_0:1;
then A46: ( M1 * (i,j) = 0. K or M2 * (j,i) = 0. K ) by A42, A44, MATRIX_1:def 8;
(mlt (L9,C9)) . j = (M1 * (i,j)) * (M2 * (j,i)) by A40, A41, A43, FVSUM_1:61;
hence ( ( j <> i implies (mlt (L9,C9)) . j = 0. K ) & ( j = i implies (mlt (L9,C9)) . j = (mlt (D19,D29)) . i ) ) by A45, A46; :: thesis: verum

end;

suppose i = j ; :: thesis: ( ( j <> i implies (mlt (L9,C9)) . j = 0. K ) & ( j = i implies (mlt (L9,C9)) . j = (mlt (D19,D29)) . i ) )

hence ( ( j <> i implies (mlt (L9,C9)) . j = 0. K ) & ( j = i implies (mlt (L9,C9)) . j = (mlt (D19,D29)) . i ) ) by A37, A40, A41, A43, FVSUM_1:61; :: thesis: verum

end;

end;

end;

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

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A48: S₁[k] ; :: thesis: S₁[k + 1]
set k1 = k + 1;
assume that
A49: 1 <= k + 1 and
A50: k + 1 <= n ; :: thesis: ( ( k + 1 < i implies f . (k + 1) = 0. K ) & ( k + 1 >= i implies f . (k + 1) = (mlt (D19,D29)) . i ) )
A51: k + 1 in Seg n by A49, A50;

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

suppose k = 0 ; :: thesis: ( ( k + 1 < i implies f . (k + 1) = 0. K ) & ( k + 1 >= i implies f . (k + 1) = (mlt (D19,D29)) . i ) )

then ( ( f . (k + 1) = 0. K & k + 1 < i ) or ( f . (k + 1) = (mlt (L9,C9)) . (k + 1) & k + 1 = i ) ) by A26, A38, A34, A51, XXREAL_0:1;
hence ( ( k + 1 < i implies f . (k + 1) = 0. K ) & ( k + 1 >= i implies f . (k + 1) = (mlt (D19,D29)) . i ) ) by A38, A51; :: thesis: verum

end;

suppose A52: k > 0 ; :: thesis: ( ( k + 1 < i implies f . (k + 1) = 0. K ) & ( k + 1 >= i implies f . (k + 1) = (mlt (D19,D29)) . i ) )

k < n by A50, NAT_1:13;
then A53: f . (k + 1) = the addF of K . ((f . k),((mlt (L9,C9)) . (k + 1))) by A35, A52;

per cases ( k + 1 < i or k + 1 = i or k + 1 > i ) by XXREAL_0:1;

suppose A54: k + 1 < i ; :: thesis: ( ( k + 1 < i implies f . (k + 1) = 0. K ) & ( k + 1 >= i implies f . (k + 1) = (mlt (D19,D29)) . i ) )

then f . (k + 1) = (0. K) + (0. K) by A38, A48, A50, A51, A52, A53, NAT_1:13, NAT_1:14;
hence ( ( k + 1 < i implies f . (k + 1) = 0. K ) & ( k + 1 >= i implies f . (k + 1) = (mlt (D19,D29)) . i ) ) by A54, RLVECT_1:def 4; :: thesis: verum

end;

suppose A55: k + 1 = i ; :: thesis: ( ( k + 1 < i implies f . (k + 1) = 0. K ) & ( k + 1 >= i implies f . (k + 1) = (mlt (D19,D29)) . i ) )

then f . (k + 1) = (0. K) + ((M1 * (i,i)) * (M2 * (i,i))) by A37, A38, A48, A50, A51, A52, A53, NAT_1:13, NAT_1:14;
hence ( ( k + 1 < i implies f . (k + 1) = 0. K ) & ( k + 1 >= i implies f . (k + 1) = (mlt (D19,D29)) . i ) ) by A37, A55, RLVECT_1:def 4; :: thesis: verum

end;

suppose A56: k + 1 > i ; :: thesis: ( ( k + 1 < i implies f . (k + 1) = 0. K ) & ( k + 1 >= i implies f . (k + 1) = (mlt (D19,D29)) . i ) )

then f . (k + 1) = ((M1 * (i,i)) * (M2 * (i,i))) + (0. K) by A37, A38, A48, A50, A51, A52, A53, NAT_1:13, NAT_1:14;
hence ( ( k + 1 < i implies f . (k + 1) = 0. K ) & ( k + 1 >= i implies f . (k + 1) = (mlt (D19,D29)) . i ) ) by A37, A56, RLVECT_1:def 4; :: thesis: verum

end;

end;

end;

end;

end;

A57: 1 <= n by A26, A27, NAT_1:14;
A58: S₁[ 0 ] ;
for k being Nat holds S₁[k] from NAT_1:sch 2(A58, A47);
hence (mlt (D19,D29)) . i = (diagonal_of_Matrix M) . i by A27, A36, A57; :: thesis: verum

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 A24, A25; :: thesis: verum