theorem Th12: :: GLCOLO00:12

for G being _Graph
for f being VColoring of G
for f9 being one-to-one Function
for f2 being VColoring of G st f2 = f9 * f & f is proper & rng f c= dom f9 holds
f2 is proper