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:106;
set L = Len F;
A4: i in NAT by ORDINAL1:def 13;
len F = len (Len F) by FINSEQ_1:def 18;
then A5: (Len F) | (len F) = Len F by FINSEQ_1:79;
A6: i <= len F by A1, FINSEQ_3:27;
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:7;
A8: dom F = dom (Len F) by Def3;
then A9: (Len F) . i = (Len F) /. i by A1, PARTFUN1:def 8;
set W = Width F;
A10: dom F = dom (Width F) by Def4;
then A11: (Width F) . i = (Width F) /. i by A1, PARTFUN1:def 8;
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:3;
len F = len (Width F) by FINSEQ_1:def 18;
then A14: (Width F) | (len F) = Width F by FINSEQ_1:79;
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:106;
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:7;
(Sum ((Len F) | (i -' 1))) + 0 <= j + (Sum ((Len F) | (i -' 1))) by XREAL_1:8;
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:235;
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:106;
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:3;
then A23: (Sum ((Width F) | (i -' 1))) + 0 < k + (Sum ((Width F) | (i -' 1))) by XREAL_1:8;
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:235;
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: