:: deftheorem Def2 defines -size MATRIX_0:def 2 :
for D being non empty set
for m, n being Nat
for M being Matrix of D holds
( M is m,n -size iff ( len M = m & ( for p being FinSequence of D st p in rng M holds
len p = n ) ) );