:: deftheorem Def1 defines tabular MATRIX_0:def 1 :
for f being FinSequence holds
( f is tabular iff ex n being Nat st
for x being object st x in rng f holds
ex s being FinSequence st
( s = x & len s = n ) );