theorem Th44: :: MATRIXJ1:44

for i being Nat
for K being Field
for a being Element of K
for A being Matrix of K
for G being FinSequence_of_Matrix of K st i in Seg (width A) holds
DelCol ((block_diagonal ((G ^ <*A*>),a)),(i + (Sum (Width G)))) = block_diagonal ((G ^ <*(DelCol (A,i))*>),a)