:: deftheorem Def4 defines len MATRIX_1:def 11 :
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 ) );