let D be non empty set ; :: thesis:
let d be Element of D; :: thesis:
let F be FinSequence_of_Matrix of D; :: thesis:
let i, j, k be Nat; :: thesis:
assume that
A1: i in dom F and
A2: [j,k] in Indices (F . i) ; :: thesis:
set Fi = F . i;
A3: k in Seg (width (F . i)) by A2, ZFMISC_1:87;
set L = Len F;
len F = len (Len F) by CARD_1:def 7;
then A4: (Len F) | (len F) = Len F by FINSEQ_1:58;
A5: i <= len F by A1, FINSEQ_3:25;
then Sum ((Len F) | i) <= Sum ((Len F) | (len F)) by POLYNOM3:18;
then A6: Seg (Sum ((Len F) | i)) c= Seg (Sum (Len F)) by A4, FINSEQ_1:5;
A7: dom F = dom (Len F) by Def3;
then A8: (Len F) . i = (Len F) /. i by A1, PARTFUN1:def 6;
set W = Width F;
A9: dom F = dom (Width F) by Def4;
then A10: (Width F) . i = (Width F) /. i by A1, PARTFUN1:def 6;
set kS = k + (Sum ((Width F) | (i -' 1)));
(Width F) . i = width (F . i) by A1, A9, Def4;
then A11: k + (Sum ((Width F) | (i -' 1))) in Seg (Sum ((Width F) | i)) by A1, A9, A3, A10, Th10;
then A12: k + (Sum ((Width F) | (i -' 1))) <= Sum ((Width F) | i) by FINSEQ_1:1;
len F = len (Width F) by CARD_1:def 7;
then A13: (Width F) | (len F) = Width F by FINSEQ_1:58;
set B = block_diagonal (F,d);
A14: len (block_diagonal (F,d)) = Sum (Len F) by Def5;
A15: width (block_diagonal (F,d)) = Sum (Width F) by Def5;
set jS = j + (Sum ((Len F) | (i -' 1)));
j in dom (F . i) by A2, ZFMISC_1:87;
then A16: j in Seg (len (F . i)) by FINSEQ_1:def 3;
Sum ((Width F) | i) <= Sum ((Width F) | (len F)) by A5, POLYNOM3:18;
then A17: Seg (Sum ((Width F) | i)) c= Seg (Sum (Width F)) by A13, FINSEQ_1:5;
(Sum ((Len F) | (i -' 1))) + 0 <= j + (Sum ((Len F) | (i -' 1))) by XREAL_1:6;
then A18: (j + (Sum ((Len F) | (i -' 1)))) -' (Sum ((Len F) | (i -' 1))) = (j + (Sum ((Len F) | (i -' 1)))) - (Sum ((Len F) | (i -' 1))) by XREAL_1:233;
A19: (Len F) . i = len (F . i) by A1, A7, Def3;
then A20: min ((Len F),(j + (Sum ((Len F) | (i -' 1))))) = i by A1, A7, A16, A8, Th10;
j + (Sum ((Len F) | (i -' 1))) in Seg (Sum ((Len F) | i)) by A1, A7, A16, A8, A19, Th10;
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 A14, A15, A11, A6, A17, ZFMISC_1:87;
hence A21: [(j + (Sum ((Len F) | (i -' 1)))),(k + (Sum ((Width F) | (i -' 1))))] in Indices (block_diagonal (F,d)) by FINSEQ_1:def 3; :: thesis:
0 < k by A3;
then A22: (Sum ((Width F) | (i -' 1))) + 0 < k + (Sum ((Width F) | (i -' 1))) by XREAL_1:6;
then (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:233;
hence (F . i) * (j,k) = (block_diagonal (F,d)) * ((j + (Sum ((Len F) | (i -' 1)))),(k + (Sum ((Width F) | (i -' 1))))) by A20, A21, A22, A12, A18, Def5; :: thesis: