theorem Th162: :: GLIB_010:162

for G3, G4 being _Graph
for v1, v2 being object
for V1, V2 being set
for G1 being addAdjVertexAll of G3,v1,V1
for G2 being addAdjVertexAll of G4,v2,V2
for F0 being PGraphMapping of G3,G4 st V1 c= the_Vertices_of G3 & V2 c= the_Vertices_of G4 & not v1 in the_Vertices_of G3 & not v2 in the_Vertices_of G4 & (F0 _V) | V1 is one-to-one & dom ((F0 _V) | V1) = V1 & rng ((F0 _V) | V1) = V2 holds
ex F being PGraphMapping of G1,G2 st
( F _V = (F0 _V) +* (v1 .--> v2) & (F _E) | (dom (F0 _E)) = F0 _E & ( 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 weak_SG-embedding implies F is weak_SG-embedding ) & ( F0 is isomorphism implies F is isomorphism ) )