As suggested, we define $u_{t}^{x}$ using recursion. Let $V$ be the set of variables and constant symbols, $T$ be the set of terms, and $h:V\rightarrow T$ be defined $$h(u)=\begin{cases} t & \mbox{if }u=x\\ u & \mbox{otherwise} \end{cases}.$$

Then, since $T$ is freely generated from $V$ by $\{\mathcal{F}_{f_{i}}\}$ where $f_{i}$ is an $n$ -place function symbol and $\mathcal{F}_{f_{i}}(u_{1},\ldots,u_{n})=f_{i}u_{1}\ldots u_{n}$ , there exists a unique extension $\overline{h}:T\rightarrow T$ such that a) $\overline{h}(u)=h(u)$ if $u\in V$ , and b) $\overline{h}(\mathcal{F}_{f_{i}}(u_{1},\ldots,u_{n}))=\mathcal{F}_{f_{i}}(\overline{h}(u_{1}),\ldots,\overline{h}(u_{n}))$ . We define $u_{t}^{x}$ to be $\overline{h}(u)$ .

Now, once $u_{t}^{x}$ is defined, we can refer to the forbidden word “replace” to verify that $u_{t}^{x}$ is indeed what we intended it to be. For $u=x$ , we have $x_{t}^{x}=\overline{h}(x)=h(x)=t$ , which is $u$ with $x$ replaced by $t$ . For any other variable symbol $y\neq x$ , we have $y_{t}^{x}=\overline{h}(y)=h(y)=y$ , and for any constant symbol $c$ , we have $c_{t}^{x}=\overline{h}(c)=h(c)=c$ , that is, in both cases, the term is left unchanged as there is no $x$ in it at all. For any other term of the form $u=f_{i}u_{1}\ldots u_{n}$ , we have $(f_{i}u_{1}\ldots u_{n})_{t}^{x}=\overline{h}(f_{i}u_{1}\ldots u_{n})$ $=\overline{h}(\mathcal{F}_{f_{i}}(u_{1},\ldots,u_{n}))$ $=\mathcal{F}_{f_{i}}(\overline{h}(u_{1}),\ldots,\overline{h}(u_{n}))$ $=f_{i}(u_{1})_{t}^{x}\ldots(u_{n})_{t}^{x}$ , i.e. $(f_{i}u_{1}\ldots u_{n})_{t}^{x}$ is obtained by substituting $t$ for $x$ in each term $u_{k}$ , $k=1,\ldots,n$ .

Finally, we observe that by definition, the extension $\overline{h}:T\rightarrow T$ , i.e. $u_{t}^{x}$ is a term.