:: deftheorem Def3 defines FinSequence-yielding PRE_POLY:def 3 :
for IT being Function holds
( IT is FinSequence-yielding iff for x being object st x in dom IT holds
IT . x is FinSequence );