Proof of Euclidean Points as Tuples of Real Numbers

Throughout we use the reading fixed in the statement: an element of $\mathbb{R}^n$ is a map from $[n]$ to $\mathbb{R}$, and for $k\in[n]$ the notation $x_k$ denotes the value of that map at $k$, as in the definition of tuples in a set.

Claim 1. Let $x,y\in\mathbb{R}^n$. Both are maps with domain $[n]$, and for $k\in[n]$ the real numbers $x_k$ and $y_k$ are their respective values at $k$. By the ambient convention for equality of maps recorded in the statement, two maps with the same domain are equal exactly when their values agree at every element of that domain. Hence $x=y$ holds if and only if $x_k=y_k$ for every $k\in[n]$.

Claim 2. Suppose a real number $a_k$ is assigned to each $k\in[n]$. This assignment attaches to each element of $[n]$ exactly one element of $\mathbb{R}$, so it is a map from $[n]$ to $\mathbb{R}$; call it $x$. Then $x\in\mathbb{R}^n$, and its value at $k$ is $a_k$, that is, $x_k=a_k$ for every $k\in[n]$. This proves existence. For uniqueness, let $y\in\mathbb{R}^n$ also satisfy $y_k=a_k$ for every $k\in[n]$. Then $x_k=a_k=y_k$ for every $k\in[n]$, so $x=y$ by claim 1.

Claim 3. Assume first that a map $f^k:S\to\mathbb{R}$ is given for each $k\in[n]$. Fix $s\in S$. The assignment sending each $k\in[n]$ to the real number $f^k(s)$ satisfies the hypothesis of claim 2, so there is exactly one element of $\mathbb{R}^n$ whose $k$-th component is $f^k(s)$ for every $k\in[n]$; denote it by $f(s)$. Since exactly one element of $\mathbb{R}^n$ is attached in this way to each $s\in S$, this defines a map $f:S\to\mathbb{R}^n$, and by construction $(f(s))_k=f^k(s)$ for every $s\in S$ and every $k\in[n]$.

For uniqueness, let $g:S\to\mathbb{R}^n$ also satisfy $(g(s))_k=f^k(s)$ for every $s\in S$ and every $k\in[n]$. Fix $s\in S$. Then $f(s)$ and $g(s)$ are elements of $\mathbb{R}^n$ with $(f(s))_k=f^k(s)=(g(s))_k$ for every $k\in[n]$, so $f(s)=g(s)$ by claim 1. Thus $f$ and $g$ are maps with the same domain $S$ whose values agree at every element of $S$, so $f=g$ by the ambient convention for equality of maps.

For the converse statement, let $f:S\to\mathbb{R}^n$ be a map and for each $k\in[n]$ let $f^k:S\to\mathbb{R}$ be defined by $f^k(s)=(f(s))_k$; each $f^k$ attaches exactly one real number to each $s\in S$ and so is indeed a map from $S$ to $\mathbb{R}$. These maps satisfy $(f(s))_k=f^k(s)$ for every $s\in S$ and every $k\in[n]$, which is the defining property above; by the uniqueness just proved, $f$ is the unique map determined by $f^1,\dots,f^n$.