let IT be Subset of fs; :: thesis: IT is FinSubsequence-like
take len fs ; :: according to FINSEQ_1:def 12 :: thesis: dom IT c= Seg (len fs)
dom IT c= dom fs by RELAT_1:11;
hence dom IT c= Seg (len fs) by FINSEQ_1:def 3; :: thesis: verum