:: deftheorem Def11 defines * FINSEQ_1:def 11 :
for D, b₂ being set holds
( b₂ = D * iff for x being object holds
( x in b₂ iff x is FinSequence of D ) );