theorem Th157: :: GLIB_010:157

for G3, G4 being _Graph
for v3 being Vertex of G3
for v4 being Vertex of G4
for e1, e2, v1, v2 being object
for G1 being addAdjVertex of G3,v3,e1,v1
for G2 being addAdjVertex of G4,v4,e2,v2
for F0 being PGraphMapping of G3,G4 st not e1 in the_Edges_of G3 & not e2 in the_Edges_of G4 & not v1 in the_Vertices_of G3 & not v2 in the_Vertices_of G4 & v3 in dom (F0 _V) & (F0 _V) . v3 = v4 holds
ex F being PGraphMapping of G1,G2 st
( F = [((F0 _V) +* (v1 .--> v2)),((F0 _E) +* (e1 .--> e2))] & ( F0 is total implies F is total ) & ( F0 is onto implies F is onto ) & ( F0 is one-to-one implies F is one-to-one ) & ( F0 is directed implies F is directed ) )