set v1 = the Vertex of G1;
set v2 = the Vertex of G2;
set f = the Vertex of G1 .--> the Vertex of G2;
the Vertex of G1 .--> the Vertex of G2 = { the Vertex of G1} --> the Vertex of G2 by FUNCOP_1:def 9;
then reconsider f = the Vertex of G1 .--> the Vertex of G2 as one-to-one PartFunc of (the_Vertices_of G1),(the_Vertices_of G2) ;

now :: thesis:

let v, w be Vertex of G1; :: thesis:
assume A1: ( v in dom f & w in dom f & v,w are_adjacent ) ; :: thesis:
then ( v = the Vertex of G1 & w = the Vertex of G1 ) by FUNCOP_1:75;
hence f /. v,f /. w are_adjacent by A1, GLIB_009:39; :: thesis:

end;

then reconsider f = f as PVertexMapping of G1,G2 by Def1;
take f ; :: thesis:
thus ( not f is empty & f is one-to-one ) ; :: thesis:
thus f is directed :: thesis:

proof

let v, w, e be object ; :: according to GLIB_011:def 2 :: thesis:
assume A2: ( v in dom f & w in dom f & e DJoins v,w,G1 ) ; :: thesis:
then ( v = the Vertex of G1 & w = the Vertex of G1 ) by FUNCOP_1:75;
then e Joins the Vertex of G1, the Vertex of G1,G1 by A2, GLIB_000:16;
hence ex e9 being object st e9 DJoins f . v,f . w,G2 by GLIB_000:18; :: thesis:

end;

thus f is continuous :: thesis:

proof

let v, w be Vertex of G1; :: according to GLIB_011:def 3 :: thesis:
assume A3: ( v in dom f & w in dom f & f /. v,f /. w are_adjacent ) ; :: thesis:
then ( v = the Vertex of G1 & w = the Vertex of G1 ) by FUNCOP_1:75;
hence v,w are_adjacent by A3, GLIB_009:39; :: thesis:

end;

thus f is Dcontinuous :: thesis:

proof

let v, w, e9 be object ; :: according to GLIB_011:def 4 :: thesis:
assume A4: ( v in dom f & w in dom f & e9 DJoins f . v,f . w,G2 ) ; :: thesis:
then ( v = the Vertex of G1 & w = the Vertex of G1 ) by FUNCOP_1:75;
then e9 Joins f . the Vertex of G1,f . the Vertex of G1,G2 by A4, GLIB_000:16;
hence ex e being object st e DJoins v,w,G1 by GLIB_000:18; :: thesis:

end;