reconsider f = _V as the_Vertices_of G1 -defined the_Vertices_of G2 -valued Function by TARSKI:1;
( dom f c= the_Vertices_of G1 & rng f c= the_Vertices_of G2 ) ;
hence _V is PartFunc of (the_Vertices_of G1),(the_Vertices_of G2) by RELSET_1:4; :: thesis: verum