theorem :: MATRIXJ1:22

for D being non empty set
for d being Element of D
for F being FinSequence_of_Matrix of D st F = {} holds
block_diagonal (F,d) = {}