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 (block_diagonal (F1 ^ F2),d) = Sum (Len (F1 ^ F2)) & width (block_diagonal (F1 ^ F2),d) = Sum (Width (F1 ^ F2)) ) by Def5;
( Len (F1 ^ F2) = (Len F1) ^ (Len F2) & Width (F1 ^ F2) = (Width F1) ^ (Width F2) ) by Th14, Th18;
then A2: ( len (block_diagonal (F1 ^ F2),d) = (Sum (Len F1)) + (Sum (Len F2)) & width (block_diagonal (F1 ^ F2),d) = (Sum (Width F1)) + (Sum (Width F2)) ) by A1, RVSUM_1:105;
A3: ( len (block_diagonal (F1 ^ <*(block_diagonal F2,d)*>),d) = Sum (Len (F1 ^ <*(block_diagonal F2,d)*>)) & len (block_diagonal F2,d) = Sum (Len F2) & width (block_diagonal (F1 ^ <*(block_diagonal F2,d)*>),d) = Sum (Width (F1 ^ <*(block_diagonal F2,d)*>)) & width (block_diagonal F2,d) = Sum (Width F2) ) by Def5;
( Len (F1 ^ <*(block_diagonal F2,d)*>) = (Len F1) ^ (Len <*(block_diagonal F2,d)*>) & Width (F1 ^ <*(block_diagonal F2,d)*>) = (Width F1) ^ (Width <*(block_diagonal F2,d)*>) ) by Th14, Th18;
then A4: ( len (block_diagonal (F1 ^ <*(block_diagonal F2,d)*>),d) = (Sum (Len <*(block_diagonal F2,d)*>)) + (Sum (Len F1)) & width (block_diagonal (F1 ^ <*(block_diagonal F2,d)*>),d) = (Sum (Width <*(block_diagonal F2,d)*>)) + (Sum (Width F1)) & Sum (Len <*(block_diagonal F2,d)*>) = len (block_diagonal F2,d) & Sum (Width <*(block_diagonal F2,d)*>) = width (block_diagonal F2,d) ) by A3, Lm4, Lm5, RVSUM_1:105;
A5: ( Sum (Len F1) = len (block_diagonal F1,d) & Sum (Width F1) = width (block_diagonal F1,d) ) by Def5;
A6: 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, A3, A4, FINSEQ_1:def 3 ;
A7: block_diagonal <*(block_diagonal F2,d)*>,d = block_diagonal F2,d by Th34;

now

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 A8: [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
A9: ( i in dom (block_diagonal (F1 ^ F2),d) & j in Seg (width (block_diagonal (F1 ^ F2),d)) & dom (block_diagonal (F1 ^ F2),d) = Seg (len (block_diagonal (F1 ^ F2),d)) ) by A8, FINSEQ_1:def 3, ZFMISC_1:106;
then A10: ( 1 <= i & 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 ( 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 ( i in dom (block_diagonal F1,d) & j in Seg (width (block_diagonal F1,d)) ) by A5, A9, A10, FINSEQ_3:27;
then A11: [i,j] in Indices (block_diagonal F1,d) by 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 Th26, A11 ;
:: thesis: verum

end;

suppose A12: ( ( 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 Th29, A8
.= (block_diagonal (F1 ^ <*(block_diagonal F2,d)*>),d) * i,j by A12, Th29, A6, A8 ;
:: thesis: verum

end;

suppose A13: ( 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;
A14: ( i = ii + (Sum (Len F1)) & j = jj + (Sum (Width F1)) ) ;
( ii <> 0 & jj <> 0 ) by A13;
then ( ii > 0 & jj > 0 ) ;
then A15: [ii,jj] in Indices (block_diagonal F2,d) by A8, Th27, A14;
hence (block_diagonal (F1 ^ F2),d) * i,j = (block_diagonal F2,d) * ii,jj by A14, Th28
.= (block_diagonal (F1 ^ <*(block_diagonal F2,d)*>),d) * i,j by A14, A15, A7, 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 A2, A3, A4, MATRIX_1:21; :: thesis: verum