let f be VColoring of G; :: thesis: not f is empty
dom f = the_Vertices_of G by PARTFUN1:def 2;
hence not f is empty ; :: thesis: verum