let G1, G2 be _Graph; :: thesis: for F being directed PGraphMapping of G1,G2 st dom (F _E) = the_Edges_of G1 holds
F _V is directed PVertexMapping of G1,G2
let F be directed PGraphMapping of G1,G2; :: thesis: ( dom (F _E) = the_Edges_of G1 implies F _V is directed PVertexMapping of G1,G2 )
assume A1: dom (F _E) = the_Edges_of G1 ; :: thesis: F _V is directed PVertexMapping of G1,G2
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 ) by A1, GLIB_000:def 14;
hence F _V is directed PVertexMapping of G1,G2 by Th19; :: thesis: verum