let G1, G2 be _Graph; :: thesis: for f being PartFunc of (the_Vertices_of G1),(the_Vertices_of G2) holds
( f is directed PVertexMapping of G1,G2 iff for v, w, e being object st v in dom f & w in dom f & e DJoins v,w,G1 holds
ex e9 being object st e9 DJoins f . v,f . w,G2 )
let f be PartFunc of (the_Vertices_of G1),(the_Vertices_of G2); :: thesis: ( f is directed PVertexMapping of G1,G2 iff for v, w, e being object st v in dom f & w in dom f & e DJoins v,w,G1 holds
ex e9 being object st e9 DJoins f . v,f . w,G2 )
thus ( f is directed PVertexMapping of G1,G2 implies for v, w, e being object st v in dom f & w in dom f & e DJoins v,w,G1 holds
ex e9 being object st e9 DJoins f . v,f . w,G2 ) by Def2; :: thesis: ( ( for v, w, e being object st v in dom f & w in dom f & e DJoins v,w,G1 holds
ex e9 being object st e9 DJoins f . v,f . w,G2 ) implies f is directed PVertexMapping of G1,G2 )
assume A1: for v, w, e being object st v in dom f & w in dom f & e DJoins v,w,G1 holds
ex e9 being object st e9 DJoins f . v,f . w,G2 ; :: thesis: f is directed PVertexMapping of G1,G2

now :: 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 b₄ Joins f . e9,f . b₂,G2 )
assume A2: ( v in dom f & w in dom f & e Joins v,w,G1 ) ; :: thesis: ex e9 being object st b₄ Joins f . e9,f . b₂,G2

per cases then ( e DJoins v,w,G1 or e DJoins w,v,G1 ) by GLIB_000:16;

suppose e DJoins v,w,G1 ; :: thesis: ex e9 being object st b₄ Joins f . e9,f . b₂,G2

then consider e9 being object such that
A3: e9 DJoins f . v,f . w,G2 by A1, A2;
take e9 = e9; :: thesis: e9 Joins f . v,f . w,G2
thus e9 Joins f . v,f . w,G2 by A3, GLIB_000:16; :: thesis: verum

end;

suppose e DJoins w,v,G1 ; :: thesis: ex e9 being object st b₄ Joins f . e9,f . b₂,G2

then consider e9 being object such that
A4: e9 DJoins f . w,f . v,G2 by A1, A2;
take e9 = e9; :: thesis: e9 Joins f . v,f . w,G2
thus e9 Joins f . v,f . w,G2 by A4, GLIB_000:16; :: thesis: verum

end;

end;

end;

hence f is directed PVertexMapping of G1,G2 by A1, Th1, Def2; :: thesis: verum