:: deftheorem Def2 defines constituted-FinSeqs MONOID_0:def 2 :
for IT being 1-sorted holds
( IT is constituted-FinSeqs iff for a being Element of IT holds a is FinSequence );