consider p being FinSequence such that
A1: rng p = the_Vertices_of G and
A2: p is one-to-one by FINSEQ_4:58;
reconsider p = p as FinSequence of the_Vertices_of G by A1, FINSEQ_1:def 4;
take p ; :: thesis: ( p is one-to-one & rng p = the_Vertices_of G )
thus ( p is one-to-one & rng p = the_Vertices_of G ) by A1, A2; :: thesis: verum