theorem Th30: :: MATRIXJ1:30

for D being non empty set
for d being Element of D
for F being FinSequence_of_Matrix of D
for i, j, k being Nat st i in dom F & [j,k] in Indices (F . i) holds
( [(j + (Sum ((Len F) | (i -' 1)))),(k + (Sum ((Width F) | (i -' 1))))] in Indices (block_diagonal (F,d)) & (F . i) * (j,k) = (block_diagonal (F,d)) * ((j + (Sum ((Len F) | (i -' 1)))),(k + (Sum ((Width F) | (i -' 1))))) )