The Recursion Theorem on Omega

In the setting of Class Theory NBG: the Axioms, Standing Conventions and Basic Notation, let $\omega$ and $0$ be as in The Class Omega of Natural Numbers with Zero §omega and The Class Omega of Natural Numbers with Zero §zero, and let $S(x)$ denote the successor of a set $x$. Let $a$ be a set, let $c\in a$, and let $g:\omega\times a\to a$ be a map from the Cartesian product $\omega\times a$ to $a$; for $n\in\omega$ and $u\in a$ write $g(n,u)$ for the value $g((n,u))$, which exists because $(n,u)\in\omega\times a$ by Membership in a Cartesian Product, and the Cartesian Product of Two Sets Is a Set §membership and $\omega\times a=\operatorname{dom}g$ by Functions, Values of a Function, and Functions from One Class to Another §map. For a map $f:\omega\to a$, the values $f(0)$ and $f(S(n))$, $n\in\omega$, exist because $0\in\omega$ and $S(n)\in\omega$ by Omega Is the Least Inductive Class: It Is a Set, Induction from Zero, the Peano Properties, and Transitivity §inductive, 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:\omega\to a$ such that $f(0)=c$ and $f(S(n))=g(n,f(n))$ for every $n\in\omega$.