:: deftheorem Def12 defines FinSubsequence-like FINSEQ_1:def 12 :
for IT being Function holds
( IT is FinSubsequence-like iff ex k being Nat st dom IT c= Seg k );