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

One value everywhere ((i)). Let $c\in Y$. Apply Maps and Relations Given by Formulas (i) with $S$ for its $a$, $Y$ for its $b$ and the expression $t(u)=c$, the parameter $c$, which contains no defined set symbol and lies in $Y$ for every $u\in S$. It gives exactly one map $h:S\to Y$ with $h(u)=c$ for every $u\in S$.

Pairings ((ii)). Let $u\in S$. The maps $f$ and $g$ have domain $S$ by Functions, Values of a Function, and Functions from One Class to Another (iii), so $f(u)$ and $g(u)$ are defined, and $f(u)\in Y$ and $g(u)\in Z$ by Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol (ii); hence $(f(u),g(u))\in Y\times Z$ by Membership in a Cartesian Product, and the Cartesian Product of Two Sets Is a Set (i). The expression $(f(u),g(u))$ is built from the variable $u$, the parameters $f$ and $g$, and the defined set symbols value of a map and ordered pair (the values $f(u)$ and $g(u)$ entering predicative formulas as in Predicative Substitution of Values of Functions and Binary Operations, and Predicative Formulas for Negatives, Differences, Absolute Values, Distances, Reciprocals and Quotients in an Ordered Field (i)); as just shown, it is used properly and lies in $Y\times Z$ for every $u\in S$. So Maps and Relations Given by Formulas (i), with $S$ for its $a$ and $Y\times Z$ for its $b$, a set by Membership in a Cartesian Product, and the Cartesian Product of Two Sets Is a Set (ii), gives exactly one map $h:S\to Y\times Z$ with $h(u)=(f(u),g(u))$ for every $u\in S$.

Maps applied to values ((iii)). Let $f:S\to Y$, $g:S\to Z$ and $F:Y\times Z\to W$ be maps, and let $p:S\to Y\times Z$ be the map of (ii), with $p(u)=(f(u),g(u))$ for $u\in S$. By Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction (ii), $F\circ p$ is a map $S\to W$ with $(F\circ p)(u)=F(p(u))=F(f(u),g(u))$ for every $u\in S$; so a map $h$ as required exists. If $h:S\to W$ is a map with $h(u)=F(f(u),g(u))$ for every $u\in S$, then $h(u)=(F\circ p)(u)$ for every $u\in S$, so $h=F\circ p$ by Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol (iv); so it is unique.

Now let $f:S\to Y$ and $\Phi:Y\to W$ be maps. By Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction (ii), $\Phi\circ f$ is a map $S\to W$ with $(\Phi\circ f)(u)=\Phi(f(u))$ for every $u\in S$; and a map $h:S\to W$ with $h(u)=\Phi(f(u))$ for every $u\in S$ agrees with $\Phi\circ f$ at every point of $S$, so $h=\Phi\circ f$ by Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol (iv). So there is exactly one map $h:S\to W$ with $h(u)=\Phi(f(u))$ for every $u\in S$, namely $h=\Phi\circ f$.

Families ((iv)). Let $G:J\times S\to Y$ be a map and let $j\in J$. For $u\in S$, $(j,u)\in J\times S$ by Membership in a Cartesian Product, and the Cartesian Product of Two Sets Is a Set (i), so $G(j,u)=G((j,u))$ is defined and lies in $Y$ by Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol (ii). The expression $G((j,u))$ is built from the variable $u$, the parameters $G$ and $j$, and the defined set symbols ordered pair and value of a map (the value $G((j,u))$ entering predicative formulas as in Predicative Substitution of Values of Functions and Binary Operations, and Predicative Formulas for Negatives, Differences, Absolute Values, Distances, Reciprocals and Quotients in an Ordered Field (i)), and it is used properly and lies in $Y$ for every $u\in S$. So Maps and Relations Given by Formulas (i), with $S$ for its $a$ and $Y$ for its $b$, gives exactly one map $S\to Y$ whose value at every $u\in S$ is $G(j,u)$.

By Projection, Evaluation and Currying Maps (iii), with $J$ for its $X$, $S$ for its $I$, $Y$ for its $Y$ and $G$ for its $g$, 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$. Let $j\in J$. Then $H(j)\in Y^{S}$ by Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol (ii), so $H(j)$ is a map $S\to Y$ by The Elements of the Class of Functions from a Set to a Set, and This Class Is a Set (i), and its value at every $u\in S$ is $G(j,u)$. By the uniqueness shown in the previous paragraph, $H(j)=G(j,\cdot)$.