theorem :: GLCOLO00:13

for G being _Graph
for f being VColoring of G
for f9 being one-to-one ManySortedSet of rng f st f is proper holds
f9 * f is proper