theorem :: MATRIXJ1:45

for D being non empty set holds {} is FinSequence_of_Square-Matrix of D