:: deftheorem Def1 defines PVertexMapping GLIB_011:def 1 :
for G1, G2 being _Graph
for b₃ being PartFunc of (the_Vertices_of G1),(the_Vertices_of G2) holds
( b₃ is PVertexMapping of G1,G2 iff for v, w being Vertex of G1 st v in dom b₃ & w in dom b₃ & v,w are_adjacent holds
b₃ /. v,b₃ /. w are_adjacent );