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

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