DEF-F. Function.
A function / mapping / transformation $f$ is a binary relation that is functional, i.e.
\[\forall x,y,z\in\operatorname{dom}f :\enspace (z,x)\in f\land(z,y)\in f \enspace\Rightarrow\enspace x=y.\]For any $x\in\operatorname{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 a function on $X$ if $X=\operatorname{dom}f$. $f$ is a function onto $Y$, if $\operatorname{ran}f=Y$. $f$ is a function from $X$ to / into $Y$, written
\[f : X\to Y,\]if $\operatorname{dom}f=X$ and $\operatorname{ran}f\subseteq Y$. In this context, $Y$ is called the codomain or set of destination of $f$.
REM-F-COD.
Notice that the codomain of a function is not an intrinsic property. When we talk about a function $f:X\to Y$, it is as if we were talking about the structure $(f,Y)$.
PROP-F-EMP.
$\varnothing$ is a function.