theorem :: GLIB_007:68

for G being _Graph
for v being object
for V being set
for G1, G2 being addAdjVertexAll of G,v,V ex f being Function of (the_Edges_of G1),(the_Edges_of G2) st
( f | (the_Edges_of G) = id (the_Edges_of G) & f is one-to-one & f is onto & ( for v1, e, v2 being object st e Joins v1,v2,G1 holds
f . e Joins v1,v2,G2 ) )