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