Universal property of a free group (source code)

= Universal property of a free group

For every function $f:S\to G$ from a set into a <group>, there is a unique <group homomorphism> $\bar f:F(S)\to G$ whose restriction to $S$ is $f$.