let i, j be Nat; :: thesis: for D being non empty set
for d being Element of D
for F1, F2 being FinSequence_of_Matrix of D st [i,j] in Indices (block_diagonal F1,d) holds
(block_diagonal F1,d) * i,j = (block_diagonal (F1 ^ F2),d) * i,j
let D be non empty set ; :: thesis: for d being Element of D
for F1, F2 being FinSequence_of_Matrix of D st [i,j] in Indices (block_diagonal F1,d) holds
(block_diagonal F1,d) * i,j = (block_diagonal (F1 ^ F2),d) * i,j
let d be Element of D; :: thesis: for F1, F2 being FinSequence_of_Matrix of D st [i,j] in Indices (block_diagonal F1,d) holds
(block_diagonal F1,d) * i,j = (block_diagonal (F1 ^ F2),d) * i,j
let F1, F2 be FinSequence_of_Matrix of D; :: thesis: ( [i,j] in Indices (block_diagonal F1,d) implies (block_diagonal F1,d) * i,j = (block_diagonal (F1 ^ F2),d) * i,j )
assume A1: [i,j] in Indices (block_diagonal F1,d) ; :: thesis: (block_diagonal F1,d) * i,j = (block_diagonal (F1 ^ F2),d) * i,j
set B1 = block_diagonal F1,d;
set L1 = Len F1;
set W1 = Width F1;
set L2 = Len F2;
set W2 = Width F2;
set F12 = F1 ^ F2;
set L = Len (F1 ^ F2);
set W = Width (F1 ^ F2);
set B12 = block_diagonal (F1 ^ F2),d;
A2: Indices (block_diagonal F1,d) is Subset of (Indices (block_diagonal (F1 ^ F2),d)) by Th25;
i in dom (block_diagonal F1,d) by A1, ZFMISC_1:106;
then ( i in Seg (len (block_diagonal F1,d)) & len (block_diagonal F1,d) = Sum (Len F1) & (Len F1) ^ (Len F2) = Len (F1 ^ F2) ) by Def5, Th14, FINSEQ_1:def 3;
then A3: ( min (Len F1),i = min (Len (F1 ^ F2)),i & min (Len F1),i in dom (Len F1) ) by Th8, Def1;
then A4: ( min (Len F1),i <= len (Len F1) & (min (Len F1),i) -' 1 <= min (Len F1),i ) by FINSEQ_3:27, NAT_D:35;
then ( (min (Len F1),i) -' 1 <= len (Len F1) & len (Len F1) = len F1 & len F1 = len (Width F1) ) by FINSEQ_1:def 18, XXREAL_0:2;
then A5: ( ((Width F1) ^ (Width F2)) | (min (Len (F1 ^ F2)),i) = (Width F1) | (min (Len F1),i) & ((Width F1) ^ (Width F2)) | ((min (Len (F1 ^ F2)),i) -' 1) = (Width F1) | ((min (Len F1),i) -' 1) & ((Len F1) ^ (Len F2)) | ((min (Len (F1 ^ F2)),i) -' 1) = (Len F1) | ((min (Len F1),i) -' 1) ) by A3, A4, FINSEQ_5:25;
A6: ( (Width F1) ^ (Width F2) = Width (F1 ^ F2) & (Len F1) ^ (Len F2) = Len (F1 ^ F2) ) by Th14, Th18;
A7: dom (Len F1) = dom F1 by Def3;

per cases ( j <= Sum ((Width F1) | ((min (Len F1),i) -' 1)) or j > Sum ((Width F1) | (min (Len F1),i)) or ( j > Sum ((Width F1) | ((min (Len F1),i) -' 1)) & j <= Sum ((Width F1) | (min (Len F1),i)) ) ) ;

suppose ( j <= Sum ((Width F1) | ((min (Len F1),i) -' 1)) or j > Sum ((Width F1) | (min (Len F1),i)) ) ; :: thesis: (block_diagonal F1,d) * i,j = (block_diagonal (F1 ^ F2),d) * i,j

then ( (block_diagonal F1,d) * i,j = d & d = (block_diagonal (F1 ^ F2),d) * i,j ) by A1, A2, A5, Def5, A6;
hence (block_diagonal F1,d) * i,j = (block_diagonal (F1 ^ F2),d) * i,j ; :: thesis: verum

end;

suppose ( j > Sum ((Width F1) | ((min (Len F1),i) -' 1)) & j <= Sum ((Width F1) | (min (Len F1),i)) ) ; :: thesis: (block_diagonal F1,d) * i,j = (block_diagonal (F1 ^ F2),d) * i,j

then ( (block_diagonal F1,d) * i,j = (F1 . (min (Len F1),i)) * (i -' (Sum ((Len F1) | ((min (Len F1),i) -' 1)))),(j -' (Sum ((Width F1) | ((min (Len F1),i) -' 1)))) & (block_diagonal (F1 ^ F2),d) * i,j = ((F1 ^ F2) . (min (Len F1),i)) * (i -' (Sum ((Len F1) | ((min (Len F1),i) -' 1)))),(j -' (Sum ((Width F1) | ((min (Len F1),i) -' 1)))) ) by A1, A2, A3, A5, Def5, A6;
hence (block_diagonal F1,d) * i,j = (block_diagonal (F1 ^ F2),d) * i,j by A7, A3, FINSEQ_1:def 7; :: thesis: verum

end;

end;