:: deftheorem Def4 defines FinSequence FINSEQ_1:def 4 :
for D being set
for b₂ being FinSequence holds
( b₂ is FinSequence of D iff rng b₂ c= D );