theorem Th43: :: MATRIXJ1:43

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 ((<*A*> ^ G),a)),i) = block_diagonal ((<*(DelCol (A,i))*> ^ G),a)