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_0:51;
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;
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:5;
then A7: 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:44
.= (Sum ((Len F) | i)) - (card (Seg (Sum ((Len F) | (i -' 1))))) by FINSEQ_1:57
.= ((Sum ((Len F) | (i -' 1))) + ((Len F) . i)) - (Sum ((Len F) | (i -' 1))) by A4, FINSEQ_1:57
.= len (F . i) by A1, A2, Def3 ;
Sum ((Width F) | (i -' 1)) <= Sum ((Width F) | i) by NAT_D:35, POLYNOM3:18;
then Seg (Sum ((Width F) | (i -' 1))) c= Seg (Sum ((Width F) | i)) by FINSEQ_1:5;
then A8: 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:44
.= (Sum ((Width F) | i)) - (card (Seg (Sum ((Width F) | (i -' 1))))) by FINSEQ_1:57
.= ((Sum ((Width F) | (i -' 1))) + ((Width F) . i)) - (Sum ((Width F) | (i -' 1))) by A6, FINSEQ_1:57
.= width (F . i) by A1, A5, Def4 ;
A9: width (F . i) = (Width F) . i by A1, A5, Def4;

now :: thesis: for j, k being Nat st [j,k] in Indices FI holds
(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)

A10: 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 A7, A8, MATRIX_0:26;
A11: 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 A12: [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 A9, A12, ZFMISC_1:87;
then A13: (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 A12, ZFMISC_1:87;
then (Sgm ((Seg (Sum ((Len F) | i))) \ (Seg (Sum ((Len F) | (i -' 1)))))) . j = j + (Sum ((Len F) | (i -' 1))) by A4, A11, 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 A12, A10, A13, MATRIX13:def 1
.= (F . i) * (j,k) by A1, A12, 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 A7, A8, MATRIX_0:27; :: thesis: verum