consider p being FinSequence such that
A1: ( rng p = the_Vertices_of G & p is one-to-one ) by FINSEQ_4:73;
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; :: thesis: verum