Is function application itself a function? Is function application itself a function? So given a function $f$ and an element $x$ we can define the function that takes $f$ and it's element $x$ to the value of $f$ at $x$?
 A: The definition of a function from $X$ to $Y$ is a subset of $X\times Y$ such that for every $x\in X$ there is a unique element of $Y$, called $f(x)$, such that the pair $(x,f(x)$ belongs in the subset of $X\times Y$ that defines the function. In simpler terms, every input has exactly one output (but different inputs may have the same output).
Let $Y^X$ denote the set of all functions from $X$ to $Y$ (as an aside, the notation is justified by setting $X=\{1,\dots,n\}$ and $Y=\{1,\dots,m\}$ ; then $Y^X$ has  $m^n$ elements).
The evaluation map, sometimes denoted by $Ev$, is then defined as a map from $Y^X \times X \to Y$, mapping the pair $(f,x)\mapsto f(x)$, where $f\in Y^X$, $x\in X$, $f(x)\in Y$. It is then a straightforward exercise on the definitions to check that the evaluation map is a function from $Y^X \times X$ to $Y$; given a pair $(f,x)$ of a function $f:X\to Y$ and an element $x\in X$ there exists a unique element $y\in Y$ (namely $f(x)$) such that $\big((f,x),y\big)\in Ev\subset \big(Y^X\times X)\times Y$. This is true precisely because $f$ is a function.
