:: deftheorem Def11 defines len MATRIX_1:def 15 :
for P being non empty permutational set
for b₂ being Nat holds
( b₂ = len P iff ex s being FinSequence st
( s in P & b₂ = len s ) );