set f = the empty PartFunc of (the_Vertices_of G1),(the_Vertices_of G2);
for v, w being Vertex of G1 st v in dom the empty PartFunc of (the_Vertices_of G1),(the_Vertices_of G2) & w in dom the empty PartFunc of (the_Vertices_of G1),(the_Vertices_of G2) & v,w are_adjacent holds
the empty PartFunc of (the_Vertices_of G1),(the_Vertices_of G2) /. v, the empty PartFunc of (the_Vertices_of G1),(the_Vertices_of G2) /. w are_adjacent ;
then reconsider f = the empty PartFunc of (the_Vertices_of G1),(the_Vertices_of G2) as PVertexMapping of G1,G2 by Def1;
take f ; :: thesis: ( f is empty & f is one-to-one & f is directed & f is continuous & f is Dcontinuous )
thus ( f is empty & f is one-to-one & f is directed & f is continuous & f is Dcontinuous ) ; :: thesis: verum