for G1, G2 being _Graph
for f being PartFunc of (the_Vertices_of G1),(the_Vertices_of G2) holds
( f is directed PVertexMapping of G1,G2 iff for v, w, e being object st v in dom f & w in dom f & e DJoins v,w,G1 holds
ex e9 being object st e9 DJoins f . v,f . w,G2 )