let G be _Graph; :: thesis: for f being VColoring of G
for f9 being Function st rng f c= dom f9 holds
f9 * f is VColoring of G
let f be VColoring of G; :: thesis: for f9 being Function st rng f c= dom f9 holds
f9 * f is VColoring of G
let f9 be Function; :: thesis: ( rng f c= dom f9 implies f9 * f is VColoring of G )
assume rng f c= dom f9 ; :: thesis: f9 * f is VColoring of G
then dom (f9 * f) = dom f by RELAT_1:27
.= the_Vertices_of G by PARTFUN1:def 2 ;
hence f9 * f is VColoring of G by PARTFUN1:def 2; :: thesis: verum