\begin{definition}[Definition:Class Mapping]
Let $S$ and $T$ be classes.
A '''class mapping $f$ from $S$ to $T$''', denoted $f: S \to T$, is a class relation $f = \RR \subseteq S \times T$ such that:
:$\forall x \in S: \forall y_1, y_2 \in T: \tuple {x, y_1} \in f \land \tuple {x, y_2} \in f \implies y_1 = y_2$
and
:$\forall x \in S: \exists y \in T: \tuple {x, y} \in f$
Usually, $\tuple {x, y} \in f$ is instead written as:
:$\map f x = y$
This is the preferred notation.
\end{definition}