theorem Th9: :: GLCOLO00:9

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