For a formal treatment, you can see Kenneth Kunen, The Foundations of Mathematics (2009), page 45 :
Theorem 1.9.2 (Primitive Recursion on $ON$) Suppose that $\forall s \ \exists!y \ \varphi(s,y)$, and define $G(s)$ to be the unique $y$ such that $\varphi(s,y)$. Then we can define a formula $\psi$ for which the following are provable:
$\forall x \ \exists!y \ \psi(x,y)$, so $\psi$ defines a function $F$, where $F(x)$ is the $y$ such that $\psi(x,y)$.
$\forall \xi \in ON \ [F(\xi) = G(F \upharpoonright \xi)]$.
See page 91 :
Definition 11.4.1 A lexicon for Polish notation is a pair $(\mathcal W, \alpha)$ where $\mathcal W$ is a set of symbols and $\alpha : \mathcal W \to \omega$. Let $\mathcal W_n = \{s \in \mathcal W : \alpha(s) = n \}$. We say
that the symbols in $\mathcal W_n$ have arity $n$. $\mathcal W^{< \omega}$ denotes the set of all finite sequences of symbols in $\mathcal W$. The (well-formed) expressions of $(\mathcal W, \alpha)$ are all sequences constructed by the following rule:
(§) If $s \in \mathcal W_n$ and $\tau_i$ is an expression for each $i < n$, then $s \tau_1 \ldots \tau_{n-1}$ is an expression.
In the "standard" applications, most of the $\mathcal W_n$ are empty. For example, we can let $\mathcal W = \{ x, y, z, !, +, . \}$, with $\mathcal W_0 = \{ x, y, z \}, \mathcal W_1 = \{ ! \}, \mathcal W_2 = \{ +, . \}$ [and thus : $\alpha(+)= \alpha(.)=2$, because $+, .$ have arity $2$]; the rest are empty. Then the following shows nine expressions of this lexicon:
$$x \quad y \quad z \quad +xy \quad .yz \quad +xx \quad +x.yz \quad .+xyz \quad !.+xyz$$
See page 92 :
A symbol is really just a set, since everything is a set. We assume always that $\mathcal W \cap \mathcal W^{< \omega} = \emptyset$, and (§) uses the terminology of concatenation. We should also distinguish between the symbol $x \in \mathcal W_0$ and the expression of length $1$ consisting of $x$, which is set-theoretically $(x) = \{ \langle 0, x \rangle \} \in \mathcal W_1 = \mathcal W^{ \{ \emptyset \} }$. Note that the rule (§) is a recursive definition
of the notion of "expression". To justify this definition using Theorem 1.9.2, recursively define $F : \omega \to \mathcal P(\mathcal W^{< \omega})$, where $F(n)$ is the set of expressions of length $\le n$.