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

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