theorem Th77: :: GLCOLO00:77

for G being _Graph
for g being EColoring of G
for g9 being Function st rng g c= dom g9 holds
g9 * g is EColoring of G