rng g = dom g9 by PARTFUN1:def 2;
hence g * g9 is EColoring of G by Th77; :: thesis: verum