theorem :: MATRIXJ1:37

for i, m being Nat
for D being non empty set
for d being Element of D
for F being FinSequence_of_Matrix of D st i in Seg (Sum (Len F)) & m = min ((Len F),i) holds
Line ((block_diagonal (F,d)),i) = (((Sum (Width (F | (m -' 1)))) |-> d) ^ (Line ((F . m),(i -' (Sum (Len (F | (m -' 1)))))))) ^ (((Sum (Width F)) -' (Sum (Width (F | m)))) |-> d)