theorem Th22: :: GLCOLO00:22

for G2 being _Graph
for v, e being object
for w being Vertex of G2
for G1 being addEdge of G2,v,e,w
for f1 being VColoring of G1
for f2 being VColoring of G2
for x being object st f1 = f2 +* (w .--> x) & v <> w & not x in rng f2 & f2 is proper holds
f1 is proper