for G2 being _Graph
for v being object
for V being set
for G1 being addAdjVertexAll of G2,v,V
for E being set st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 & the_Edges_of G1 = (the_Edges_of G2) \/ E & E misses the_Edges_of G2 holds
ex f, g being Function of E,(V \/ {v}) st
( the_Source_of G1 = (the_Source_of G2) +* f & the_Target_of G1 = (the_Target_of G2) +* g & ( for e being object st e in E holds
( e DJoins f . e,g . e,G1 & ( f . e = v implies g . e <> v ) & ( g . e <> v implies f . e = v ) ) ) )