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