theorem Th82: :: GLCOLO00:82

for G2 being _Graph
for v being object
for V being Subset of (the_Vertices_of G2)
for G1 being addAdjVertexAll of G2,v,V
for g2 being EColoring of G2
for h being Function st not v in the_Vertices_of G2 & dom h = G1 .edgesBetween (V,{v}) holds
g2 +* h is EColoring of G1