take {} ; :: thesis: {} is FinSubsequence-like
take len {} ; :: according to FINSEQ_1:def 12 :: thesis: dom {} c= Seg (len {} )
thus dom {} c= Seg (len {} ) ; :: thesis: verum