let D be non empty set ; 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 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)) ) ) )
let d be 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 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)) ) ) )
let M1, M2 be 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 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)) ) ) )
let M be Matrix of Sum (Len <*M1,M2*>), Sum (Width <*M1,M2*>),D; ( M = block_diagonal (<*M1,M2*>,d) iff 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 F1 = <*M1*>;
set F2 = <*M2*>;
set F12 = <*M1,M2*>;
set B = block_diagonal (<*M1,M2*>,d);
set L1 = len M1;
set L2 = len M2;
reconsider W1 = width M1 as Element of NAT by ORDINAL1:def 12;
set W2 = width M2;
A1:
Sum <*W1*> = W1
by RVSUM_1:73;
len (block_diagonal (<*M1,M2*>,d)) = Sum (Len <*M1,M2*>)
by Def5;
then A2:
len (block_diagonal (<*M1,M2*>,d)) = (len M1) + (len M2)
by Th16;
A3:
len <*M1,M2*> = len (Len <*M1,M2*>)
by CARD_1:def 7;
A4:
(Len <*M1,M2*>) | 0 = <*> REAL
;
A5:
(Width <*M1,M2*>) | 0 = <*> REAL
;
A6:
1 -' 1 = 0
by XREAL_1:232;
A7:
width (block_diagonal (<*M1,M2*>,d)) = Sum (Width <*M1,M2*>)
by Def5;
then A8:
width (block_diagonal (<*M1,M2*>,d)) = W1 + (width M2)
by Th20;
A9:
len <*W1*> = 1
by FINSEQ_1:40;
A10:
len <*M1*> = 1
by FINSEQ_1:40;
A11:
Len <*M1*> = <*(len M1)*>
by Th15;
A12:
Len <*M1,M2*> = (Len <*M1*>) ^ (Len <*M2*>)
by Th14;
then A13:
(Len <*M1,M2*>) . 1 = len M1
by A11, FINSEQ_1:41;
A14:
len <*(len M1)*> = 1
by FINSEQ_1:40;
then A15:
(Len <*M1,M2*>) | 1 = <*(len M1)*>
by A12, A11, FINSEQ_5:23;
A16:
Width <*M1*> = <*W1*>
by Th19;
A17:
Sum <*(len M1)*> = len M1
by RVSUM_1:73;
Width <*M1,M2*> = (Width <*M1*>) ^ (Width <*M2*>)
by Th18;
then A18:
(Width <*M1,M2*>) | 1 = <*W1*>
by A16, A9, FINSEQ_5:23;
A19:
Len <*M2*> = <*(len M2)*>
by Th15;
then A20:
len (Len <*M1,M2*>) = 1 + 1
by A12, A11, A14, FINSEQ_2:16;
A21:
(Len <*M1,M2*>) . 2 = len M2
by A12, A11, A19, A14, FINSEQ_1:42;
len (Width <*M1,M2*>) = len <*M1,M2*>
by CARD_1:def 7;
then A22:
(Width <*M1,M2*>) | 2 = Width <*M1,M2*>
by A20, A3, FINSEQ_1:58;
A23:
dom (Len <*M1,M2*>) = {1,2}
by A20, FINSEQ_1:2, FINSEQ_1:def 3;
then A24:
1 in dom (Len <*M1,M2*>)
by TARSKI:def 2;
then A25:
(Len <*M1,M2*>) /. 1 = (Len <*M1,M2*>) . 1
by PARTFUN1:def 6;
A26:
2 -' 1 = 2 - 1
by XREAL_1:233;
( Sum (Len <*M1,M2*>) = 0 implies Sum (Width <*M1,M2*>) = 0 )
by Th13;
then A27:
width M = W1 + (width M2)
by A7, A8, MATRIX13:1;
A28:
2 in dom (Len <*M1,M2*>)
by A23, TARSKI:def 2;
then A29:
(Len <*M1,M2*>) /. 2 = (Len <*M1,M2*>) . 2
by PARTFUN1:def 6;
hereby ( ( 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)) ) ) ) implies M = block_diagonal (<*M1,M2*>,d) )
assume A30:
M = block_diagonal (
<*M1,M2*>,
d)
;
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)) ) )let i be
Nat;
( ( 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)) ) )thus
(
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)) )proof
set W2d =
(width M2) |-> d;
set LM1 =
Line (
M1,
i);
set LM =
Line (
M,
i);
A31:
len M1 <= (len M1) + (len M2)
by NAT_1:11;
A32:
len (Line (M1,i)) = W1
by CARD_1:def 7;
assume A33:
i in dom M1
;
Line (M,i) = (Line (M1,i)) ^ ((width M2) |-> d)
then A34:
1
<= i
by FINSEQ_3:25;
i <= len M1
by A33, FINSEQ_3:25;
then
i <= (len M1) + (len M2)
by A31, XXREAL_0:2;
then A35:
i in dom (block_diagonal (<*M1,M2*>,d))
by A2, A34, FINSEQ_3:25;
A36:
len ((width M2) |-> d) = width M2
by CARD_1:def 7;
A37:
len ((Line (M1,i)) ^ ((width M2) |-> d)) = (len (Line (M1,i))) + (len ((width M2) |-> d))
by FINSEQ_1:22;
A38:
len (Line (M,i)) = W1 + (width M2)
by A27, CARD_1:def 7;
A39:
i in Seg (len M1)
by A33, FINSEQ_1:def 3;
now for j being Nat st 1 <= j & j <= len (Line (M,i)) holds
(Line (M,i)) . j = ((Line (M1,i)) ^ ((width M2) |-> d)) . jA40:
min (
(Len <*M1,M2*>),
(i + 0))
= 1
by A24, A6, A13, A25, A4, A39, Th10, RVSUM_1:72;
let j be
Nat;
( 1 <= j & j <= len (Line (M,i)) implies (Line (M,i)) . j = ((Line (M1,i)) ^ ((width M2) |-> d)) . j )assume that A41:
1
<= j
and A42:
j <= len (Line (M,i))
;
(Line (M,i)) . j = ((Line (M1,i)) ^ ((width M2) |-> d)) . jA43:
j in Seg (width (block_diagonal (<*M1,M2*>,d)))
by A8, A38, A41, A42;
then A44:
[i,j] in Indices (block_diagonal (<*M1,M2*>,d))
by A35, ZFMISC_1:87;
A45:
j in dom ((Line (M1,i)) ^ ((width M2) |-> d))
by A38, A32, A36, A37, A41, A42, FINSEQ_3:25;
now (Line (M,i)) . j = ((Line (M1,i)) ^ ((width M2) |-> d)) . jper cases
( j <= W1 or j > W1 )
;
suppose A46:
j <= W1
;
(Line (M,i)) . j = ((Line (M1,i)) ^ ((width M2) |-> d)) . jthen A47:
j in Seg (width M1)
by A41;
A48:
j in dom (Line (M1,i))
by A32, A41, A46, FINSEQ_3:25;
thus (Line (M,i)) . j =
M * (
i,
j)
by A8, A27, A43, MATRIX_0:def 7
.=
(<*M1,M2*> . 1) * (
(i -' (Sum ((Len <*M1,M2*>) | 0))),
(j -' (Sum ((Width <*M1,M2*>) | 0))))
by A1, A6, A18, A30, A41, A44, A40, A46, Def5, RVSUM_1:72
.=
(<*M1,M2*> . 1) * (
i,
(j -' 0))
by NAT_D:40, RVSUM_1:72
.=
(<*M1,M2*> . 1) * (
i,
j)
by NAT_D:40
.=
M1 * (
i,
j)
.=
(Line (M1,i)) . j
by A47, MATRIX_0:def 7
.=
((Line (M1,i)) ^ ((width M2) |-> d)) . j
by A48, FINSEQ_1:def 7
;
verum end; suppose A49:
j > W1
;
(Line (M,i)) . j = ((Line (M1,i)) ^ ((width M2) |-> d)) . jA50:
dom ((width M2) |-> d) = Seg (width M2)
by A36, FINSEQ_1:def 3;
not
j in dom (Line (M1,i))
by A32, A49, FINSEQ_3:25;
then consider k being
Nat such that A51:
k in dom ((width M2) |-> d)
and A52:
j = (len (Line (M1,i))) + k
by A45, FINSEQ_1:25;
thus (Line (M,i)) . j =
M * (
i,
j)
by A8, A27, A43, MATRIX_0:def 7
.=
d
by A1, A18, A30, A44, A40, A49, Def5
.=
((width M2) |-> d) . k
by A51, A50, FINSEQ_2:57
.=
((Line (M1,i)) ^ ((width M2) |-> d)) . j
by A51, A52, FINSEQ_1:def 7
;
verum end; hence
(Line (M,i)) . j = ((Line (M1,i)) ^ ((width M2) |-> d)) . j
;
verum end;
hence
Line (
M,
i)
= (Line (M1,i)) ^ ((width M2) |-> d)
by A38, A32, A36, A37;
verum
end; thus
(
i in dom M2 implies
Line (
M,
(i + (len M1)))
= ((width M1) |-> d) ^ (Line (M2,i)) )
verumproof
set LM2 =
Line (
M2,
i);
set W1d =
W1 |-> d;
set LM =
Line (
M,
(i + (len M1)));
A53:
len (Line (M2,i)) = width M2
by CARD_1:def 7;
A54:
len ((W1 |-> d) ^ (Line (M2,i))) = (len (W1 |-> d)) + (len (Line (M2,i)))
by FINSEQ_1:22;
A55:
len (W1 |-> d) = W1
by CARD_1:def 7;
A56:
len (Line (M,(i + (len M1)))) = W1 + (width M2)
by A27, CARD_1:def 7;
assume
i in dom M2
;
Line (M,(i + (len M1))) = ((width M1) |-> d) ^ (Line (M2,i))
then A57:
i in Seg (len M2)
by FINSEQ_1:def 3;
then
(len M1) + i in Seg ((len M1) + (len M2))
by FINSEQ_1:60;
then A58:
(len M1) + i in dom (block_diagonal (<*M1,M2*>,d))
by A2, FINSEQ_1:def 3;
now for j being Nat st 1 <= j & j <= len (Line (M,(i + (len M1)))) holds
(Line (M,(i + (len M1)))) . j = ((W1 |-> d) ^ (Line (M2,i))) . jA59:
min (
(Len <*M1,M2*>),
(i + (len M1)))
= 2
by A17, A28, A26, A21, A29, A15, A57, Th10;
let j be
Nat;
( 1 <= j & j <= len (Line (M,(i + (len M1)))) implies (Line (M,(i + (len M1)))) . b1 = ((W1 |-> d) ^ (Line (M2,i))) . b1 )assume that A60:
1
<= j
and A61:
j <= len (Line (M,(i + (len M1))))
;
(Line (M,(i + (len M1)))) . b1 = ((W1 |-> d) ^ (Line (M2,i))) . b1A62:
j in Seg (width (block_diagonal (<*M1,M2*>,d)))
by A8, A56, A60, A61;
then A63:
[(i + (len M1)),j] in Indices (block_diagonal (<*M1,M2*>,d))
by A58, ZFMISC_1:87;
A64:
j in dom ((W1 |-> d) ^ (Line (M2,i)))
by A56, A53, A55, A54, A60, A61, FINSEQ_3:25;
per cases
( j <= W1 or j > W1 )
;
suppose A65:
j <= W1
;
(Line (M,(i + (len M1)))) . b1 = ((W1 |-> d) ^ (Line (M2,i))) . b1A66:
dom (W1 |-> d) = Seg W1
by A55, FINSEQ_1:def 3;
A67:
j in Seg W1
by A60, A65;
thus (Line (M,(i + (len M1)))) . j =
(block_diagonal (<*M1,M2*>,d)) * (
(i + (len M1)),
j)
by A30, A62, MATRIX_0:def 7
.=
d
by A1, A26, A18, A63, A59, A65, Def5
.=
(W1 |-> d) . j
by A67, FINSEQ_2:57
.=
((W1 |-> d) ^ (Line (M2,i))) . j
by A67, A66, FINSEQ_1:def 7
;
verum end; suppose A68:
j > W1
;
(Line (M,(i + (len M1)))) . b1 = ((W1 |-> d) ^ (Line (M2,i))) . b1A69:
dom (Line (M2,i)) = Seg (width M2)
by A53, FINSEQ_1:def 3;
not
j in dom (W1 |-> d)
by A55, A68, FINSEQ_3:25;
then consider k being
Nat such that A70:
k in dom (Line (M2,i))
and A71:
j = W1 + k
by A55, A64, FINSEQ_1:25;
thus (Line (M,(i + (len M1)))) . j =
(block_diagonal (<*M1,M2*>,d)) * (
(i + (len M1)),
j)
by A30, A62, MATRIX_0:def 7
.=
(<*M1,M2*> . 2) * (
((i + (len M1)) -' (len M1)),
(j -' W1))
by A7, A8, A1, A17, A26, A15, A18, A22, A56, A61, A63, A59, A68, Def5
.=
(<*M1,M2*> . 2) * (
i,
(j -' W1))
by NAT_D:34
.=
(<*M1,M2*> . ((len <*M1*>) + 1)) * (
i,
k)
by A10, A71, NAT_D:34
.=
M2 * (
i,
k)
by FINSEQ_1:42
.=
(Line (M2,i)) . k
by A70, A69, MATRIX_0:def 7
.=
((W1 |-> d) ^ (Line (M2,i))) . j
by A55, A70, A71, FINSEQ_1:def 7
;
verum end; end;
hence
Line (
M,
(i + (len M1)))
= ((width M1) |-> d) ^ (Line (M2,i))
by A56, A53, A55, A54;
verum
end;
end;
assume A72:
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)) ) )
; M = block_diagonal (<*M1,M2*>,d)
A73:
Sum ((Width <*M1,M2*>) | 2) = W1 + (width M2)
by A22, Th20;
now for i, j being Nat st [i,j] in Indices M holds
M * (i,j) = (block_diagonal (<*M1,M2*>,d)) * (i,j)set W1d =
W1 |-> d;
set W2d =
(width M2) |-> d;
A74:
Indices M = Indices (block_diagonal (<*M1,M2*>,d))
by MATRIX_0:26;
let i,
j be
Nat;
( [i,j] in Indices M implies M * (i,j) = (block_diagonal (<*M1,M2*>,d)) * (i,j) )assume A75:
[i,j] in Indices M
;
M * (i,j) = (block_diagonal (<*M1,M2*>,d)) * (i,j)A76:
i in dom (block_diagonal (<*M1,M2*>,d))
by A75, A74, ZFMISC_1:87;
then A77:
1
<= i
by FINSEQ_3:25;
A78:
j in Seg (width (block_diagonal (<*M1,M2*>,d)))
by A75, A74, ZFMISC_1:87;
then A79:
1
<= j
by FINSEQ_1:1;
A80:
i in Seg ((len M1) + (len M2))
by A2, A76, FINSEQ_1:def 3;
set LM1 =
Line (
M1,
i);
A81:
len (Line (M1,i)) = W1
by CARD_1:def 7;
A82:
len (W1 |-> d) = W1
by CARD_1:def 7;
A83:
len ((width M2) |-> d) = width M2
by CARD_1:def 7;
A84:
len ((Line (M1,i)) ^ ((width M2) |-> d)) = (len (Line (M1,i))) + (len ((width M2) |-> d))
by FINSEQ_1:22;
A85:
j <= width (block_diagonal (<*M1,M2*>,d))
by A78, FINSEQ_1:1;
now M * (i,j) = (block_diagonal (<*M1,M2*>,d)) * (i,j)per cases
( i <= len M1 or i > len M1 )
;
suppose A86:
i <= len M1
;
M * (i,j) = (block_diagonal (<*M1,M2*>,d)) * (i,j)then
i in Seg (len M1)
by A77;
then A87:
min (
(Len <*M1,M2*>),
(i + 0))
= 1
by A24, A6, A13, A25, A4, Th10, RVSUM_1:72;
A88:
now (block_diagonal (<*M1,M2*>,d)) * (i,j) = ((Line (M1,i)) ^ ((width M2) |-> d)) . jper cases
( j <= W1 or j > W1 )
;
suppose A89:
j <= W1
;
(block_diagonal (<*M1,M2*>,d)) * (i,j) = ((Line (M1,i)) ^ ((width M2) |-> d)) . jthen A90:
j in Seg (width M1)
by A79;
A91:
j in dom (Line (M1,i))
by A79, A81, A89, FINSEQ_3:25;
thus (block_diagonal (<*M1,M2*>,d)) * (
i,
j) =
(<*M1,M2*> . 1) * (
(i -' 0),
(j -' 0))
by A1, A6, A4, A5, A18, A75, A74, A79, A87, A89, Def5, RVSUM_1:72
.=
(<*M1,M2*> . 1) * (
i,
(j -' 0))
by NAT_D:40
.=
(<*M1,M2*> . 1) * (
i,
j)
by NAT_D:40
.=
M1 * (
i,
j)
.=
(Line (M1,i)) . j
by A90, MATRIX_0:def 7
.=
((Line (M1,i)) ^ ((width M2) |-> d)) . j
by A91, FINSEQ_1:def 7
;
verum end; suppose A92:
j > W1
;
(block_diagonal (<*M1,M2*>,d)) * (i,j) = ((Line (M1,i)) ^ ((width M2) |-> d)) . jthen A93:
not
j in dom (Line (M1,i))
by A81, FINSEQ_3:25;
A94:
dom ((width M2) |-> d) = Seg (width M2)
by A83, FINSEQ_1:def 3;
dom ((Line (M1,i)) ^ ((width M2) |-> d)) = Seg (width (block_diagonal (<*M1,M2*>,d)))
by A8, A81, A83, A84, FINSEQ_1:def 3;
then consider k being
Nat such that A95:
k in dom ((width M2) |-> d)
and A96:
j = (len (Line (M1,i))) + k
by A78, A93, FINSEQ_1:25;
thus (block_diagonal (<*M1,M2*>,d)) * (
i,
j) =
d
by A1, A18, A75, A74, A87, A92, Def5
.=
((width M2) |-> d) . k
by A95, A94, FINSEQ_2:57
.=
((Line (M1,i)) ^ ((width M2) |-> d)) . j
by A95, A96, FINSEQ_1:def 7
;
verum end;
i in dom M1
by A77, A86, FINSEQ_3:25;
then
Line (
M,
i)
= (Line (M1,i)) ^ ((width M2) |-> d)
by A72;
hence
M * (
i,
j)
= (block_diagonal (<*M1,M2*>,d)) * (
i,
j)
by A8, A27, A78, A88, MATRIX_0:def 7;
verum end; suppose A97:
i > len M1
;
M * (i,j) = (block_diagonal (<*M1,M2*>,d)) * (i,j)then reconsider iL =
i - (len M1) as
Element of
NAT by NAT_1:21;
A98:
iL <> 0
by A97;
set LM2 =
Line (
M2,
iL);
i = iL + (len M1)
;
then
iL in Seg (len M2)
by A80, A98, FINSEQ_1:61;
then A99:
min (
(Len <*M1,M2*>),
(iL + (len M1)))
= 2
by A17, A28, A26, A21, A29, A15, Th10;
A100:
now (block_diagonal (<*M1,M2*>,d)) * (i,j) = ((W1 |-> d) ^ (Line (M2,iL))) . jper cases
( j <= W1 or j > W1 )
;
suppose A101:
j <= W1
;
(block_diagonal (<*M1,M2*>,d)) * (i,j) = ((W1 |-> d) ^ (Line (M2,iL))) . jthen A102:
j in Seg W1
by A79;
A103:
j in dom (W1 |-> d)
by A79, A82, A101, FINSEQ_3:25;
thus (block_diagonal (<*M1,M2*>,d)) * (
i,
j) =
d
by A1, A26, A18, A75, A74, A99, A101, Def5
.=
(W1 |-> d) . j
by A102, FINSEQ_2:57
.=
((W1 |-> d) ^ (Line (M2,iL))) . j
by A103, FINSEQ_1:def 7
;
verum end; suppose A104:
j > W1
;
(block_diagonal (<*M1,M2*>,d)) * (i,j) = ((W1 |-> d) ^ (Line (M2,iL))) . j
len (Line (M2,iL)) = width M2
by MATRIX_0:def 7;
then A105:
dom ((width M2) |-> d) = dom (Line (M2,iL))
by A83, FINSEQ_3:29;
A106:
not
j in dom (Line (M1,i))
by A81, A104, FINSEQ_3:25;
A107:
dom ((width M2) |-> d) = Seg (width M2)
by A83, FINSEQ_1:def 3;
dom ((Line (M1,i)) ^ ((width M2) |-> d)) = Seg (width (block_diagonal (<*M1,M2*>,d)))
by A8, A81, A83, A84, FINSEQ_1:def 3;
then consider k being
Nat such that A108:
k in dom ((width M2) |-> d)
and A109:
j = W1 + k
by A78, A81, A106, FINSEQ_1:25;
thus (block_diagonal (<*M1,M2*>,d)) * (
i,
j) =
(<*M1,M2*> . 2) * (
((iL + (len M1)) -' (len M1)),
(j -' W1))
by A8, A1, A17, A26, A15, A18, A73, A75, A74, A85, A99, A104, Def5
.=
(<*M1,M2*> . 2) * (
iL,
(j -' W1))
by NAT_D:34
.=
(<*M1,M2*> . ((len <*M1*>) + 1)) * (
iL,
k)
by A10, A109, NAT_D:34
.=
M2 * (
iL,
k)
by FINSEQ_1:42
.=
(Line (M2,iL)) . k
by A108, A107, MATRIX_0:def 7
.=
((W1 |-> d) ^ (Line (M2,iL))) . j
by A82, A108, A109, A105, FINSEQ_1:def 7
;
verum end;
Seg (len M2) = dom M2
by FINSEQ_1:def 3;
then
Line (
M,
(iL + (len M1)))
= (W1 |-> d) ^ (Line (M2,iL))
by A72, A80, A98, FINSEQ_1:61;
hence
M * (
i,
j)
= (block_diagonal (<*M1,M2*>,d)) * (
i,
j)
by A8, A27, A78, A100, MATRIX_0:def 7;
verum end; hence
M * (
i,
j)
= (block_diagonal (<*M1,M2*>,d)) * (
i,
j)
;
verum end;
hence
M = block_diagonal (<*M1,M2*>,d)
by MATRIX_0:27; verum