let G be _Graph; :: thesis: ( dom H₃(G) = [:(the_Edges_of G),{0}:] & dom H₄(G) = [:(the_Edges_of G),{1}:] )
thus dom H₃(G) = [:(dom H₁(G)),(dom (id {0})):] by FUNCT_3:def 8
.= [:(the_Edges_of G),{0}:] by Lm4 ; :: thesis: dom H₄(G) = [:(the_Edges_of G),{1}:]
thus dom H₄(G) = [:(dom H₂(G)),(dom (id {1})):] by FUNCT_3:def 8
.= [:(the_Edges_of G),{1}:] by Lm4 ; :: thesis: verum