:: deftheorem Def3 defines FinSequenceSet FINSEQ_2:def 3 :
for D, b₂ being set holds
( b₂ is FinSequenceSet of D iff for a being object st a in b₂ holds
a is FinSequence of D );