Proof of Component Maps of a Map into $\mathbb{R}^{q}$, Entry Maps of a Map into Matrices, and Maps Assembled from Them

The sets involved. $[p]$ and $[q]$ are sets by Tuples in a Set: the Set of n-Tuples and Their Components (i), and $[p]\times[q]$ is a set by Membership in a Cartesian Product, and the Cartesian Product of Two Sets Is a Set (ii). By Euclidean Space $\mathbb{R}^n$: n-Tuples of Real Numbers with Their Componentwise Operations (i), $\mathbb{R}^{q}$ is the set $\mathbb{R}^{[q]}$ of maps $[q]\to\mathbb{R}$, and for $z\in\mathbb{R}^{q}$ and $k\in[q]$, $z_{k}=z(k)$ by Euclidean Space $\mathbb{R}^n$: n-Tuples of Real Numbers with Their Componentwise Operations (ii). By Real Matrices: the Set of Real m x n Matrices with Their Entrywise Operations (i), $\mathcal{M}_{p\times q}(\mathbb{R})$ is the set $\mathbb{R}^{[p]\times[q]}$ of maps $[p]\times[q]\to\mathbb{R}$, and for $B\in\mathcal{M}_{p\times q}(\mathbb{R})$, $B_{ij}=B(i,j)$ by Real Matrices: the Set of Real m x n Matrices with Their Entrywise Operations (ii). For every set $D$, $\mathbb{R}^{D}$ is a set by The Elements of the Class of Functions from a Set to a Set, and This Class Is a Set (ii), and its elements are exactly the maps $D\to\mathbb{R}$, by The Elements of the Class of Functions from a Set to a Set, and This Class Is a Set (i).

Transposition. Let $D$ and $E$ be sets and $F:E\to\mathbb{R}^{D}$ a map. We show: there is exactly one map $G:D\to\mathbb{R}^{E}$ with $G(a)(b)=F(b)(a)$ for all $a\in D$ and $b\in E$. By Projection, Evaluation and Currying Maps (ii), with $\mathbb{R}$ for $Y$ and $D$ for $I$, there is a map $\mathrm{ev}:\mathbb{R}^{D}\times D\to\mathbb{R}$ with $\mathrm{ev}(f,a)=f(a)$ for all $f\in\mathbb{R}^{D}$ and $a\in D$. Let $a\in D$ and $b\in E$. Then $F(b)\in\mathbb{R}^{D}$ by Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol (ii), so $(F(b),a)\in\mathbb{R}^{D}\times D$ by Membership in a Cartesian Product, and the Cartesian Product of Two Sets Is a Set (i), and the expression $\mathrm{ev}(F(b),a)$, built from values of maps at elements of their domains, is used properly, with $\mathrm{ev}(F(b),a)=F(b)(a)\in\mathbb{R}$. Hence there is exactly one map $g:D\times E\to\mathbb{R}$ with $g(a,b)=\mathrm{ev}(F(b),a)=F(b)(a)$ for all $a\in D$ and $b\in E$ (Maps and Relations Given by Formulas (ii), with $\mathbb{R}$, $D$ and $E$ for $b$, $c$ and $d$). By Projection, Evaluation and Currying Maps (iii), with $D$, $E$ and $\mathbb{R}$ for $X$, $I$ and $Y$, there is exactly one map $G:D\to\mathbb{R}^{E}$ with $G(a)(b)=g(a,b)$ for all $a\in D$ and $b\in E$, that is, with $G(a)(b)=F(b)(a)$. A map $G':D\to\mathbb{R}^{E}$ with $G'(a)(b)=F(b)(a)$ for all $a\in D$ and $b\in E$ satisfies $G'(a)(b)=g(a,b)$ for all of them, so $G'=G$ by the uniqueness in Projection, Evaluation and Currying Maps (iii).

Proof of (i). Apply the transposition to $D=[q]$, $E=S$ and $F=x$, which is a map $S\to\mathbb{R}^{[q]}$: there is a map $G:[q]\to\mathbb{R}^{S}$ with $G(k)(u)=x(u)(k)=x(u)_{k}$ for all $k\in[q]$ and $u\in S$. For $k\in[q]$, $G(k)\in\mathbb{R}^{S}$ by Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol (ii), so, by The Elements of the Class of Functions from a Set to a Set, and This Class Is a Set (i), $x_{k}=G(k)$ is a map $S\to\mathbb{R}$ with $x_{k}(u)=x(u)_{k}$ for every $u\in S$. If $y:S\to\mathbb{R}$ is a map with $y(u)=x(u)_{k}$ for every $u\in S$, then $y$ and $x_{k}$ are functions with the same domain $S$ (Functions, Values of a Function, and Functions from One Class to Another (iii)) and the same value at every $u\in S$, so $y=x_{k}$ by Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction (i). So $x_{k}$ is the only such map. The map $G$ has value $x_{k}$ at every $k\in[q]$; any map $H:[q]\to\mathbb{R}^{S}$ with $H(k)=x_{k}=G(k)$ for every $k\in[q]$ has the domain and the values of $G$, so $H=G$ by Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction (i).

Proof of (ii). Apply the transposition to $D=[p]\times[q]$, $E=S$ and $F=A$, which is a map $S\to\mathbb{R}^{[p]\times[q]}$: there is a map $G:[p]\times[q]\to\mathbb{R}^{S}$ with $G(i,j)(u)=A(u)(i,j)=A(u)_{ij}$ for all $i\in[p]$, $j\in[q]$ and $u\in S$, where $(i,j)\in[p]\times[q]$ by Membership in a Cartesian Product, and the Cartesian Product of Two Sets Is a Set (i). For such $i$ and $j$, $A_{ij}=G(i,j)$ lies in $\mathbb{R}^{S}$ by Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol (ii), so it is, by The Elements of the Class of Functions from a Set to a Set, and This Class Is a Set (i), a map $S\to\mathbb{R}$ with $A_{ij}(u)=A(u)_{ij}$ for every $u\in S$, and every map $S\to\mathbb{R}$ with these values equals it by Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction (i), as in the proof of (i). The map $G$ has value $A_{ij}$ at every $(i,j)\in[p]\times[q]$. Every element of $[p]\times[q]$ is an ordered pair $(i,j)$ with $i\in[p]$ and $j\in[q]$, by The Cartesian Product of Two Classes (i) and Membership in a Cartesian Product, and the Cartesian Product of Two Sets Is a Set (i); so any map $H:[p]\times[q]\to\mathbb{R}^{S}$ with $H(i,j)=A_{ij}$ for all such $i$ and $j$ has the domain and the values of $G$, and $H=G$ by Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction (i).

Proof of (iii). Let $y:[q]\to\mathbb{R}^{S}$, $k\mapsto y_{k}$. Apply the transposition to $D=S$, $E=[q]$ and $F=y$: there is exactly one map $x:S\to\mathbb{R}^{[q]}=\mathbb{R}^{q}$ with $x(u)(k)=y(k)(u)$ for all $u\in S$ and $k\in[q]$. As $x(u)(k)=x(u)_{k}$ and $y(k)(u)=y_{k}(u)$, these are exactly the maps $x:S\to\mathbb{R}^{q}$ with $x(u)_{k}=y_{k}(u)$ for all $u\in S$ and $k\in[q]$, so there is exactly one such map. For $k\in[q]$, $y_{k}\in\mathbb{R}^{S}$ by Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol (ii), so, by The Elements of the Class of Functions from a Set to a Set, and This Class Is a Set (i), $y_{k}$ is a map $S\to\mathbb{R}$, with $y_{k}(u)=x(u)_{k}$ for every $u\in S$; so $y_{k}=x_{k}$, by the uniqueness in (i).

Proof of (iv). Let $b:[p]\times[q]\to\mathbb{R}^{S}$, $(i,j)\mapsto b_{ij}$. Apply the transposition to $D=S$, $E=[p]\times[q]$ and $F=b$: there is exactly one map $A:S\to\mathbb{R}^{[p]\times[q]}=\mathcal{M}_{p\times q}(\mathbb{R})$ with $A(u)(w)=b(w)(u)$ for all $u\in S$ and $w\in[p]\times[q]$. As every $w\in[p]\times[q]$ is a pair $(i,j)$ with $i\in[p]$ and $j\in[q]$, and every such pair lies in $[p]\times[q]$ (The Cartesian Product of Two Classes (i) and Membership in a Cartesian Product, and the Cartesian Product of Two Sets Is a Set (i)), and as $A(u)(i,j)=A(u)_{ij}$ and $b(i,j)(u)=b_{ij}(u)$, a map $A':S\to\mathcal{M}_{p\times q}(\mathbb{R})$ satisfies $A'(u)(w)=b(w)(u)$ for all $u$ and $w$ if and only if $A'(u)_{ij}=b_{ij}(u)$ for all $u\in S$, $i\in[p]$ and $j\in[q]$. So $A$ is the only map with the latter property. For $i\in[p]$ and $j\in[q]$, $b_{ij}\in\mathbb{R}^{S}$ by Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol (ii), so, by The Elements of the Class of Functions from a Set to a Set, and This Class Is a Set (i), $b_{ij}$ is a map $S\to\mathbb{R}$, with $b_{ij}(u)=A(u)_{ij}$ for every $u\in S$; so $b_{ij}=A_{ij}$, by the uniqueness in (ii).