theorem Th47: :: MATRIXJ1:47

for i, j, n being Nat
for K being Field
for a being Element of K
for R being FinSequence_of_Square-Matrix of K
for A being Matrix of n,K st i in dom A & j in Seg n holds
Deleting ((block_diagonal ((<*A*> ^ R),a)),i,j) = block_diagonal ((<*(Deleting (A,i,j))*> ^ R),a)