consider v1 being object such that
A1: ex e1 being object st e1 Joins v1,v1,G1 by GLIB_000:18;
reconsider v1 = v1 as Vertex of G1 by A1, GLIB_000:13;
consider v2 being object such that
A2: ex e2 being object st e2 Joins v2,v2,G2 by GLIB_000:18;
reconsider v2 = v2 as Vertex of G2 by A2, GLIB_000:13;
set f = v1 .--> v2;
v1 .--> v2 = {v1} --> v2 by FUNCOP_1:def 9;
then reconsider f = v1 .--> v2 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 A3: ( v in dom f & w in dom f & v,w are_adjacent ) ; :: thesis:
then ( v = v1 & w = v1 ) by FUNCOP_1:75;
then ( f /. v = f . v1 & f /. w = f . v1 ) by A3, PARTFUN1:def 6;
then ( f /. v = v2 & f /. w = v2 ) by FUNCOP_1:72;
hence f /. v,f /. w are_adjacent by A2, CHORD:def 3; :: 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 ( v in dom f & w in dom f & e DJoins v,w,G1 ) ; :: thesis:
then ( v = v1 & w = v1 ) by FUNCOP_1:75;
then A4: ( f . v = v2 & f . w = v2 ) by FUNCOP_1:72;
then consider e2 being object such that
A5: e2 Joins f . v,f . w,G2 by A2;
take e2 ; :: thesis:
thus e2 DJoins f . v,f . w,G2 by A4, A5, GLIB_000:16; :: thesis:

end;

thus f is continuous :: thesis:

proof

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

end;

thus f is Dcontinuous :: thesis:

proof

let v, w, e9 be object ; :: according to GLIB_011:def 4 :: thesis:
assume ( v in dom f & w in dom f & e9 DJoins f . v,f . w,G2 ) ; :: thesis:
then A6: ( v = v1 & w = v1 ) by FUNCOP_1:75;
then consider e1 being object such that
A7: e1 Joins v,w,G1 by A1;
take e1 ; :: thesis:
thus e1 DJoins v,w,G1 by A6, A7, GLIB_000:16; :: thesis:

end;