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: for v, w being Vertex of G1 st v in dom f & w in dom f & v,w are_adjacent holds
f /. v,f /. w are_adjacent

let v, w be Vertex of G1; :: thesis: ( v in dom f & w in dom f & v,w are_adjacent implies f /. v,f /. w are_adjacent )
assume A1: ( v in dom f & w in dom f & v,w are_adjacent ) ; :: thesis: f /. v,f /. w are_adjacent
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: verum

end;

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

proof

let v, w, e be object ; :: according to GLIB_011:def 2 :: thesis: ( v in dom f & w in dom f & e DJoins v,w,G1 implies ex e9 being object st e9 DJoins f . v,f . w,G2 )
assume A2: ( v in dom f & w in dom f & e DJoins v,w,G1 ) ; :: thesis: ex e9 being object st e9 DJoins f . v,f . w,G2
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: verum

end;