Abelianization of Free Group is Free Abelian Group

Theorem

Let $X$ be a set.

Let $\struct {F_X, \iota}$ be a free group on $X$.

Let $F_X^{\mathrm {ab} }$ be its abelianization.

Let $\pi : F_X \to F_X^{\mathrm {ab} }$ be the quotient group epimorphism.

Then $\struct {F_X^{\mathrm {ab} }, \pi \circ \iota}$ is a free abelian group on $X$.