theorem Th12: :: MATRIXJ1:12

for D being non empty set holds {} is FinSequence_of_Matrix of D