Projection, Evaluation and Currying Maps

This lemma adopts the setting of Sets and Maps: Ordinary Notation. Let $X$, $Y$ and $I$ be sets, with the Cartesian products $X\times Y$ and $X\times I$, the set $Y^{I}$ of maps from $I$ to $Y$, the components $p_{1}$ and $p_{2}$ of an ordered pair $p$, and maps and their values as in Sets and Maps: Ordinary Notation §maps, so that $g(x,y)$ stands for $g((x,y))$.

¶ There is exactly one map $\pi_{1}:X\times Y\to X$ with $\pi_{1}(x,y)=x$ for all $x\in X$ and $y\in Y$, and exactly one map $\pi_{2}:X\times Y\to Y$ with $\pi_{2}(x,y)=y$ for all $x\in X$ and $y\in Y$. For every $p\in X\times Y$, $\pi_{1}(p)=p_{1}$ and $\pi_{2}(p)=p_{2}$.

¶ There is exactly one map $\mathrm{ev}:Y^{I}\times I\to Y$ with $\mathrm{ev}(f,i)=f(i)$ for all $f\in Y^{I}$ and $i\in I$.

¶ For every map $g:X\times I\to Y$ there is exactly one map $h:X\to Y^{I}$ with $h(x)(i)=g(x,i)$ for all $x\in X$ and $i\in I$.