Recursion on the Natural Numbers Starting at One

In the setting of Class Theory NBG: the Axioms, Standing Conventions and Basic Notation, let $\mathbb{N}$ and $1$ be as in The Set of Natural Numbers and the Number One §naturals and The Set of Natural Numbers and the Number One §one, and let $+$ be the addition. Let $a$ be a set, let $c\in a$, and let $g:\mathbb{N}\times a\to a$ be a map on the Cartesian product $\mathbb{N}\times a$; for $n\in\mathbb{N}$ and $u\in a$ write $g(n,u)$ for the value $g((n,u))$, which exists because $(n,u)\in\mathbb{N}\times a$ by Membership in a Cartesian Product, and the Cartesian Product of Two Sets Is a Set §membership and $\mathbb{N}\times a$ is the domain of $g$ by Functions, Values of a Function, and Functions from One Class to Another §map. For a map $f:\mathbb{N}\to a$ and $n\in\mathbb{N}$, the values $f(1)$ and $f(n+1)$ exist because the domain of $f$ is $\mathbb{N}$ by Functions, Values of a Function, and Functions from One Class to Another §map, $1\in\mathbb{N}$ by Natural Numbers Are the Successors in Omega: One Is Least and Not a Successor of a Natural Number, the Successor Is Injective, and N Is Closed under Addition and Multiplication §one, and $n+1\in\mathbb{N}$ by Natural Numbers Are the Successors in Omega: One Is Least and Not a Successor of a Natural Number, the Successor Is Injective, and N Is Closed under Addition and Multiplication §closed; and $f(n)\in a$ because it lies in the range of $f$, which is included in $a$ by Functions, Values of a Function, and Functions from One Class to Another §map, so $g(n,f(n))$ exists.

¶ There is exactly one map $f:\mathbb{N}\to a$ such that $f(1)=c$ and $f(n+1)=g(n,f(n))$ for every $n\in\mathbb{N}$.