:: deftheorem Def3 defines len FINSEQ_1:def 3 :
for p being FinSequence
for b₂ being Element of NAT holds
( b₂ = len p iff Seg b₂ = dom p );