for m being Nat
for p being b₁ -element FinSequence holds len p = m by CARD_1:def 7;