let D be non empty set ; :: thesis: for d being Element of D
for F1, F2 being FinSequence_of_Matrix of D holds block_diagonal (F1 ^ F2),d = block_diagonal (F1 ^ <*(block_diagonal F2,d)*>),d
let d be Element of D; :: thesis: for F1, F2 being FinSequence_of_Matrix of D holds block_diagonal (F1 ^ F2),d = block_diagonal (F1 ^ <*(block_diagonal F2,d)*>),d
let F1, F2 be FinSequence_of_Matrix of D; :: thesis: block_diagonal (F1 ^ F2),d = block_diagonal (F1 ^ <*(block_diagonal F2,d)*>),d
set F12 = F1 ^ F2;
set D1 = block_diagonal F1,d;
set D2 = block_diagonal F2,d;
set D12 = block_diagonal (F1 ^ F2),d;
set FD = F1 ^ <*(block_diagonal F2,d)*>;
set FD2 = block_diagonal (F1 ^ <*(block_diagonal F2,d)*>),d;
set LF1 = Len F1;
set WF1 = Width F1;
set LF2 = Len F2;
set WF2 = Width F2;
set LF = Len (F1 ^ F2);
set WF = Width (F1 ^ F2);
A1: Len (F1 ^ F2) = (Len F1) ^ (Len F2) by Th14;
len (block_diagonal (F1 ^ F2),d) = Sum (Len (F1 ^ F2)) by Def5;
then A2: len (block_diagonal (F1 ^ F2),d) = (Sum (Len F1)) + (Sum (Len F2)) by A1, RVSUM_1:105;
A3: Sum (Width <*(block_diagonal F2,d)*>) = width (block_diagonal F2,d) by Lm5;
A4: Len (F1 ^ <*(block_diagonal F2,d)*>) = (Len F1) ^ (Len <*(block_diagonal F2,d)*>) by Th14;
len (block_diagonal (F1 ^ <*(block_diagonal F2,d)*>),d) = Sum (Len (F1 ^ <*(block_diagonal F2,d)*>)) by Def5;
then A5: len (block_diagonal (F1 ^ <*(block_diagonal F2,d)*>),d) = (Sum (Len <*(block_diagonal F2,d)*>)) + (Sum (Len F1)) by A4, RVSUM_1:105;
A6: Sum (Len F1) = len (block_diagonal F1,d) by Def5;
A7: Width (F1 ^ F2) = (Width F1) ^ (Width F2) by Th18;
A8: Width (F1 ^ <*(block_diagonal F2,d)*>) = (Width F1) ^ (Width <*(block_diagonal F2,d)*>) by Th18;
width (block_diagonal (F1 ^ <*(block_diagonal F2,d)*>),d) = Sum (Width (F1 ^ <*(block_diagonal F2,d)*>)) by Def5;
then A9: width (block_diagonal (F1 ^ <*(block_diagonal F2,d)*>),d) = (Sum (Width <*(block_diagonal F2,d)*>)) + (Sum (Width F1)) by A8, RVSUM_1:105;
A10: Sum (Width F1) = width (block_diagonal F1,d) by Def5;
A11: len (block_diagonal F2,d) = Sum (Len F2) by Def5;
A12: width (block_diagonal (F1 ^ F2),d) = Sum (Width (F1 ^ F2)) by Def5;
then A13: width (block_diagonal (F1 ^ F2),d) = (Sum (Width F1)) + (Sum (Width F2)) by A7, RVSUM_1:105;
A14: Sum (Len <*(block_diagonal F2,d)*>) = len (block_diagonal F2,d) by Lm4;
A15: block_diagonal <*(block_diagonal F2,d)*>,d = block_diagonal F2,d by Th34;
A16: width (block_diagonal F2,d) = Sum (Width F2) by Def5;
A17: Indices (block_diagonal (F1 ^ F2),d) = [:(Seg (len (block_diagonal (F1 ^ F2),d))),(Seg (width (block_diagonal (F1 ^ F2),d))):] by FINSEQ_1:def 3
.= Indices (block_diagonal (F1 ^ <*(block_diagonal F2,d)*>),d) by A2, A13, A11, A16, A5, A9, A14, A3, FINSEQ_1:def 3 ;

now

A18: dom (block_diagonal (F1 ^ F2),d) = Seg (len (block_diagonal (F1 ^ F2),d)) by FINSEQ_1:def 3;
let i, j be Nat; :: thesis: ( [i,j] in Indices (block_diagonal (F1 ^ F2),d) implies (block_diagonal (F1 ^ F2),d) * i,j = (block_diagonal (F1 ^ <*(block_diagonal F2,d)*>),d) * i,j )
assume A19: [i,j] in Indices (block_diagonal (F1 ^ F2),d) ; :: thesis: (block_diagonal (F1 ^ F2),d) * i,j = (block_diagonal (F1 ^ <*(block_diagonal F2,d)*>),d) * i,j
i in dom (block_diagonal (F1 ^ F2),d) by A19, ZFMISC_1:106;
then A20: 1 <= i by A18, FINSEQ_1:3;
A21: j in Seg (width (block_diagonal (F1 ^ F2),d)) by A19, ZFMISC_1:106;
then A22: 1 <= j by FINSEQ_1:3;

now

per cases ( ( i <= Sum (Len F1) & j <= Sum (Width F1) ) or ( i > Sum (Len F1) & j <= Sum (Width F1) ) or ( i <= Sum (Len F1) & j > Sum (Width F1) ) or ( i > Sum (Len F1) & j > Sum (Width F1) ) ) ;

suppose A23: ( i <= Sum (Len F1) & j <= Sum (Width F1) ) ; :: thesis: (block_diagonal (F1 ^ F2),d) * i,j = (block_diagonal (F1 ^ <*(block_diagonal F2,d)*>),d) * i,j

then A24: i in dom (block_diagonal F1,d) by A6, A20, FINSEQ_3:27;
j in Seg (width (block_diagonal F1,d)) by A10, A21, A22, A23;
then A25: [i,j] in Indices (block_diagonal F1,d) by A24, ZFMISC_1:106;
hence (block_diagonal (F1 ^ F2),d) * i,j = (block_diagonal F1,d) * i,j by Th26
.= (block_diagonal (F1 ^ <*(block_diagonal F2,d)*>),d) * i,j by A25, Th26 ;
:: thesis: verum

end;

suppose A26: ( ( i > Sum (Len F1) & j <= Sum (Width F1) ) or ( i <= Sum (Len F1) & j > Sum (Width F1) ) ) ; :: thesis: (block_diagonal (F1 ^ F2),d) * i,j = (block_diagonal (F1 ^ <*(block_diagonal F2,d)*>),d) * i,j

hence (block_diagonal (F1 ^ F2),d) * i,j = d by A19, Th29
.= (block_diagonal (F1 ^ <*(block_diagonal F2,d)*>),d) * i,j by A17, A19, A26, Th29 ;
:: thesis: verum

end;

suppose A27: ( i > Sum (Len F1) & j > Sum (Width F1) ) ; :: thesis: (block_diagonal (F1 ^ F2),d) * i,j = (block_diagonal (F1 ^ <*(block_diagonal F2,d)*>),d) * i,j

then reconsider ii = i - (Sum (Len F1)), jj = j - (Sum (Width F1)) as Element of NAT by NAT_1:21;
A28: jj <> 0 by A27;
A29: i = ii + (Sum (Len F1)) ;
A30: j = jj + (Sum (Width F1)) ;
ii <> 0 by A27;
then A31: [ii,jj] in Indices (block_diagonal F2,d) by A19, A29, A30, A28, Th27;
hence (block_diagonal (F1 ^ F2),d) * i,j = (block_diagonal F2,d) * ii,jj by A29, A30, Th28
.= (block_diagonal (F1 ^ <*(block_diagonal F2,d)*>),d) * i,j by A15, A29, A30, A31, Th28 ;
:: thesis: verum

end;

end;

end;

hence (block_diagonal (F1 ^ F2),d) * i,j = (block_diagonal (F1 ^ <*(block_diagonal F2,d)*>),d) * i,j ; :: thesis: verum

end;

hence block_diagonal (F1 ^ F2),d = block_diagonal (F1 ^ <*(block_diagonal F2,d)*>),d by A12, A7, A2, A11, A16, A5, A9, A14, A3, MATRIX_1:21, RVSUM_1:105; :: thesis: verum