let G1, G2 be _Graph; :: thesis: for f being PartFunc of (the_Vertices_of G1),(the_Vertices_of G2) holds
( f is PVertexMapping of G1,G2 iff for v, w, e being object st v in dom f & w in dom f & e Joins v,w,G1 holds
ex e9 being object st e9 Joins f . v,f . w,G2 )
let f be PartFunc of (the_Vertices_of G1),(the_Vertices_of G2); :: thesis: ( f is PVertexMapping of G1,G2 iff for v, w, e being object st v in dom f & w in dom f & e Joins v,w,G1 holds
ex e9 being object st e9 Joins f . v,f . w,G2 )

hereby :: thesis: ( ( for v, w, e being object st v in dom f & w in dom f & e Joins v,w,G1 holds
ex e9 being object st e9 Joins f . v,f . w,G2 ) implies f is PVertexMapping of G1,G2 )

assume A1: f is PVertexMapping of G1,G2 ; :: thesis: for v, w, e being object st v in dom f & w in dom f & e Joins v,w,G1 holds
ex e9 being object st e9 Joins f . v,f . w,G2
let v, w, e be object ; :: thesis: ( v in dom f & w in dom f & e Joins v,w,G1 implies ex e9 being object st e9 Joins f . v,f . w,G2 )
assume A2: ( v in dom f & w in dom f & e Joins v,w,G1 ) ; :: thesis: ex e9 being object st e9 Joins f . v,f . w,G2
then reconsider v0 = v, w0 = w as Vertex of G1 ;
v0,w0 are_adjacent by A2, CHORD:def 3;
then consider e9 being object such that
A3: e9 Joins f /. v0,f /. w0,G2 by A1, A2, Def1, CHORD:def 3;
take e9 = e9; :: thesis: e9 Joins f . v,f . w,G2
( f /. v0 = f . v & f /. w0 = f . w ) by A2, PARTFUN1:def 6;
hence e9 Joins f . v,f . w,G2 by A3; :: thesis: verum

end;

assume A4: for v, w, e being object st v in dom f & w in dom f & e Joins v,w,G1 holds
ex e9 being object st e9 Joins f . v,f . w,G2 ; :: thesis: f is PVertexMapping of G1,G2
let v, w be Vertex of G1; :: according to GLIB_011:def 1 :: thesis: ( v in dom f & w in dom f & v,w are_adjacent implies f /. v,f /. w are_adjacent )
assume A5: ( v in dom f & w in dom f ) ; :: thesis: ( not v,w are_adjacent or f /. v,f /. w are_adjacent )
assume v,w are_adjacent ; :: thesis: f /. v,f /. w are_adjacent
then consider e being object such that
A6: e Joins v,w,G1 by CHORD:def 3;
consider e9 being object such that
A7: e9 Joins f . v,f . w,G2 by A4, A5, A6;
( f /. v = f . v & f /. w = f . w ) by A5, PARTFUN1:def 6;
hence f /. v,f /. w are_adjacent by A7, CHORD:def 3; :: thesis: verum