# Does(n't) associativity of functional composition follow straightaway from associativity of relational composition?

One thing I find puzzling about the typical way in which associativity of functional composition is proved is that it makes explicit use of the fact that a function is a 'right-unique' relation, i.e. that nothing has two distinct values under any function. Another puzzling thing is that those who give such proofs sometimes feel the need to show that the two ways of associating $f\circ g\circ h$ have the same domain. (see the proof over at ProofWiki) The reason I'm puzzled is that I've been assuming that since a function is just a kind of relation, and since the associativity of relational composition can be proved as a simple matter of logic (see below) -- no assumption of right-uniqueness is needed, nor is the identity of domain needed in the proof -- the associativity of functional composition follows straightaway from that of relational composition. Am I not right? (And isn't such a proof better, since it makes explicit that only the existence but not the uniqueness property of functions is needed in the proof?)

\begin{aligned} xR\circ(S\circ T)y\quad&\text{iff}\quad\exists i(x(S\circ T)i \land iRy)\\ &\text{iff}\quad \exists i(\exists j (xTj \land jSi) \land iRy)\\ &\text{iff}\quad \exists i \exists j (xTj \land jSi \land iRy)\\ &\text{iff}\quad \exists j (xTj \land \exists i(jSi \land iRy))\\ &\text{iff}\quad \exists j(xTj \land j(R\circ S)y)\\ &\text{iff}\quad x((R\circ S)\circ T)y \end{aligned}

## 1 Answer

Yes, you are right.

I can imagine that some books did not want to deal with binary relations at all, and proving directly associativity of function composition is -- as you correctly observed -- basically the same as proving associativity of relation composition.