Is the following result true? (I hope so because I've given a proof...)
Many thanks!
Claim. Let $S$ be a (non-empty) set and let $\sim$ be an equivalence relation on $S.$
The natural map $S\to S/\sim$ induces an isomorphism $$F(S)/\langle\{s-s' \, : \, s,s' \in S \;\text{ with }\; s\sim s'\}\rangle \to F(S/\sim)$$ where $F$ is the "free abelian group" functor.
Proof. The quotient map $S\to S/\sim$ induces a surjective group hom $$\Phi:F(S) \to F(S/\sim)$$ $$\sum_{s \in S}a_s s \longmapsto \sum_{s \in S}a_s[s]$$ where the $a_s$ are integers almost all of which are zero.
It is clear that any element of $F(S)$ of the form $s-s'$ where $s\sim s'$ is in $\ker \Phi$.
Conversely, if $\sum_{s \in S} a_s s$ is in the kernel, then, for each $[s] \in S/\sim,$ one has $$\sum_{t \in [s]}a_t=0.$$ Fix some $[s] \in S/\sim.$ If there exists $t \in [s]$ such that $a_t\neq0,$ then we have $$a_t=-\sum_{u \in [s] \\ \,u\neq t}a_u$$ and so we can write $$\sum_{v \in [s]} a_v v = \sum_{u \in [s] \\ \,u\neq t}a_u(u-t)$$ and so the result follows.
Yes, the statement is true, and your proof works (up to the missing sign in $a_t = -\sum_{u \in [s], u \neq t} a_u$).
Another way to prove this statement is to construct a pair of inverse homomorphisms $$ \varphi \colon F(S)/N \to F(S/{\sim}) \qquad\text{and}\qquad \psi \colon F(S/{\sim}) \to F(S)/N $$ (where $N = \langle s - s' \mid s, s' \in S, s \sim s' \rangle$) by using the universal properties of the various objects involved:
You have already mentioned that the canonical projection $S \to S/{\sim}$, $s \mapsto [s]$ induces a group homomorphism $$ \Phi \colon F(S) \to F(S/{\sim}), \quad \sum_{s \in S} a_s s \mapsto \sum_{s \in S} a_s [s], $$ and that $N \subseteq \ker \Phi$. It follows that $\Phi$ induces a well-defined homomorphism $$ \varphi \colon F(S)/N \to F(S/{\sim}), \quad \left[ \sum_{s \in S} a_s s \right] \mapsto \sum_{s \in S} a_s [s]. $$
To construct $\psi$ we start with the canonical inclusion $S \to F(S)$, $s \mapsto s$. Then the composition $$ S \to F(S) \to F(S)/N, \quad s \mapsto [s] $$ maps $s, s' \in S$ with $s \sim s'$ onto the same element, and thus induces a well-defined map $$ S/{\sim} \to F(S)/N, \quad [s] \mapsto [s]. $$ By the universal property of the free group, this map induces a well-defined homomorphism $$ \psi \colon F(S/{\sim}) \to F(S)/N, \quad \sum_{[s] \in S/{\sim}} b_{[s]} [s] \mapsto \sum_{[s] \in S/{\sim}} b_{[s]} [s] = \left[ \sum_{[s] \in S/{\sim}} b_{[s]} s \right]. $$
Checking that $\varphi$ and $\psi$ are inverse to each other can be done on generators: The group $F(S)$ is generated by the elements $s \in S$, so $F(S)/N$ is generated by the elements $[s]$ with $s \in S$; the group $F(S/{\sim})$ is generated by th elements $[s]$ with $[s] \in S/{\sim}$, i.e. by the elements $[s]$ with $s \in S$. For every $s \in S$ we have that $$ \varphi(\psi([s])) = \varphi([s]) = [s], $$ and similarly $$ \psi(\varphi([s])) = \psi([s]) = [s]. $$ So we have that $\varphi \circ \psi = \operatorname{id}$ and $\psi \circ \varphi = \operatorname{id}$, showing that $\varphi$ is an isomorphism with $\varphi^{-1} = \psi$.