theorem Th1: :: GLCOLO00:1

for G being _Graph
for f being VColoring of G
for f9 being Function st rng f c= dom f9 holds
f9 * f is VColoring of G