theorem :: GLCOLO00:88

for G being _Graph
for g being EColoring of G
for g9 being one-to-one ManySortedSet of rng g st g is proper holds
g9 * g is proper by Th87;