let G1, G2 be _Graph; :: thesis: for F being PGraphMapping of G1,G2 st dom (F _E) = the_Edges_of G1 holds
F _V is PVertexMapping of G1,G2
let F be PGraphMapping of G1,G2; :: thesis: ( dom (F _E) = the_Edges_of G1 implies F _V is PVertexMapping of G1,G2 )
assume A1: dom (F _E) = the_Edges_of G1 ; :: thesis: F _V is PVertexMapping of G1,G2

now :: thesis: for v, w being Vertex of G1 st v in dom (F _V) & w in dom (F _V) & v,w are_adjacent holds
ex e being object st
( e in dom (F _E) & e Joins v,w,G1 )

let v, w be Vertex of G1; :: thesis: ( v in dom (F _V) & w in dom (F _V) & v,w are_adjacent implies ex e being object st
( e in dom (F _E) & e Joins v,w,G1 ) )
assume ( v in dom (F _V) & w in dom (F _V) & v,w are_adjacent ) ; :: thesis: ex e being object st
( e in dom (F _E) & e Joins v,w,G1 )
then consider e being object such that
A2: e Joins v,w,G1 by CHORD:def 3;
take e = e; :: thesis: ( e in dom (F _E) & e Joins v,w,G1 )
thus e in dom (F _E) by A1, A2, GLIB_000:def 13; :: thesis: e Joins v,w,G1
thus e Joins v,w,G1 by A2; :: thesis: verum

end;

hence F _V is PVertexMapping of G1,G2 by Th16; :: thesis: verum