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

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