let G be _Graph; :: thesis: H₅(G) is one-to-one
rng H₃(G) misses rng H₄(G) by Lm7;
hence H₅(G) is one-to-one by FUNCT_4:92; :: thesis: verum