Showing that the free group of a disjoint union is isomorphic to the free product of the corresponding free groups P. Aluffi's "Algebra: Chapter $\it 0$", exercise II.$5.8$.

Still more generally, prove that $F(A\amalg B)=F(A)*F(B)$ and that $F^{ab}(A\amalg B)=F^{ab}(A)\oplus F^{ab}(B)$ for all sets $A,B$. $($That is, the constructions $F,F^{ab}$ 'preserve coproducts'.$)$

Here $F(A)$ is the free groups on the set $A$, $A\amalg B$ is the disjoint union of $A$ and $B$, and $G*H$ is the free product of $G$ and $H$ (i.e. the coproduct in $\sf Grp$). All of those are characterized by their usual universal properties which will be used extensively for the proof.$^*$
Proof. We will show that $F(A\amalg B)$ satisfies the universal property of $F(A)*F(B)$. For startes, we will construct the (canonical) inclusion homomorphisms. Thus, consider the following diagrams

Here $\iota_A,\iota_B,\iota$ are the inclusion of $A,B,A\amalg B$ into their respective free groups. The (unique) group homomorphisms $I_A,I_B$ are induced by considering the compositions $\iota\circ i_B$ and $\iota\circ i_B$ and the universal properties of $F(A)$ and $F(B)$. Hence they are such that
$$I_A\circ\iota_A=\iota\circ i_A,~~~I_B\circ\iota_B=\iota\circ i_B$$
Now, suppose we are given group homomorphisms $g_A\colon F(A)\to G,\,g_B\colon F(B)\to G$ to some arbitrary group $G$. We can consider them in particular as set-functions and precomposing with $\iota_A$ and $\iota_B$, respectively, gives us the following

The unique map $g$ is given by the universal property of $A\amalg B$ and such that
$$g\circ i_A=g_A\circ\iota_A,~~~g\circ i_B=g_B\circ\iota_B$$
Finally, $\overline{g}$ induces a unique map $\overline{f}$ such that

by the universal property of $F(A\amalg B)$ and so $\overline{g}\circ\iota=g$. Composing gives us uniquely determined group homomorphisms $\overline{g}\circ I_A\colon F(A)\to G$ and $\overline{g}\circ I_B\colon F(B)\to G$ factoring through $F(A\amalg B)$. It remains to show the following
$$\overline{g}\circ I_A=g_A,~~~\overline{g}\circ I_B=g_B$$
But using the given commutativity relations we see that
$$(\overline{g}\circ I_A)\circ\iota_A=\overline{g}\circ(I_A\circ\iota_A)=\overline{g}\circ(\iota\circ i_A)=(\overline{g}\circ\iota)\circ i_A=g\circ i_A=g_A\circ\iota_A$$
and hence both triangles in the following diagram commute

The right triangle corresponds to the fact the by $g_A\circ\iota_A$ universally induced map is $g_A$ itself. But from the left triangles we see that $\overline{f}\circ I_A$ makes the corresponding diagram commute as well and hence $\overline{f}\circ I_A=g_A$ by the uniquesness of the induced map. The same argument, with all $A$s replaced by $B$s, yields $\overline{f}\circ I_B=g_B$. Thus, we conclude that $F(A\amalg B)$ satisfies the universal property of $F(A)*F(B)$ as every pair of group homomorphisms $g_A\colon F(A)\to G,\,g_B\colon F(B)\to G$ factors uniquely through $F(A\amalg B)$ using $I_A,I_B$ and $\overline{g}$. Hence, $F(A\amalg B)\cong F(A)*F(B)$.
The argument is precisely the same for $F^{ab}$ where we note that $G*H=G\oplus H=G\times H$ for abelian groups.   $\square$

Is the given proof correct; if so, can it be (substantially) improved? If not, where did I went wrong? I am not sure how to show actual equality instead 'mere' isomorphy (which is enough for me, to be honest) and the last part, i.e. showing that $\overline{g}\circ I_A=g_A$, is a little bit sketchy to me, even though I am quite sure the argument works.

Thanks in advance!

$^*$ I know that this preservation essentially boils down to 'left adjoints presever colimits' as the (binary) coproduct is a simple colimit and the free functor $F\colon\sf{Set}\to\sf{Grp}$ is left adjoint to the forgetful functor $\sf{Grp}\to\sf{Set}$. However, I would like to not dabble to deep into category theoretic terrain if it does not make the proof easier/more understandable. So the given proof is more or less from scratch.
 A: So, let me argue for proving the other universal property; that is, showing that $F(A)*F(B)$ has the universal property of $F(A\amalg B)$.
Let $u_A\colon A\to F(A)$ and $u_B\colon B\to F(B)$ be the canonical maps from the set to the corresponding free group. Let $\iota_A\colon F(A)\to F(A)*F(B)$ and $\iota_B\colon F(B)\to F(A)*F(B)$ be the canonical inclusions into the free product. And let $j_A\colon A\to A\amalg B$ and $j_B\colon B\to A\amalg B$ be the set-theoretic inclusions into the disjoint union/set-theoretic coproduct.
We want to show that there is a map $u_{A\amalg B}\colon A\amalg B\to F(A)*F(B)$ such that for every group $G$ and every set-theoretic map $f\colon A\amalg B\to G$, there exists a unique group homomorphism $\mathscr{F}\colon F(A)*F(B)\to G$ such that $\mathscr{F}\circ u_{A\amalg B}=f$.
So, first, the maps $\iota_A\circ u_A\colon A\to F(A)*F(B)$ and $\iota_B\circ u_B\colon B\to F(A)*F(B)$ yield a unique map $u_{A\amalg B}\to F(A)*F(B)$ such that $u_{A\amalg B}\circ j_A=\iota_A\circ u_A$ and $u_{A\amalg B}\circ j_B=\iota_B\circ u_B$.
Now let $f\colon A\amalg B\to G$. The map $f\circ j_A\colon A\to G$ induces a morphism $F_A\colon F(A)\to G$ with $F_A\circ u_A=f\circ j_A$; similarly, we have a morphism $F_B\colon F(B)\to G$ with $F_B\circ u_B=f\circ j_B$. And the maps $F_A$ and $F_B$ induce a morphism $\mathscr{F}\colon F(A)*F(B)\to G$ with $\mathscr{F}\circ \iota_A=F_A$ and $\mathscr{F}\circ \iota_B=F_B$. We want to show that this $\mathscr{F}$ satisfies $\mathscr{F}\circ u_{A\amalg B}=f$, and that it is the unique map with this property.
The universal property of $A\amalg B$ tells us that $f$ is the unique map $g\colon A\amalg B\to G$ such that $g\circ j_A=f\circ j_A$ and $g\circ j_B=f\circ j_B$. So if we can prove that $\mathscr{F}\circ u_{A\amalg B}$ also has this property, then we will have the equality with $f$.
Now,
$$\begin{align*}
(\mathscr{F}\circ u_{A\amalg B})\circ j_A&=\mathscr{F}\circ (u_{A\amalg B}\circ j_A)\\
&= \mathscr{F}\circ (i_A\circ u_A)\\
&=(\mathscr{F}\circ i_A)\circ u_A\\
&= F_A\circ u_A\\
&= f\circ j_A;\\
(\mathscr{F}\circ u_{A\amalg B})\circ j_B &= \mathscr{F}\circ (u_{A\amalg B}\circ j_B)\\
&= \mathscr{F}\circ (i_B\circ u_B)\\
&= (\mathscr{F}\circ i_B)\circ u_B\\
&= F_B\circ u_B\\
&= f\circ j_B.
\end{align*}$$
Therefore, $\mathscr{F}\circ u_{A\amalg B}=f$, as desired.
As for uniqueness, let $\mathscr{G}\colon F(A)*F(B)\to G$ be such that $\mathscr{G}\circ u_{A\amalg B} = f$. We want to show that $\mathscr{G}=\mathscr{F}$. Since $\mathscr{F}$ is the unique map such that $\mathscr{F}\circ i_A=F_A$ and $\mathscr{F}\circ i_B=F_B$, it is enough to show that $\mathscr{G}$ has this property as well.
To show that $\mathscr{G}\circ i_A=F_A$, it is enough to show that it has the universal property of $F_A$, namely, that $(\mathscr{G}\circ i_A)\circ u_A=f\circ j_A$. And, indeed,
$$\begin{align*}
(\mathscr{G}\circ i_A)\circ u_A &= \mathscr{G}\circ (i_A\circ u_A)\\
&= \mathscr{G}\circ(u_{A\amalg B}\circ j_A)\\
&= (\mathscr{G}\circ u_{A\amalg B})\circ j_A\\
&= f\circ j_A,
\end{align*}$$
as desired. Thus, $\mathscr{G}\circ i_A=F_A$, as needed. Symmetrically, $\mathscr{G}\circ i_B=F_B$. This proves that $\mathscr{G}=\mathscr{F}$, giving uniqueness, and we are done.
