let D be non empty set ; :: thesis: for d being Element of D
for F being FinSequence_of_Matrix of D
for i, j, k being Nat st i in dom F & [j,k] in Indices (F . i) holds
( [(j + (Sum ((Len F) | (i -' 1)))),(k + (Sum ((Width F) | (i -' 1))))] in Indices (block_diagonal F,d) & (F . i) * j,k = (block_diagonal F,d) * (j + (Sum ((Len F) | (i -' 1)))),(k + (Sum ((Width F) | (i -' 1)))) )
let d be Element of D; :: thesis: for F being FinSequence_of_Matrix of D
for i, j, k being Nat st i in dom F & [j,k] in Indices (F . i) holds
( [(j + (Sum ((Len F) | (i -' 1)))),(k + (Sum ((Width F) | (i -' 1))))] in Indices (block_diagonal F,d) & (F . i) * j,k = (block_diagonal F,d) * (j + (Sum ((Len F) | (i -' 1)))),(k + (Sum ((Width F) | (i -' 1)))) )
let F be FinSequence_of_Matrix of D; :: thesis: for i, j, k being Nat st i in dom F & [j,k] in Indices (F . i) holds
( [(j + (Sum ((Len F) | (i -' 1)))),(k + (Sum ((Width F) | (i -' 1))))] in Indices (block_diagonal F,d) & (F . i) * j,k = (block_diagonal F,d) * (j + (Sum ((Len F) | (i -' 1)))),(k + (Sum ((Width F) | (i -' 1)))) )
let i, j, k be Nat; :: thesis: ( i in dom F & [j,k] in Indices (F . i) implies ( [(j + (Sum ((Len F) | (i -' 1)))),(k + (Sum ((Width F) | (i -' 1))))] in Indices (block_diagonal F,d) & (F . i) * j,k = (block_diagonal F,d) * (j + (Sum ((Len F) | (i -' 1)))),(k + (Sum ((Width F) | (i -' 1)))) ) )
assume that
A1: i in dom F and
A2: [j,k] in Indices (F . i) ; :: thesis: ( [(j + (Sum ((Len F) | (i -' 1)))),(k + (Sum ((Width F) | (i -' 1))))] in Indices (block_diagonal F,d) & (F . i) * j,k = (block_diagonal F,d) * (j + (Sum ((Len F) | (i -' 1)))),(k + (Sum ((Width F) | (i -' 1)))) )
A3: i <= len F by A1, FINSEQ_3:27;
set Fi = F . i;
set L = Len F;
set W = Width F;
set B = block_diagonal F,d;
A4: ( len (block_diagonal F,d) = Sum (Len F) & width (block_diagonal F,d) = Sum (Width F) ) by Def5;
A5: ( len F = len (Len F) & len F = len (Width F) ) by FINSEQ_1:def 18;
A6: ( dom F = dom (Len F) & dom F = dom (Width F) ) by Def3, Def4;
set jS = j + (Sum ((Len F) | (i -' 1)));
set kS = k + (Sum ((Width F) | (i -' 1)));
A7: ( j in dom (F . i) & k in Seg (width (F . i)) ) by A2, ZFMISC_1:106;
then ( j in Seg (len (F . i)) & (Len F) . i = (Len F) /. i & (Len F) . i = len (F . i) & (Width F) . i = (Width F) /. i & (Width F) . i = width (F . i) ) by A1, A6, Def3, Def4, FINSEQ_1:def 3, PARTFUN1:def 8;
then A8: ( j + (Sum ((Len F) | (i -' 1))) in Seg (Sum ((Len F) | i)) & min (Len F),(j + (Sum ((Len F) | (i -' 1)))) = i & k + (Sum ((Width F) | (i -' 1))) in Seg (Sum ((Width F) | i)) ) by A6, A1, A7, Th10;
i in NAT by ORDINAL1:def 13;
then ( Sum ((Len F) | i) <= Sum ((Len F) | (len F)) & Sum ((Width F) | i) <= Sum ((Width F) | (len F)) & (Len F) | (len F) = Len F & (Width F) | (len F) = Width F ) by A5, A3, FINSEQ_1:79, POLYNOM3:18;
then ( Seg (Sum ((Len F) | i)) c= Seg (Sum (Len F)) & Seg (Sum ((Width F) | i)) c= Seg (Sum (Width F)) ) by FINSEQ_1:7;
then [(j + (Sum ((Len F) | (i -' 1)))),(k + (Sum ((Width F) | (i -' 1))))] in [:(Seg (len (block_diagonal F,d))),(Seg (width (block_diagonal F,d))):] by A8, A4, ZFMISC_1:106;
hence A9: [(j + (Sum ((Len F) | (i -' 1)))),(k + (Sum ((Width F) | (i -' 1))))] in Indices (block_diagonal F,d) by FINSEQ_1:def 3; :: thesis: (F . i) * j,k = (block_diagonal F,d) * (j + (Sum ((Len F) | (i -' 1)))),(k + (Sum ((Width F) | (i -' 1))))
0 < k by A7, FINSEQ_1:3;
then A10: ( (Sum ((Width F) | (i -' 1))) + 0 < k + (Sum ((Width F) | (i -' 1))) & (Sum ((Len F) | (i -' 1))) + 0 <= j + (Sum ((Len F) | (i -' 1))) & k + (Sum ((Width F) | (i -' 1))) <= Sum ((Width F) | i) ) by A8, FINSEQ_1:3, XREAL_1:8;
then ( (j + (Sum ((Len F) | (i -' 1)))) -' (Sum ((Len F) | (i -' 1))) = (j + (Sum ((Len F) | (i -' 1)))) - (Sum ((Len F) | (i -' 1))) & (k + (Sum ((Width F) | (i -' 1)))) -' (Sum ((Width F) | (i -' 1))) = (k + (Sum ((Width F) | (i -' 1)))) - (Sum ((Width F) | (i -' 1))) ) by XREAL_1:235;
hence (F . i) * j,k = (block_diagonal F,d) * (j + (Sum ((Len F) | (i -' 1)))),(k + (Sum ((Width F) | (i -' 1)))) by A8, A9, A10, Def5; :: thesis: verum