let G be _Graph; :: thesis: ( dom H₁(G) = the_Edges_of G & dom H₂(G) = the_Edges_of G )
thus dom H₁(G) = (dom (the_Source_of G)) /\ (dom (id (the_Edges_of G))) by FUNCT_3:def 7
.= (the_Edges_of G) /\ (the_Edges_of G) by FUNCT_2:def 1
.= the_Edges_of G ; :: thesis: dom H₂(G) = the_Edges_of G
thus dom H₂(G) = (dom (the_Target_of G)) /\ (dom (id (the_Edges_of G))) by FUNCT_3:def 7
.= (the_Edges_of G) /\ (the_Edges_of G) by FUNCT_2:def 1
.= the_Edges_of G ; :: thesis: verum