:: deftheorem Def2 defines FinSequence-like FINSEQ_1:def 2 :
for IT being Relation holds
( IT is FinSequence-like iff ex n being Nat st dom IT = Seg n );