A function / mapping / transformation is a binary relation that is functional, i.e. a binary relation $f$ such that for any $x$, $y$, $z\in\dom f$,
\[(z,x)\in f \,\land\, (z,y)\in f \enspace\rimp\enspace x=y.\]
For any $x\in\dom f$, the value of $f$ at $x$, written as $f(x)$, is the unique $y$ such that $(x,y)\in f$. Another notation for $f(x)=y$ is
\[f : x\mapsto y.\]$f$ is onto $Y$ if $\ran f=Y$.
$f$ is from $X$ to / into $Y$, written
\[f : X\to Y,\]if $\dom f=X$ and $\ran f\subseteq Y$. In this context, $Y$ is called the codomain / set of destination of $f$.
$f$ is on $X$, if $f:X\to X$.
An $n$-ary operation on $X$ is a function $*:X^n\to X$.
If $*$ is a binary operation, we write
\[x*y \quad\text{for}\quad *(x,y).\]The set of all functions from $X$ to $Y$ is denoted by
\[Y^X \quad\text{or}\quad \fun(X,Y).\]This is a set:
\[\fun(X,Y) \subseteq \powerset(X\times Y).\]
$\varnothing$ is a function.