:: deftheorem Def1 defines Enumeration RLAFFIN3:def 1 :
for X being finite set
for b₂ being one-to-one FinSequence holds
( b₂ is Enumeration of X iff rng b₂ = X );