Sometimes a sequence $(s_n)_{n \in \mathbf{N}}$, where $\mathbf{N}$ is the set of natural numbers, is defined as follows: (a) let $s_0 = ...$; (b) for $n \geq0$ assume that $s_0, s_1, s_2, \dots, s_n$ have already been defined; then define $s_{n+1}$ in terms of$s_0, s_1, s_2, \dots, s_n$ by .....
What is a precise statement of the mathematical theorem justifying that "complete recursion" (an analog of "complete" induction)? Where might one find it stated in the literature along with a proof?
I ask this because so often even the definition of the factorial function is wrongly based upon too weak a theorem. [Justifying the usual definition requires not "ordinary" recursion, but rather "primitive recursion" — start with a set $X$, an element $c \in X$, and a function $G : X \times \mathbf{N} \rightarrow X$; then the theorem on primitive recursion asserts the existence of a unique function $f : \mathbf{N} \rightarrow X$ such that $f(0) = c$ and, for each $n \in \mathbf{N}$, $f(n+1) = G(n, f(n))$.]
The issue is mainly being able to say what kind of function or relation replaces such $G$ when one is dealing with a "function" that has a variable number of arguments.
Here's an attempt at such a thorem. Is this valid? And is there some place specific in the literature where it appears?
Theorem. Let $X$ be a set, let $c \in X$, and let $G : \bigcup_{n=1}^{\infty} X^{n} \rightarrow X$ be a given map (where $X^{n}$ denotes the $n$-fold Cartesian product of $X$ with itself). Then there is a unique map $f : \mathbf{N} \rightarrow X$ such that $f(0) = c$ and, for each $n \in \mathbf{N}$, we have $f(n+1) = G(f(0), f(1), f(2), \dots, f(n))$.