theorem Th26: :: GLCOLO00:26

for G, G1 being _Graph
for f being VColoring of G
for F being PGraphMapping of G1,G
for f9 being VColoring of G1 st F is total & f9 = f * (F _V) & f is proper holds
f9 is proper