Sections of Subsets and Functions on a Product

In the setting of Routine Facts Used Without Citation: Arithmetic, Maps, Predicativity and Indices, let $X$ and $Y$ be sets and let $X\times Y$ be their Cartesian product.

(i) Sections of sets. Let $E\subseteq X\times Y$. For $x\in X$, the section of $E$ at $x$ is the subset $E_{x}$ of $Y$, and for $y\in Y$, the section of $E$ at $y$ is the subset $E^{y}$ of $X$, given by

$$E_{x}=\{y'\in Y:(x,y')\in E\},\qquad E^{y}=\{x'\in X:(x',y)\in E\}.$$

(ii) Sections of functions. Let $Z$ be a set and $f:X\times Y\to Z$ a function. For $x\in X$, the section of $f$ at $x$ is the function $f_{x}:Y\to Z$, and for $y\in Y$, the section of $f$ at $y$ is the function $f^{y}:X\to Z$, given by

$$f_{x}(y')=f(x,y')\quad(y'\in Y),\qquad f^{y}(x')=f(x',y)\quad(x'\in X)$$

(these functions exist and are unique by Sets and Maps: Ordinary Notation (v)).