let i be Nat; :: thesis: for D being non empty set
for d being Element of D
for F being FinSequence_of_Matrix of D st i in dom F holds
F . i = Segm (block_diagonal F,d),((Seg (Sum ((Len F) | i))) \ (Seg (Sum ((Len F) | (i -' 1))))),((Seg (Sum ((Width F) | i))) \ (Seg (Sum ((Width F) | (i -' 1)))))
let D be non empty set ; :: thesis: for d being Element of D
for F being FinSequence_of_Matrix of D st i in dom F holds
F . i = Segm (block_diagonal F,d),((Seg (Sum ((Len F) | i))) \ (Seg (Sum ((Len F) | (i -' 1))))),((Seg (Sum ((Width F) | i))) \ (Seg (Sum ((Width F) | (i -' 1)))))
let d be Element of D; :: thesis: for F being FinSequence_of_Matrix of D st i in dom F holds
F . i = Segm (block_diagonal F,d),((Seg (Sum ((Len F) | i))) \ (Seg (Sum ((Len F) | (i -' 1))))),((Seg (Sum ((Width F) | i))) \ (Seg (Sum ((Width F) | (i -' 1)))))
let F be FinSequence_of_Matrix of D; :: thesis: ( i in dom F implies F . i = Segm (block_diagonal F,d),((Seg (Sum ((Len F) | i))) \ (Seg (Sum ((Len F) | (i -' 1))))),((Seg (Sum ((Width F) | i))) \ (Seg (Sum ((Width F) | (i -' 1))))) )
assume A1: i in dom F ; :: thesis: F . i = Segm (block_diagonal F,d),((Seg (Sum ((Len F) | i))) \ (Seg (Sum ((Len F) | (i -' 1))))),((Seg (Sum ((Width F) | i))) \ (Seg (Sum ((Width F) | (i -' 1)))))
set L = Len F;
set Fi = F . i;
A2: dom F = dom (Len F) by Def3;
then A3: len (F . i) = (Len F) . i by A1, Def3;
set SL = Sum ((Len F) | i);
set SL1 = Sum ((Len F) | (i -' 1));
A4: (Sum ((Len F) | (i -' 1))) + ((Len F) . i) = Sum ((Len F) | i) by A1, A2, Lm2;
reconsider FI = F . i as Matrix of len (F . i), width (F . i),D by MATRIX_2:7;
set B = block_diagonal F,d;
set W = Width F;
set SW1 = Sum ((Width F) | (i -' 1));
set SW = Sum ((Width F) | i);
A5: dom F = dom (Width F) by Def4;
then A6: (Sum ((Width F) | (i -' 1))) + ((Width F) . i) = Sum ((Width F) | i) by A1, Lm2;
A7: i in NAT by ORDINAL1:def 13;
then Sum ((Len F) | (i -' 1)) <= Sum ((Len F) | i) by NAT_D:35, POLYNOM3:18;
then Seg (Sum ((Len F) | (i -' 1))) c= Seg (Sum ((Len F) | i)) by FINSEQ_1:7;
then A8: card ((Seg (Sum ((Len F) | i))) \ (Seg (Sum ((Len F) | (i -' 1))))) = (card (Seg (Sum ((Len F) | i)))) - (card (Seg (Sum ((Len F) | (i -' 1))))) by CARD_2:63
.= (Sum ((Len F) | i)) - (card (Seg (Sum ((Len F) | (i -' 1))))) by FINSEQ_1:78
.= ((Sum ((Len F) | (i -' 1))) + ((Len F) . i)) - (Sum ((Len F) | (i -' 1))) by A4, FINSEQ_1:78
.= len (F . i) by A1, A2, Def3 ;
Sum ((Width F) | (i -' 1)) <= Sum ((Width F) | i) by A7, NAT_D:35, POLYNOM3:18;
then Seg (Sum ((Width F) | (i -' 1))) c= Seg (Sum ((Width F) | i)) by FINSEQ_1:7;
then A9: card ((Seg (Sum ((Width F) | i))) \ (Seg (Sum ((Width F) | (i -' 1))))) = (card (Seg (Sum ((Width F) | i)))) - (card (Seg (Sum ((Width F) | (i -' 1))))) by CARD_2:63
.= (Sum ((Width F) | i)) - (card (Seg (Sum ((Width F) | (i -' 1))))) by FINSEQ_1:78
.= ((Sum ((Width F) | (i -' 1))) + ((Width F) . i)) - (Sum ((Width F) | (i -' 1))) by A6, FINSEQ_1:78
.= width (F . i) by A1, A5, Def4 ;
A10: width (F . i) = (Width F) . i by A1, A5, Def4;

now

A11: Indices FI = Indices (Segm (block_diagonal F,d),((Seg (Sum ((Len F) | i))) \ (Seg (Sum ((Len F) | (i -' 1))))),((Seg (Sum ((Width F) | i))) \ (Seg (Sum ((Width F) | (i -' 1)))))) by A8, A9, MATRIX_1:27;
A12: dom FI = Seg ((Len F) . i) by A3, FINSEQ_1:def 3;
let j, k be Nat; :: thesis: ( [j,k] in Indices FI implies (Segm (block_diagonal F,d),((Seg (Sum ((Len F) | i))) \ (Seg (Sum ((Len F) | (i -' 1))))),((Seg (Sum ((Width F) | i))) \ (Seg (Sum ((Width F) | (i -' 1)))))) * j,k = (F . i) * j,k )
assume A13: [j,k] in Indices FI ; :: thesis: (Segm (block_diagonal F,d),((Seg (Sum ((Len F) | i))) \ (Seg (Sum ((Len F) | (i -' 1))))),((Seg (Sum ((Width F) | i))) \ (Seg (Sum ((Width F) | (i -' 1)))))) * j,k = (F . i) * j,k
k in Seg ((Width F) . i) by A10, A13, ZFMISC_1:106;
then A14: (Sgm ((Seg (Sum ((Width F) | i))) \ (Seg (Sum ((Width F) | (i -' 1)))))) . k = k + (Sum ((Width F) | (i -' 1))) by A6, MATRIX15:8;
j in dom FI by A13, ZFMISC_1:106;
then (Sgm ((Seg (Sum ((Len F) | i))) \ (Seg (Sum ((Len F) | (i -' 1)))))) . j = j + (Sum ((Len F) | (i -' 1))) by A4, A12, MATRIX15:8;
hence (Segm (block_diagonal F,d),((Seg (Sum ((Len F) | i))) \ (Seg (Sum ((Len F) | (i -' 1))))),((Seg (Sum ((Width F) | i))) \ (Seg (Sum ((Width F) | (i -' 1)))))) * j,k = (block_diagonal F,d) * (j + (Sum ((Len F) | (i -' 1)))),(k + (Sum ((Width F) | (i -' 1)))) by A13, A11, A14, MATRIX13:def 1
.= (F . i) * j,k by A1, A13, Th30 ;
:: thesis: verum

end;

hence F . i = Segm (block_diagonal F,d),((Seg (Sum ((Len F) | i))) \ (Seg (Sum ((Len F) | (i -' 1))))),((Seg (Sum ((Width F) | i))) \ (Seg (Sum ((Width F) | (i -' 1))))) by A8, A9, MATRIX_1:28; :: thesis: verum