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;
A4: i in NAT by ORDINAL1:def 12;
len F = len (Len F) by CARD_1:def 7;
then A5: (Len F) | (len F) = Len F by FINSEQ_1:58;
A6: i <= len F by A1, FINSEQ_3:25;
then Sum ((Len F) | i) <= Sum ((Len F) | (len F)) by A4, POLYNOM3:18;
then A7: Seg (Sum ((Len F) | i)) c= Seg (Sum (Len F)) by A5, FINSEQ_1:5;
A8: dom F = dom (Len F) by Def3;
then A9: (Len F) . i = (Len F) /. i by A1, PARTFUN1:def 6;
set W = Width F;
A10: dom F = dom (Width F) by Def4;
then A11: (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, A10, Def4;
then A12: k + (Sum ((Width F) | (i -' 1))) in Seg (Sum ((Width F) | i)) by A1, A10, A3, A11, Th10;
then A13: 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 A14: (Width F) | (len F) = Width F by FINSEQ_1:58;
set B = block_diagonal (F,d);
A15: len (block_diagonal (F,d)) = Sum (Len F) by Def5;
A16: 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 A17: j in Seg (len (F . i)) by FINSEQ_1:def 3;
Sum ((Width F) | i) <= Sum ((Width F) | (len F)) by A6, A4, POLYNOM3:18;
then A18: Seg (Sum ((Width F) | i)) c= Seg (Sum (Width F)) by A14, FINSEQ_1:5;
(Sum ((Len F) | (i -' 1))) + 0 <= j + (Sum ((Len F) | (i -' 1))) by XREAL_1:6;
then A19: (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;
A20: (Len F) . i = len (F . i) by A1, A8, Def3;
then A21: min ((Len F),(j + (Sum ((Len F) | (i -' 1))))) = i by A1, A8, A17, A9, Th10;
j + (Sum ((Len F) | (i -' 1))) in Seg (Sum ((Len F) | i)) by A1, A8, A17, A9, A20, 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 A15, A16, A12, A7, A18, ZFMISC_1:87;
hence A22: [(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, FINSEQ_1:1;
then A23: (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 A21, A22, A23, A13, A19, Def5; :: thesis: