theorem :: MATRIXJ1:72

for K being Field
for a1, a2 being Element of K
for R1, R2 being FinSequence_of_Square-Matrix of K st Len R1 = Len R2 & Width R1 = Width R2 holds
(block_diagonal (R1,a1)) + (block_diagonal (R2,a2)) = block_diagonal ((R1 (+) R2),(a1 + a2))