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