theorem Th17: :: GLCOLO00:17

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