let E be Enumeration of X; :: thesis: E is one-to-one FinSequence of X
rng E = X by RLAFFIN3:def 1;
hence E is one-to-one FinSequence of X by FINSEQ_1:def 4; :: thesis: verum