theorem :: MATRIXJ1:48

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 ((R ^ <*A*>),a)),(i + (Sum (Len R))),(j + (Sum (Len R)))) = block_diagonal ((R ^ <*(Deleting (A,i,j))*>),a)