rng f = dom f9 by PARTFUN1:def 2;
hence f * f9 is VColoring of G by Th1; :: thesis: verum