theorem Th87: :: GLCOLO00:87

for G being _Graph
for g being EColoring of G
for g9 being one-to-one Function
for g2 being EColoring of G st g2 = g9 * g & g is proper holds
g2 is proper