Here’s an update with things written out:
Definition:
Let ##G## be a graph. ##G## is a functional graph if and only if ##(x_1,y_1) \in G## and ##(x_1,y_2) \in G## implies ##y_1=y_2##.
Problem statement, as written:
Let ##G## be a functional graph. Prove that ##G## is injective if and only if for arbitrary graphs ##J## and ##H##: ##G \circ (H \cap J) = (G \circ H) \cap (G \circ J).##
I am concerned with the direction of the biconditional proving that ##G## is injective. I have completed a proof which seems consistent to me, but does not utilize the premise of ##G## being a functional graph anywhere in the argument (including the other direction of the biconditional). Is it simply necessary, a priori, for a graph to be a functional graph in order for it to be considered injective?
I can post my proof if needed, but here is the gist: I suppose the antecedent (assume for arbitrary graphs ##J,H## that the equality written above holds). Then I proceed via contradiction, supposing (to the contrary) ##G## is not injective. This brings into existence two elements (ordered pairs) of ##G## with unequal first elements, but equal second elements. From here, I construct ##J,H## such that I may use the equality given above to show that the unequal first elements, in fact, are equal- a contradiction.
*Nowhere do I use the fact that ##G## is a functional graph. For some reason, this isn’t sitting well. Is my conjecture above true about graphs unable to be considered injective if they are not first classified as functional?