theorem :: GLCOLO00:2

for G being _Graph
for f being VColoring of G
for v being Vertex of G
for x being object holds f +* (v .--> x) is VColoring of G ;