theorem Th27: :: MATRIXJ1:27

for i, j being Nat
for D being non empty set
for d1, d2 being Element of D
for F1, F2 being FinSequence_of_Matrix of D holds
( [i,j] in Indices (block_diagonal (F2,d1)) iff ( i > 0 & j > 0 & [(i + (Sum (Len F1))),(j + (Sum (Width F1)))] in Indices (block_diagonal ((F1 ^ F2),d2)) ) )