Euclidean Norm on $\mathbb{R}^n$

Let $n$ be a natural number and let $x=(x_1,\dots,x_n)$ be a point of Euclidean space $\mathbb{R}^n$, so that each coordinate $x_i$ is a real number. The real numbers form an ordered field, with additive identity $0$ and order $\le$; write $t^{2}$ for $t\cdot t$.

By claim 2 of Nonnegativity of Squares in an Ordered Field each summand below satisfies $0\le x_i^{2}$, so by claim 5 of Properties of Finite Sums the finite sum $\sum_{i=1}^{n}x_i^{2}$ satisfies

The Euclidean norm of $x$ is the real number

where $\sqrt{\ \cdot\ }$ denotes the nonnegative square root given by Existence and Uniqueness of the Nonnegative Square Root.