Proof of The Earlier and the New Versions of the Definitions of Euclidean Space, Real Matrices and Normed Spaces Agree

Each new version treated here has the text of its earlier version, except that the words "real numbers" carry a link to The Real Numbers as a Type and, for $\mathbb{R}^{n}$ and the real matrices, the adopted setting is a newer version. An element of $\mathrm{Real}$ in the sense of The Real Numbers as a Type (i) is given by its set, an element of $\mathbb{R}$, and corresponds to the element of the earlier $\mathrm{Real}$ with the same set, by The Earlier and the New Versions of the Definitions of the Natural Numbers, the Complex Numbers, the Conjugate and the Modulus Agree, and the Two Versions of Real Correspond (v); so the link names the elements of $\mathbb{R}$, as the earlier texts do.

(iii): apart from that link, Norms and Real Normed Spaces is Norms and Real Normed Spaces word for word, with the same references; in both the function $\lVert\cdot\rVert$ takes values in $\mathbb{R}$, so the four conditions on $\lVert\cdot\rVert$, and with them the notions of norm and of real normed space, are the same.

(i) and (ii): apart from that link, Euclidean Space $\mathbb{R}^n$: n-Tuples of Real Numbers with Their Componentwise Operations and Real Matrices: the Set of Real m x n Matrices with Their Entrywise Operations have the texts of Euclidean Space $\mathbb{R}^n$: n-Tuples of Real Numbers with Their Componentwise Operations and Real Matrices: the Set of Real m x n Matrices with Their Entrywise Operations word for word, with the same cited items, except that they adopt Metric Spaces: Balls, the Metric Topology, and the Real and Complex Numbers as Metric Spaces in place of Metric Spaces: Balls, the Metric Topology, and the Real and Complex Numbers as Metric Spaces. These two settings extend The Complex Numbers, with the Real Numbers Identified with a Subset of the Complex Numbers and The Complex Numbers, with the Real Numbers Identified with a Subset of the Complex Numbers, both extensions of The Real Numbers, with the Natural Numbers, Integers and Rationals Identified with Subsets of the Reals, and Completeness, and differ only in references to new versions of definitions, which fix the notation for complex numbers, for metric spaces with their sequences, limits, open sets and continuous maps, and for the modulus and the distances on $\mathbb{R}$ and $\mathbb{C}$. The two definitions use none of this notation; their $\mathbb{N}$, $\mathbb{R}$ and operations on $\mathbb{R}$ come from The Real Numbers, with the Natural Numbers, Integers and Rationals Identified with Subsets of the Reals, and Completeness in both. Hence the two versions define the same set $\mathbb{R}^{n}=\mathbb{R}^{[n]}$ and the same set $\mathcal{M}_{m\times n}(\mathbb{R})=\mathbb{R}^{[m]\times[n]}$, with the same pointwise operations, entries, origin and zero matrix.