let G be _Graph; :: thesis: dom H₃(G) misses dom H₄(G)
{0} misses {1} by ZFMISC_1:11;
then [:(the_Edges_of G),{0}:] misses [:(the_Edges_of G),{1}:] by ZFMISC_1:104;
then dom H₃(G) misses [:(the_Edges_of G),{1}:] by Lm5;
hence dom H₃(G) misses dom H₄(G) by Lm5; :: thesis: verum