let G, G1 be _Graph; :: thesis: for f being VColoring of G
for F being PGraphMapping of G1,G st dom (F _V) = the_Vertices_of G1 holds
f * (F _V) is VColoring of G1
let f be VColoring of G; :: thesis: for F being PGraphMapping of G1,G st dom (F _V) = the_Vertices_of G1 holds
f * (F _V) is VColoring of G1
let F be PGraphMapping of G1,G; :: thesis: ( dom (F _V) = the_Vertices_of G1 implies f * (F _V) is VColoring of G1 )
assume A1: dom (F _V) = the_Vertices_of G1 ; :: thesis: f * (F _V) is VColoring of G1
rng (F _V) c= the_Vertices_of G ;
then rng (F _V) c= dom f by PARTFUN1:def 2;
then dom (f * (F _V)) = dom (F _V) by RELAT_1:27;
hence f * (F _V) is VColoring of G1 by A1, PARTFUN1:def 2; :: thesis: verum