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