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:75;
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:75;
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:75;
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:75;
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 :: thesis: for i, j being Nat st [i,j] in Indices (block_diagonal ((F1 ^ F2),d)) holds
(block_diagonal ((F1 ^ F2),d)) * (i,j) = (block_diagonal ((F1 ^ <*(block_diagonal (F2,d))*>),d)) * (i,j)

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:87;
then A20: 1 <= i by A18, FINSEQ_1:1;
j in Seg (width (block_diagonal ((F1 ^ F2),d))) by A19, ZFMISC_1:87;
then A21: 1 <= j by FINSEQ_1:1;

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

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 A22: ( 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 A23: i in dom (block_diagonal (F1,d)) by A6, A20, FINSEQ_3:25;
j in Seg (width (block_diagonal (F1,d))) by A10, A21, A22;
then A24: [i,j] in Indices (block_diagonal (F1,d)) by A23, ZFMISC_1:87;
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 A24, Th26 ;
:: thesis: verum

end;

suppose A25: ( ( 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, A25, Th29 ;
:: thesis: verum

end;

suppose A26: ( 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;
A27: jj <> 0 by A26;
A28: i = ii + (Sum (Len F1)) ;
A29: j = jj + (Sum (Width F1)) ;
ii <> 0 by A26;
then A30: [ii,jj] in Indices (block_diagonal (F2,d)) by A19, A28, A29, A27, Th27;
hence (block_diagonal ((F1 ^ F2),d)) * (i,j) = (block_diagonal (F2,d)) * (ii,jj) by A28, A29, Th28
.= (block_diagonal ((F1 ^ <*(block_diagonal (F2,d))*>),d)) * (i,j) by A15, A28, A29, A30, 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_0:21, RVSUM_1:75; :: thesis: verum