\begin{definition}[Definition:Injection/Definition 6]
Let $f: S \to T$ be a mapping where $S \ne \O$.
Then $f$ is an '''injection''' {{iff}} $f$ is left cancellable:
:$\forall X: \forall g_1, g_2: X \to S: f \circ g_1 = f \circ g_2 \implies g_1 = g_2$
where $g_1$ and $g_2$ are arbitrary mappings from an arbitrary set $X$ to the domain $S$ of $f$.
\end{definition}