take f = id (Seg n); :: thesis: ( f is one-to-one & f is FinSequence-like )
dom f = Seg n by RELAT_1:45;
hence ( f is one-to-one & f is FinSequence-like ) by FINSEQ_1:def 2; :: thesis: verum