let G, G1 be _Graph; :: thesis: for f being VColoring of G
for F being PGraphMapping of G1,G st F is total holds
f * (F _V) is VColoring of G1
let f be VColoring of G; :: thesis: for F being PGraphMapping of G1,G st F is total holds
f * (F _V) is VColoring of G1
let F be PGraphMapping of G1,G; :: thesis: ( F is total implies f * (F _V) is VColoring of G1 )
assume F is total ; :: thesis: f * (F _V) is VColoring of G1
then dom (F _V) = the_Vertices_of G1 by GLIB_010:def 11;
hence f * (F _V) is VColoring of G1 by Th8; :: thesis: verum