Maps Formed Pointwise: Constant Maps, Pairs of Values, Maps Applied to Values, and Families of Maps

This helper adopts the setting of Sets and Maps: Ordinary Notation. Let $S$, $Y$, $Z$, $W$ and $J$ be sets, with maps and their values as in Sets and Maps: Ordinary Notation (v), so that, for a map $F$ on a Cartesian product, $F(y,z)$ stands for $F((y,z))$; with the Cartesian products $Y\times Z$ and $J\times S$, the set $Y^{S}$ of maps from $S$ to $Y$, and the composite $\Phi\circ f$ of maps $f:S\to Y$ and $\Phi:Y\to W$ as in Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction (ii).

(i) For every $c\in Y$ there is exactly one map $h:S\to Y$ with $h(u)=c$ for every $u\in S$.

(ii) For maps $f:S\to Y$ and $g:S\to Z$ there is exactly one map $h:S\to Y\times Z$ with $h(u)=(f(u),g(u))$ for every $u\in S$.

(iii) For maps $f:S\to Y$, $g:S\to Z$ and $F:Y\times Z\to W$ there is exactly one map $h:S\to W$ with $h(u)=F(f(u),g(u))$ for every $u\in S$. For maps $f:S\to Y$ and $\Phi:Y\to W$, the composite $\Phi\circ f:S\to W$ is the only map $h:S\to W$ with $h(u)=\Phi(f(u))$ for every $u\in S$.

(iv) Let $G:J\times S\to Y$ be a map. For every $j\in J$ there is exactly one map $S\to Y$ whose value at every $u\in S$ is $G(j,u)$; it is written $G(j,\cdot)$. There is exactly one map $H:J\to Y^{S}$ with $H(j)(u)=G(j,u)$ for all $j\in J$ and $u\in S$, and $H(j)=G(j,\cdot)$ for every $j\in J$.