theorem Th151: :: FINSEQ_3:153

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