let D be non empty set ; :: thesis: for d being Element of D
for M1, M2 being Matrix of D
for M being Matrix of Sum (Len <*M1,M2*>), Sum (Width <*M1,M2*>),D holds
( M = block_diagonal (<*M1,M2*>,d) iff for i being Nat holds
( ( i in Seg (width M1) implies Col (M,i) = (Col (M1,i)) ^ ((len M2) |-> d) ) & ( i in Seg (width M2) implies Col (M,(i + (width M1))) = ((len M1) |-> d) ^ (Col (M2,i)) ) ) )
let d be Element of D; :: thesis: for M1, M2 being Matrix of D
for M being Matrix of Sum (Len <*M1,M2*>), Sum (Width <*M1,M2*>),D holds
( M = block_diagonal (<*M1,M2*>,d) iff for i being Nat holds
( ( i in Seg (width M1) implies Col (M,i) = (Col (M1,i)) ^ ((len M2) |-> d) ) & ( i in Seg (width M2) implies Col (M,(i + (width M1))) = ((len M1) |-> d) ^ (Col (M2,i)) ) ) )
let M1, M2 be Matrix of D; :: thesis: for M being Matrix of Sum (Len <*M1,M2*>), Sum (Width <*M1,M2*>),D holds
( M = block_diagonal (<*M1,M2*>,d) iff for i being Nat holds
( ( i in Seg (width M1) implies Col (M,i) = (Col (M1,i)) ^ ((len M2) |-> d) ) & ( i in Seg (width M2) implies Col (M,(i + (width M1))) = ((len M1) |-> d) ^ (Col (M2,i)) ) ) )
let M be Matrix of Sum (Len <*M1,M2*>), Sum (Width <*M1,M2*>),D; :: thesis: ( M = block_diagonal (<*M1,M2*>,d) iff for i being Nat holds
( ( i in Seg (width M1) implies Col (M,i) = (Col (M1,i)) ^ ((len M2) |-> d) ) & ( i in Seg (width M2) implies Col (M,(i + (width M1))) = ((len M1) |-> d) ^ (Col (M2,i)) ) ) )
set m12 = <*M1,M2*>;
set B = block_diagonal (<*M1,M2*>,d);
A1: Seg (len M) = dom M by FINSEQ_1:def 3;
A2: Seg (len M1) = dom M1 by FINSEQ_1:def 3;
A3: dom M2 = Seg (len M2) by FINSEQ_1:def 3;
A4: Sum (Len <*M1,M2*>) = (len M1) + (len M2) by Th16;
A5: ( Sum (Len <*M1,M2*>) = 0 implies Sum (Width <*M1,M2*>) = 0 ) by Th13;
then A6: len M = Sum (Len <*M1,M2*>) by MATRIX13:1;
A7: width M = Sum (Width <*M1,M2*>) by A5, MATRIX13:1;
A8: Sum (Width <*M1,M2*>) = (width M1) + (width M2) by Th20;
then width M1 <= width M by A7, NAT_1:12;
then A9: Seg (width M1) c= Seg (width M) by FINSEQ_1:5;
thus ( M = block_diagonal (<*M1,M2*>,d) implies for i being Nat holds
( ( i in Seg (width M1) implies Col (M,i) = (Col (M1,i)) ^ ((len M2) |-> d) ) & ( i in Seg (width M2) implies Col (M,(i + (width M1))) = ((len M1) |-> d) ^ (Col (M2,i)) ) ) ) :: thesis: ( ( for i being Nat holds
( ( i in Seg (width M1) implies Col (M,i) = (Col (M1,i)) ^ ((len M2) |-> d) ) & ( i in Seg (width M2) implies Col (M,(i + (width M1))) = ((len M1) |-> d) ^ (Col (M2,i)) ) ) ) implies M = block_diagonal (<*M1,M2*>,d) )

proof

A10: dom ((width M2) |-> d) = Seg (width M2) by FINSEQ_2:124;
A11: dom ((width M1) |-> d) = Seg (width M1) by FINSEQ_2:124;
set L2 = (len M2) |-> d;
set L1 = (len M1) |-> d;
assume A12: M = block_diagonal (<*M1,M2*>,d) ; :: thesis: for i being Nat holds
( ( i in Seg (width M1) implies Col (M,i) = (Col (M1,i)) ^ ((len M2) |-> d) ) & ( i in Seg (width M2) implies Col (M,(i + (width M1))) = ((len M1) |-> d) ^ (Col (M2,i)) ) )
let i be Nat; :: thesis: ( ( i in Seg (width M1) implies Col (M,i) = (Col (M1,i)) ^ ((len M2) |-> d) ) & ( i in Seg (width M2) implies Col (M,(i + (width M1))) = ((len M1) |-> d) ^ (Col (M2,i)) ) )
set CM = Col (M,i);
set CM1 = Col (M1,i);
A13: len (Col (M,i)) = len M by CARD_1:def 7;
A14: dom ((len M1) |-> d) = Seg (len M1) by FINSEQ_2:124;
A15: dom ((len M2) |-> d) = Seg (len M2) by FINSEQ_2:124;
A16: len (Col (M1,i)) = len M1 by CARD_1:def 7;
then A17: dom (Col (M1,i)) = dom M1 by FINSEQ_3:29;
A18: len ((len M2) |-> d) = len M2 by CARD_1:def 7;
then A19: dom ((len M2) |-> d) = dom M2 by FINSEQ_3:29;
thus ( i in Seg (width M1) implies Col (M,i) = (Col (M1,i)) ^ ((len M2) |-> d) ) :: thesis: ( i in Seg (width M2) implies Col (M,(i + (width M1))) = ((len M1) |-> d) ^ (Col (M2,i)) )

proof

assume A20: i in Seg (width M1) ; :: thesis: Col (M,i) = (Col (M1,i)) ^ ((len M2) |-> d)
A21: len ((Col (M1,i)) ^ ((len M2) |-> d)) = (len (Col (M1,i))) + (len ((len M2) |-> d)) by FINSEQ_1:22;

now :: thesis: for j being Nat st 1 <= j & j <= len (Col (M,i)) holds
((Col (M1,i)) ^ ((len M2) |-> d)) . j = (Col (M,i)) . j

let j be Nat; :: thesis: ( 1 <= j & j <= len (Col (M,i)) implies ((Col (M1,i)) ^ ((len M2) |-> d)) . j = (Col (M,i)) . j )
assume that
A22: 1 <= j and
A23: j <= len (Col (M,i)) ; :: thesis: ((Col (M1,i)) ^ ((len M2) |-> d)) . j = (Col (M,i)) . j
j in dom M by A13, A22, A23, FINSEQ_3:25;
then A24: (Col (M,i)) . j = (Line (M,j)) . i by A9, A20, MATRIX_0:42;
A25: dom (Line (M1,j)) = Seg (width M1) by FINSEQ_2:124;
A26: j in dom ((Col (M1,i)) ^ ((len M2) |-> d)) by A6, A4, A13, A16, A18, A21, A22, A23, FINSEQ_3:25;

now :: thesis: (Col (M,i)) . j = ((Col (M1,i)) ^ ((len M2) |-> d)) . j

per cases ( j in dom (Col (M1,i)) or ex k being Nat st
( k in dom ((len M2) |-> d) & j = (len (Col (M1,i))) + k ) ) by A26, FINSEQ_1:25;

suppose A27: j in dom (Col (M1,i)) ; :: thesis: (Col (M,i)) . j = ((Col (M1,i)) ^ ((len M2) |-> d)) . j

hence (Col (M,i)) . j = ((Line (M1,j)) ^ ((width M2) |-> d)) . i by A12, A17, A24, Th23
.= (Line (M1,j)) . i by A20, A25, FINSEQ_1:def 7
.= (Col (M1,i)) . j by A17, A20, A27, MATRIX_0:42
.= ((Col (M1,i)) ^ ((len M2) |-> d)) . j by A27, FINSEQ_1:def 7 ;
:: thesis: verum

end;

suppose ex k being Nat st
( k in dom ((len M2) |-> d) & j = (len (Col (M1,i))) + k ) ; :: thesis: (Col (M,i)) . j = ((Col (M1,i)) ^ ((len M2) |-> d)) . j

then consider k being Nat such that
A28: k in dom ((len M2) |-> d) and
A29: j = (len (Col (M1,i))) + k ;
thus (Col (M,i)) . j = (((width M1) |-> d) ^ (Line (M2,k))) . i by A12, A16, A19, A24, A28, A29, Th23
.= ((width M1) |-> d) . i by A11, A20, FINSEQ_1:def 7
.= d by A20, FINSEQ_2:57
.= ((len M2) |-> d) . k by A15, A28, FINSEQ_2:57
.= ((Col (M1,i)) ^ ((len M2) |-> d)) . j by A28, A29, FINSEQ_1:def 7 ; :: thesis: verum

end;

end;

end;

hence ((Col (M1,i)) ^ ((len M2) |-> d)) . j = (Col (M,i)) . j ; :: thesis: verum

end;

hence Col (M,i) = (Col (M1,i)) ^ ((len M2) |-> d) by A6, A13, A16, A18, A21, Th16; :: thesis: verum

end;

set CM2 = Col (M2,i);
set CMi = Col (M,(i + (width M1)));
A30: len (Col (M,(i + (width M1)))) = len M by CARD_1:def 7;
A31: len (Col (M2,i)) = len M2 by CARD_1:def 7;
then A32: dom (Col (M2,i)) = dom M2 by FINSEQ_3:29;
A33: len (((len M1) |-> d) ^ (Col (M2,i))) = (len ((len M1) |-> d)) + (len (Col (M2,i))) by FINSEQ_1:22;
assume A34: i in Seg (width M2) ; :: thesis: Col (M,(i + (width M1))) = ((len M1) |-> d) ^ (Col (M2,i))
A35: len ((len M1) |-> d) = len M1 by CARD_1:def 7;
then A36: dom ((len M1) |-> d) = dom M1 by FINSEQ_3:29;

now :: thesis: for j being Nat st 1 <= j & j <= len (Col (M,(i + (width M1)))) holds
(((len M1) |-> d) ^ (Col (M2,i))) . j = (Col (M,(i + (width M1)))) . j

A37: len ((width M1) |-> d) = width M1 by CARD_1:def 7;
let j be Nat; :: thesis: ( 1 <= j & j <= len (Col (M,(i + (width M1)))) implies (((len M1) |-> d) ^ (Col (M2,i))) . j = (Col (M,(i + (width M1)))) . j )
assume that
A38: 1 <= j and
A39: j <= len (Col (M,(i + (width M1)))) ; :: thesis: (((len M1) |-> d) ^ (Col (M2,i))) . j = (Col (M,(i + (width M1)))) . j
A40: j in dom M by A30, A38, A39, FINSEQ_3:25;
i + (width M1) in Seg (width M) by A7, A8, A34, FINSEQ_1:60;
then A41: (Col (M,(i + (width M1)))) . j = (Line (M,j)) . (i + (width M1)) by A40, MATRIX_0:42;
A42: len (Line (M1,j)) = width M1 by CARD_1:def 7;
A43: j in dom (((len M1) |-> d) ^ (Col (M2,i))) by A6, A4, A30, A31, A35, A33, A38, A39, FINSEQ_3:25;

now :: thesis: (Col (M,(i + (width M1)))) . j = (((len M1) |-> d) ^ (Col (M2,i))) . j

per cases ( j in dom ((len M1) |-> d) or ex k being Nat st
( k in dom (Col (M2,i)) & j = (len ((len M1) |-> d)) + k ) ) by A43, FINSEQ_1:25;

suppose A44: j in dom ((len M1) |-> d) ; :: thesis: (Col (M,(i + (width M1)))) . j = (((len M1) |-> d) ^ (Col (M2,i))) . j

hence (Col (M,(i + (width M1)))) . j = ((Line (M1,j)) ^ ((width M2) |-> d)) . (i + (width M1)) by A12, A36, A41, Th23
.= ((width M2) |-> d) . i by A10, A34, A42, FINSEQ_1:def 7
.= d by A34, FINSEQ_2:57
.= ((len M1) |-> d) . j by A14, A44, FINSEQ_2:57
.= (((len M1) |-> d) ^ (Col (M2,i))) . j by A44, FINSEQ_1:def 7 ;
:: thesis: verum

end;

suppose ex k being Nat st
( k in dom (Col (M2,i)) & j = (len ((len M1) |-> d)) + k ) ; :: thesis: (Col (M,(i + (width M1)))) . j = (((len M1) |-> d) ^ (Col (M2,i))) . j

then consider k being Nat such that
A45: k in dom (Col (M2,i)) and
A46: j = (len ((len M1) |-> d)) + k ;
A47: dom (Line (M2,k)) = Seg (width M2) by FINSEQ_2:124;
thus (Col (M,(i + (width M1)))) . j = (((width M1) |-> d) ^ (Line (M2,k))) . (i + (width M1)) by A12, A35, A32, A41, A45, A46, Th23
.= (Line (M2,k)) . i by A34, A37, A47, FINSEQ_1:def 7
.= (Col (M2,i)) . k by A32, A34, A45, MATRIX_0:42
.= (((len M1) |-> d) ^ (Col (M2,i))) . j by A45, A46, FINSEQ_1:def 7 ; :: thesis: verum

end;

end;

end;

hence (((len M1) |-> d) ^ (Col (M2,i))) . j = (Col (M,(i + (width M1)))) . j ; :: thesis: verum

end;

hence Col (M,(i + (width M1))) = ((len M1) |-> d) ^ (Col (M2,i)) by A6, A30, A31, A35, A33, Th16; :: thesis: verum

end;

assume A48: for i being Nat holds
( ( i in Seg (width M1) implies Col (M,i) = (Col (M1,i)) ^ ((len M2) |-> d) ) & ( i in Seg (width M2) implies Col (M,(i + (width M1))) = ((len M1) |-> d) ^ (Col (M2,i)) ) ) ; :: thesis: M = block_diagonal (<*M1,M2*>,d)
len M1 <= len M by A6, A4, NAT_1:12;
then A49: Seg (len M1) c= Seg (len M) by FINSEQ_1:5;

now :: thesis: for i being Nat holds
( ( i in dom M1 implies Line (M,i) = (Line (M1,i)) ^ ((width M2) |-> d) ) & ( i in dom M2 implies Line (M,(i + (len M1))) = ((width M1) |-> d) ^ (Line (M2,i)) ) )

set W2 = (width M2) |-> d;
set W1 = (width M1) |-> d;
let i be Nat; :: thesis: ( ( i in dom M1 implies Line (M,i) = (Line (M1,i)) ^ ((width M2) |-> d) ) & ( i in dom M2 implies Line (M,(i + (len M1))) = ((width M1) |-> d) ^ (Line (M2,i)) ) )
set LM = Line (M,i);
set LMi = Line (M,(i + (len M1)));
set LM1 = Line (M1,i);
set LM2 = Line (M2,i);
A50: len (Line (M,(i + (len M1)))) = width M by CARD_1:def 7;
A51: len ((width M2) |-> d) = width M2 by CARD_1:def 7;
then A52: dom ((width M2) |-> d) = Seg (width M2) by FINSEQ_1:def 3;
A53: len (Line (M,i)) = width M by CARD_1:def 7;
then A54: dom (Line (M,i)) = Seg (width M) by FINSEQ_1:def 3;
A55: len (Line (M1,i)) = width M1 by CARD_1:def 7;
then A56: dom (Line (M1,i)) = Seg (width M1) by FINSEQ_1:def 3;
thus ( i in dom M1 implies Line (M,i) = (Line (M1,i)) ^ ((width M2) |-> d) ) :: thesis: ( i in dom M2 implies Line (M,(i + (len M1))) = ((width M1) |-> d) ^ (Line (M2,i)) )

proof

assume A57: i in dom M1 ; :: thesis: Line (M,i) = (Line (M1,i)) ^ ((width M2) |-> d)
A58: len ((Line (M1,i)) ^ ((width M2) |-> d)) = (len (Line (M1,i))) + (len ((width M2) |-> d)) by FINSEQ_1:22;

now :: thesis: for j being Nat st 1 <= j & j <= len (Line (M,i)) holds
(Line (M,i)) . j = ((Line (M1,i)) ^ ((width M2) |-> d)) . j

A59: dom ((len M1) |-> d) = Seg (len M1) by FINSEQ_2:124;
let j be Nat; :: thesis: ( 1 <= j & j <= len (Line (M,i)) implies (Line (M,i)) . j = ((Line (M1,i)) ^ ((width M2) |-> d)) . j )
assume that
A60: 1 <= j and
A61: j <= len (Line (M,i)) ; :: thesis: (Line (M,i)) . j = ((Line (M1,i)) ^ ((width M2) |-> d)) . j
j in Seg (width M) by A54, A60, A61, FINSEQ_3:25;
then A62: (Line (M,i)) . j = (Col (M,j)) . i by A49, A1, A2, A57, MATRIX_0:42;
A63: dom (Col (M1,j)) = Seg (len M1) by FINSEQ_2:124;
A64: j in dom ((Line (M1,i)) ^ ((width M2) |-> d)) by A7, A8, A53, A55, A51, A58, A60, A61, FINSEQ_3:25;

now :: thesis: (Line (M,i)) . j = ((Line (M1,i)) ^ ((width M2) |-> d)) . j

per cases ( j in dom (Line (M1,i)) or ex n being Nat st
( n in dom ((width M2) |-> d) & j = (len (Line (M1,i))) + n ) ) by A64, FINSEQ_1:25;

suppose A65: j in dom (Line (M1,i)) ; :: thesis: (Line (M,i)) . j = ((Line (M1,i)) ^ ((width M2) |-> d)) . j

hence (Line (M,i)) . j = ((Col (M1,j)) ^ ((len M2) |-> d)) . i by A48, A56, A62
.= (Col (M1,j)) . i by A2, A57, A63, FINSEQ_1:def 7
.= (Line (M1,i)) . j by A56, A57, A65, MATRIX_0:42
.= ((Line (M1,i)) ^ ((width M2) |-> d)) . j by A65, FINSEQ_1:def 7 ;
:: thesis: verum

end;

suppose ex n being Nat st
( n in dom ((width M2) |-> d) & j = (len (Line (M1,i))) + n ) ; :: thesis: (Line (M,i)) . j = ((Line (M1,i)) ^ ((width M2) |-> d)) . j

then consider n being Nat such that
A66: n in dom ((width M2) |-> d) and
A67: j = (len (Line (M1,i))) + n ;
thus (Line (M,i)) . j = (((len M1) |-> d) ^ (Col (M2,n))) . i by A48, A55, A52, A62, A66, A67
.= ((len M1) |-> d) . i by A2, A57, A59, FINSEQ_1:def 7
.= d by A2, A57, FINSEQ_2:57
.= ((width M2) |-> d) . n by A52, A66, FINSEQ_2:57
.= ((Line (M1,i)) ^ ((width M2) |-> d)) . j by A66, A67, FINSEQ_1:def 7 ; :: thesis: verum

end;

end;

end;

hence (Line (M,i)) . j = ((Line (M1,i)) ^ ((width M2) |-> d)) . j ; :: thesis: verum

end;

hence Line (M,i) = (Line (M1,i)) ^ ((width M2) |-> d) by A7, A53, A55, A51, A58, Th20; :: thesis: verum

end;

A68: len (Line (M2,i)) = width M2 by CARD_1:def 7;
then A69: dom (Line (M2,i)) = Seg (width M2) by FINSEQ_1:def 3;
A70: len ((width M1) |-> d) = width M1 by CARD_1:def 7;
then A71: dom ((width M1) |-> d) = Seg (width M1) by FINSEQ_1:def 3;
thus ( i in dom M2 implies Line (M,(i + (len M1))) = ((width M1) |-> d) ^ (Line (M2,i)) ) :: thesis: verum

proof

assume A72: i in dom M2 ; :: thesis: Line (M,(i + (len M1))) = ((width M1) |-> d) ^ (Line (M2,i))
A73: len (((width M1) |-> d) ^ (Line (M2,i))) = (len ((width M1) |-> d)) + (len (Line (M2,i))) by FINSEQ_1:22;

now :: thesis: for j being Nat st 1 <= j & j <= len (Line (M,(i + (len M1)))) holds
(Line (M,(i + (len M1)))) . j = (((width M1) |-> d) ^ (Line (M2,i))) . j

A74: len ((len M1) |-> d) = len M1 by CARD_1:def 7;
A75: dom ((len M2) |-> d) = Seg (len M2) by FINSEQ_2:124;
A76: dom M2 = Seg (len M2) by FINSEQ_1:def 3;
let j be Nat; :: thesis: ( 1 <= j & j <= len (Line (M,(i + (len M1)))) implies (Line (M,(i + (len M1)))) . j = (((width M1) |-> d) ^ (Line (M2,i))) . j )
assume that
A77: 1 <= j and
A78: j <= len (Line (M,(i + (len M1)))) ; :: thesis: (Line (M,(i + (len M1)))) . j = (((width M1) |-> d) ^ (Line (M2,i))) . j
j in Seg (width M) by A50, A77, A78;
then A79: (Line (M,(i + (len M1)))) . j = (Col (M,j)) . (i + (len M1)) by A6, A4, A1, A72, A76, FINSEQ_1:60, MATRIX_0:42;
A80: len (Col (M1,j)) = len M1 by CARD_1:def 7;
A81: j in dom (((width M1) |-> d) ^ (Line (M2,i))) by A7, A8, A50, A68, A70, A73, A77, A78, FINSEQ_3:25;

now :: thesis: (Line (M,(i + (len M1)))) . j = (((width M1) |-> d) ^ (Line (M2,i))) . j

per cases ( j in dom ((width M1) |-> d) or ex n being Nat st
( n in dom (Line (M2,i)) & j = (len ((width M1) |-> d)) + n ) ) by A81, FINSEQ_1:25;

suppose A82: j in dom ((width M1) |-> d) ; :: thesis: (Line (M,(i + (len M1)))) . j = (((width M1) |-> d) ^ (Line (M2,i))) . j

hence (Line (M,(i + (len M1)))) . j = ((Col (M1,j)) ^ ((len M2) |-> d)) . (i + (len M1)) by A48, A71, A79
.= ((len M2) |-> d) . i by A3, A72, A80, A75, FINSEQ_1:def 7
.= d by A3, A72, FINSEQ_2:57
.= ((width M1) |-> d) . j by A71, A82, FINSEQ_2:57
.= (((width M1) |-> d) ^ (Line (M2,i))) . j by A82, FINSEQ_1:def 7 ;
:: thesis: verum

end;

suppose ex n being Nat st
( n in dom (Line (M2,i)) & j = (len ((width M1) |-> d)) + n ) ; :: thesis: (Line (M,(i + (len M1)))) . j = (((width M1) |-> d) ^ (Line (M2,i))) . j

then consider n being Nat such that
A83: n in dom (Line (M2,i)) and
A84: j = (len ((width M1) |-> d)) + n ;
A85: dom (Col (M2,n)) = Seg (len M2) by FINSEQ_2:124;
thus (Line (M,(i + (len M1)))) . j = (((len M1) |-> d) ^ (Col (M2,n))) . (i + (len M1)) by A48, A70, A69, A79, A83, A84
.= (Col (M2,n)) . i by A3, A72, A74, A85, FINSEQ_1:def 7
.= (Line (M2,i)) . n by A69, A72, A83, MATRIX_0:42
.= (((width M1) |-> d) ^ (Line (M2,i))) . j by A83, A84, FINSEQ_1:def 7 ; :: thesis: verum

end;

end;

end;

hence (Line (M,(i + (len M1)))) . j = (((width M1) |-> d) ^ (Line (M2,i))) . j ; :: thesis: verum

end;

hence Line (M,(i + (len M1))) = ((width M1) |-> d) ^ (Line (M2,i)) by A7, A50, A68, A70, A73, Th20; :: thesis: verum

end;

end;

hence M = block_diagonal (<*M1,M2*>,d) by Th23; :: thesis: verum