theorem Th83: :: GLCOLO00:83

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