theorem Th42: :: MATRIXJ1:42

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