theorem Th29: :: MATRIXJ1:29

for i, j being Nat
for D being non empty set
for d being Element of D
for F1, F2 being FinSequence_of_Matrix of D st [i,j] in Indices (block_diagonal ((F1 ^ F2),d)) & ( ( i <= Sum (Len F1) & j > Sum (Width F1) ) or ( i > Sum (Len F1) & j <= Sum (Width F1) ) ) holds
(block_diagonal ((F1 ^ F2),d)) * (i,j) = d