theorem Th84: :: GLCOLO00:84

for G, G1 being _Graph
for g being EColoring of G
for F being PGraphMapping of G1,G st F is total holds
g * (F _E) is EColoring of G1