:: deftheorem Def3 defines width MATRIX_0:def 3 :
for M being tabular FinSequence
for b₂ being Nat holds
( ( len M > 0 implies ( b₂ = width M iff ex s being FinSequence st
( s in rng M & len s = b₂ ) ) ) & ( not len M > 0 implies ( b₂ = width M iff b₂ = 0 ) ) );