theorem Th8: :: GLCOLO00:8

for G, G1 being _Graph
for f being VColoring of G
for F being PGraphMapping of G1,G st dom (F _V) = the_Vertices_of G1 holds
f * (F _V) is VColoring of G1