let G1, G2 be _Graph; :: thesis: for F being directed PGraphMapping of G1,G2 st ( for v, w being object st v in dom (F _V) & w in dom (F _V) & ex e being object st e DJoins v,w,G1 holds
ex e being object st
( e in dom (F _E) & e DJoins v,w,G1 ) ) holds
F _V is directed PVertexMapping of G1,G2
let F be directed PGraphMapping of G1,G2; :: thesis: ( ( for v, w being object st v in dom (F _V) & w in dom (F _V) & ex e being object st e DJoins v,w,G1 holds
ex e being object st
( e in dom (F _E) & e DJoins v,w,G1 ) ) implies F _V is directed PVertexMapping of G1,G2 )
assume A1: for v, w being object st v in dom (F _V) & w in dom (F _V) & ex e being object st e DJoins v,w,G1 holds
ex e being object st
( e in dom (F _E) & e DJoins v,w,G1 ) ; :: thesis: F _V is directed PVertexMapping of G1,G2

now :: thesis: for v, w, e being object st v in dom (F _V) & w in dom (F _V) & e Joins v,w,G1 holds
ex e9 being object st e9 Joins (F _V) . v,(F _V) . w,G2

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

then consider e0 being object such that
A3: ( e0 in dom (F _E) & e0 DJoins v,w,G1 ) by A1, A2;
reconsider e9 = (F _E) . e0 as object ;
take e9 = e9; :: thesis: e9 Joins (F _V) . v,(F _V) . w,G2
e0 Joins v,w,G1 by A3, GLIB_000:16;
hence e9 Joins (F _V) . v,(F _V) . w,G2 by A2, A3, GLIB_010:4; :: thesis: verum

end;

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

then consider e0 being object such that
A4: ( e0 in dom (F _E) & e0 DJoins w,v,G1 ) by A1, A2;
reconsider e9 = (F _E) . e0 as object ;
take e9 = e9; :: thesis: e9 Joins (F _V) . v,(F _V) . w,G2
e0 Joins v,w,G1 by A4, GLIB_000:16;
hence e9 Joins (F _V) . v,(F _V) . w,G2 by A2, A4, GLIB_010:4; :: thesis: verum

end;

end;

end;

then A5: F _V is PVertexMapping of G1,G2 by Th1;

now :: thesis: for v, w, e being object st v in dom (F _V) & w in dom (F _V) & e DJoins v,w,G1 holds
ex e9 being object st e9 DJoins (F _V) . v,(F _V) . w,G2

let v, w, e be object ; :: thesis: ( v in dom (F _V) & w in dom (F _V) & e DJoins v,w,G1 implies ex e9 being object st e9 DJoins (F _V) . v,(F _V) . w,G2 )
assume A6: ( v in dom (F _V) & w in dom (F _V) & e DJoins v,w,G1 ) ; :: thesis: ex e9 being object st e9 DJoins (F _V) . v,(F _V) . w,G2
then consider e0 being object such that
A7: ( e0 in dom (F _E) & e0 DJoins v,w,G1 ) by A1;
reconsider e9 = (F _E) . e0 as object ;
take e9 = e9; :: thesis: e9 DJoins (F _V) . v,(F _V) . w,G2
thus e9 DJoins (F _V) . v,(F _V) . w,G2 by A6, A7, GLIB_010:def 14; :: thesis: verum

end;

hence F _V is directed PVertexMapping of G1,G2 by A5, Def2; :: thesis: verum