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 Fi = F . i;
set L = Len F;
set W = Width F;
set SL1 = Sum ((Len F) | (i -' 1));
set SW1 = Sum ((Width F) | (i -' 1));
set SL = Sum ((Len F) | i);
set SW = Sum ((Width F) | i);
set B = block_diagonal F,d;
A2: ( dom F = dom (Len F) & dom F = dom (Width F) ) by Def3, Def4;
A3: ( (Sum ((Len F) | (i -' 1))) + ((Len F) . i) = Sum ((Len F) | i) & (Sum ((Width F) | (i -' 1))) + ((Width F) . i) = Sum ((Width F) | i) ) by A1, A2, Lm2;
A4: ( width (F . i) = (Width F) . i & len (F . i) = (Len F) . i ) by A1, A2, Def3, Def4;
( i -' 1 <= i & i in NAT ) by NAT_D:35, ORDINAL1:def 13;
then ( Sum ((Len F) | (i -' 1)) <= Sum ((Len F) | i) & Sum ((Width F) | (i -' 1)) <= Sum ((Width F) | i) ) by POLYNOM3:18;
then A5: ( Seg (Sum ((Len F) | (i -' 1))) c= Seg (Sum ((Len F) | i)) & Seg (Sum ((Width F) | (i -' 1))) c= Seg (Sum ((Width F) | i)) ) by FINSEQ_1:7;
then A6: 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 A3, FINSEQ_1:78
.= len (F . i) by A1, A2, Def3 ;
A7: 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 A5, 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 A3, FINSEQ_1:78
.= width (F . i) by A1, A2, Def4 ;
reconsider FI = F . i as Matrix of len (F . i), width (F . i),D by MATRIX_2:7;

now

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 A8: [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
A9: 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 A6, A7, MATRIX_1:27;
( j in dom FI & k in Seg ((Width F) . i) & dom FI = Seg ((Len F) . i) ) by A4, A8, FINSEQ_1:def 3, ZFMISC_1:106;
then ( (Sgm ((Seg (Sum ((Len F) | i))) \ (Seg (Sum ((Len F) | (i -' 1)))))) . j = j + (Sum ((Len F) | (i -' 1))) & (Sgm ((Seg (Sum ((Width F) | i))) \ (Seg (Sum ((Width F) | (i -' 1)))))) . k = k + (Sum ((Width F) | (i -' 1))) ) by A3, 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 A8, A9, MATRIX13:def 1
.= (F . i) * j,k by A1, A8, 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 A6, A7, MATRIX_1:28; :: thesis: verum