The Natural Numbers Read in ℝ: a Predicative Condition and a Function from ℕ₀ to ℝ

In the setting of Routine Facts Used Without Citation: Arithmetic, Maps, Predicativity and Indices, for $n\in\mathbb{N}_{0}$ let $n_{\mathbb{R}}$ be its image in $\mathbb{R}$, the reading of $n$ in $\mathbb{R}$ of Commutative Rings, Fields and Ordered Fields: Standard Notation (iv). Let $N\ge2$ be a metatheoretic number, let $x_{0},\dots,x_{N-1}$ be distinct set variables, and let $i,j<N$ be distinct.

(i) A predicative condition. The condition "$x_{j}\in\mathbb{N}_{0}$ and $x_{i}=(x_{j})_{\mathbb{R}}$" on $x_{0},\dots,x_{N-1}$ is expressed by a predicative formula, with $x_{0},\dots,x_{N-1}$ in place of the variables $x_{1},\dots,x_{k}$ of Conditions Expressed by a Predicative Formula, and Guards (i) and no displayed variables.

(ii) A function from $\mathbb{N}_{0}$ to $\mathbb{R}$. There is exactly one function $\iota:\mathbb{N}_{0}\to\mathbb{R}$ with $\iota(n)=n_{\mathbb{R}}$ for every $n\in\mathbb{N}_{0}$.