let E be Enumeration of A; :: thesis: E is one-to-one FinSequence of X

rng E = A by Def1;

hence E is one-to-one FinSequence of X by FINSEQ_1:def 4; :: thesis: verum

rng E = A by Def1;

hence E is one-to-one FinSequence of X by FINSEQ_1:def 4; :: thesis: verum