theorem :: MATRIXJ1:38

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 (Width F)) & m = min ((Width F),i) holds
Col ((block_diagonal (F,d)),i) = (((Sum (Len (F | (m -' 1)))) |-> d) ^ (Col ((F . m),(i -' (Sum (Width (F | (m -' 1)))))))) ^ (((Sum (Len F)) -' (Sum (Len (F | m)))) |-> d)