:: deftheorem defines empty-yielding MATRIX_0:def 10 :
for D being non empty set
for M being Matrix of D holds
( M is empty-yielding iff ( 0 = len M or 0 = width M ) );