Proof of 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

Two definitions whose texts differ only in references to items that define the same objects, and in links that name those objects, define the same objects; each clause is checked this way, the correspondence of the two versions of $\mathrm{Real}$ first, since the new texts link to the second of them.

(v): The Real Numbers as a Type (i) and The Real Numbers as a Type (i) are the same word for word: in both, an element of $\mathrm{Real}$ is a set $x\in\mathbb{R}$, carried with the fact that it lies in $\mathbb{R}$, and two elements are equal when their sets are. So $\hat{x}$ exists and is unique, $x\mapsto\hat{x}$ is injective, and it is onto, since the set of an element of the second $\mathrm{Real}$ lies in $\mathbb{R}$ and is therefore the set of an element of the first. The Real Numbers as a Type (ii) and The Real Numbers as a Type (ii) agree on $0$, $1$, $+$, $\cdot$, $-$ and $\le$: in both these are the elements, operations and order of $\mathbb{R}$ (The Real Numbers (iii), The Real Numbers (iv)) and the negative in $\mathbb{R}$. Hence the set of $x+y$ and the set of $\hat{x}+\hat{y}$ are both the sum in $\mathbb{R}$ of the sets of $x$ and $y$, so $\widehat{x+y}=\hat{x}+\hat{y}$; the same argument gives the identities for $0$, $1$, $\cdot$ and $-$, and $x\le y$ and $\hat{x}\le\hat{y}$ both say that the set of $x$ is at most the set of $y$ in $\mathbb{R}$. Both versions also define $x-y$ as $x+(-y)$ and $x<y$ as the strict relation of $\le$, so $\widehat{x-y}=\widehat{x+(-y)}=\hat{x}+(-\hat{y})=\hat{x}-\hat{y}$, and $x<y$, that is $x\le y$ and $x\ne y$, holds if and only if $\hat{x}\le\hat{y}$ and $\hat{x}\ne\hat{y}$, as the correspondence is one-to-one. Finally, The Real Numbers as a Type (iii) and The Real Numbers as a Type (iii) are the same word for word and build numerals and powers recursively from $0$, $1$, $+$, $-$ and $\cdot$; by induction on $n$, using the identities just proved, the correspondence maps the numeral $n$ to $n$ and $x^{n}$ to $\hat{x}^{n}$, hence the integer numerals to the integer numerals, and $n\cdot x$ and $i\cdot x$ to $n\cdot\hat{x}$ and $i\cdot\hat{x}$. For $x\ne0$, The Reciprocal on the Type of Real Numbers (i) and The Real Numbers as a Type (vii) both take the element whose set is the reciprocal in $\mathbb{R}$ of the set of $x$, and $\hat{x}\ne0$ as the correspondence is one-to-one and maps $0$ to $0$; so the reciprocal of $x$ is mapped to the reciprocal of $\hat{x}$.

(i): The Set of Natural Numbers and the Number One has the text of The Set of Natural Numbers and the Number One word for word, with the same references; so both define $\mathbb{N}=\omega\setminus\{0\}$ and $1=S(0)$.

(ii): The Complex Numbers: Pairs of Real Numbers with Their Addition and Multiplication, and the Imaginary Unit has the text of The Complex Numbers: Pairs of Real Numbers with Their Addition and Multiplication, and the Imaginary Unit word for word, with the same references, except that The Complex Numbers: Pairs of Real Numbers with Their Addition and Multiplication, and the Imaginary Unit (i) adds that $\mathbb{R}\times\mathbb{R}$ is the set of pairs of real numbers, with a link to The Real Numbers as a Type. That link names the elements of $\mathbb{R}$: 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 (v). So both versions define $\mathbb{C}=\mathbb{R}\times\mathbb{R}$ with the same sum and product and $i=(0,1)$.

(iii) and (iv): The Complex Conjugate of a Complex Number and The Modulus of a Complex Number have the texts of The Complex Conjugate of a Complex Number and The Modulus of a Complex Number word for word, except that they adopt The Complex Numbers, with the Real Numbers Identified with a Subset of the Complex Numbers in place of The Complex Numbers, with the Real Numbers Identified with a Subset of the Complex Numbers, the remark of the modulus on real arguments cites a clause of the new setting, and The Modulus of a Complex Number (i) links the words "real number" to The Real Numbers as a Type. The two settings differ only in that The Complex Numbers, with the Real Numbers Identified with a Subset of the Complex Numbers (ii) and The Complex Numbers, with the Real Numbers Identified with a Subset of the Complex Numbers (iii) cite The Complex Numbers: Pairs of Real Numbers with Their Addition and Multiplication, and the Imaginary Unit where the earlier setting cites The Complex Numbers: Pairs of Real Numbers with Their Addition and Multiplication, and the Imaginary Unit; by (ii) they fix the same $\mathbb{C}$, sum, product and $i$, and so the same field notation on $\mathbb{C}$. Real and imaginary parts and square roots come from the same items Real and Imaginary Parts of a Complex Number (i) and The k-th Root and the Square Root of a Nonnegative Real Number (ii) in both versions. Hence

$$\overline{z}=\operatorname{Re}z-(\operatorname{Im}z)\,i,\qquad |z|=\sqrt{(\operatorname{Re}z)^{2}+(\operatorname{Im}z)^{2}}$$

denote the same complex number in both versions, and the same element of $\mathbb{R}$; the new version reads this element as the element of $\mathrm{Real}$ whose set it is, which corresponds to the earlier reading by (v). So the two moduli are the same real number.