theorem :: MATRIX_4:58

for D being non empty set
for M being Matrix of D st len M > 0 holds
for n being Nat holds
( M is Matrix of n, width M,D iff n = len M ) by MATRIX_0:20, MATRIX_0:def 2;