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