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 dom A & width A = width (DelLine (A,i)) holds
DelLine ((block_diagonal ((<*A*> ^ G),a)),i) = block_diagonal ((<*(DelLine (A,i))*> ^ G),a)