Let us recall that we show that $f(a)=g(h_{1}(a),h_{2}(a))$ is representable if $g$ , $h_{1}$ and $h_{2}$ are (functionally) representable (by $\psi$ , $\theta_{1}$ and $\theta_{2}$ , respectively). We let $\phi$ be $\forall y_{1}\forall y_{2}(\theta_{1}(v_{1},y_{1})\rightarrow\theta_{2}(v_{1},y_{2})\rightarrow\psi(y_{1},y_{2},v_{2}))$ , and argue that for every $a\in\mathbb{N}$ , $$\begin{eqnarray*} A_{E}\vdash & \forall v_{2}[\psi(\mathbb{S}^{h_{1}(a)}0,\mathbb{S}^{h_{2}(a)}0,v_{2})\leftrightarrow v_{2}=\mathbb{S}^{f(a)}0] & (1)\\ A_{E}\vdash & \forall y_{1}[\theta_{1}(\mathbb{S}^{a}0,y_{1})\leftrightarrow y_{1}=\mathbb{S}^{h_{1}(a)}0] & (2)\\ A_{E}\vdash & \forall y_{2}[\theta_{2}(\mathbb{S}^{a}0,y_{2})\leftrightarrow y_{2}=\mathbb{S}^{h_{2}(a)}0] & (3) \end{eqnarray*}$$ imply $$\begin{eqnarray*} A_{E}\vdash & \forall v_{2}(\forall y_{1}\forall y_{2}[\theta_{1}(\mathbb{S}^{a}0,y_{1})\rightarrow\theta_{2}(\mathbb{S}^{a}0,y_{2})\\ & \rightarrow\psi(y_{1},y_{2},v_{2})]\leftrightarrow v_{2}=\mathbb{S}^{f(a)}0). & (4) \end{eqnarray*}$$

To show (4), by the generalization (DG) theorem, it is sufficient to show $A_{E}\vdash\forall y_{1}\forall y_{2}[\theta_{1}(\mathbb{S}^{a}0,y_{1})\rightarrow\theta_{2}(\mathbb{S}^{a}0,y_{2})$ $\rightarrow\psi(y_{1},y_{2},v_{2})]\leftrightarrow v_{2}=\mathbb{S}^{f(a)}0$ .

Now, $\forall y_{1}\forall y_{2}[\theta_{1}(\mathbb{S}^{a}0,y_{1})\rightarrow\theta_{2}(\mathbb{S}^{a}0,y_{2})$ $\rightarrow\psi(y_{1},y_{2},v_{2})]\rightarrow v_{2}=\mathbb{S}^{f(a)}0$ is logically equivalent to $\neg\forall y_{1}\forall y_{2}\neg\{[\theta_{1}(\mathbb{S}^{a}0,y_{1})\rightarrow\theta_{2}(\mathbb{S}^{a}0,y_{2})$ $\rightarrow\psi(y_{1},y_{2},v_{2})]\rightarrow v_{2}=\mathbb{S}^{f(a)}0\}$ (the prenex normal form, see Section 2.6), and to show $A_{E}\vdash\neg\forall y_{1}\forall y_{2}\neg\{[\theta_{1}(\mathbb{S}^{a}0,y_{1})\rightarrow\theta_{2}(\mathbb{S}^{a}0,y_{2})$ $\rightarrow\psi(y_{1},y_{2},v_{2})]\rightarrow v_{2}=\mathbb{S}^{f(a)}0\}$ it is sufficient to show that $A_{E}\vdash[\theta_{1}(\mathbb{S}^{a}0,t_{1})\rightarrow\theta_{2}(\mathbb{S}^{a}0,t_{2})\rightarrow\psi(t_{1},t_{2},v_{2})]\rightarrow v_{2}=\mathbb{S}^{f(a)}0$ for some terms $t_{1}$ and $t_{2}$ substitutable for $y_{1}$ and $y_{2}$ , respectively. So, let $t_{i}=\mathbb{S}^{h_{i}(a)}0$ . Then, by the deduction (DD) and contraposition (DC) theorems, it is sufficient to show that $A_{E};v_{2}\neq\mathbb{S}^{f(a)}0\vdash\theta_{1}(\mathbb{S}^{a}0,\mathbb{S}^{h_{1}(a)}0)\wedge\theta_{2}(\mathbb{S}^{a}0,\mathbb{S}^{h_{2}(a)}0)\wedge\neg\psi(\mathbb{S}^{h_{1}(a)}0,\mathbb{S}^{h_{2}(a)}0,v_{2})$ . By using deduction axiom group 2 (DA2), we can get rid of quantifiers in equations (1)-(3) and substitute $t_{i}$ for $y_{i}$ , hence, $$\begin{eqnarray*} A_{E}\vdash & \psi(\mathbb{S}^{h_{1}(a)}0,\mathbb{S}^{h_{2}(a)}0,v_{2})\leftrightarrow v_{2}=\mathbb{S}^{f(a)}0, & (5)\\ A_{E}\vdash & \theta_{1}(\mathbb{S}^{a}0,\mathbb{S}^{h_{1}(a)}0)\leftrightarrow\mathbb{S}^{h_{1}(a)}0=\mathbb{S}^{h_{1}(a)}0, & (6)\\ A_{E}\vdash & \theta_{2}(\mathbb{S}^{a}0,\mathbb{S}^{h_{2}(a)}0)\leftrightarrow\mathbb{S}^{h_{2}(a)}0=\mathbb{S}^{h_{2}(a)}0. & (7) \end{eqnarray*}$$ Equation (5), by DA1 and modus ponens (DMP), implies $A_{E};v_{2}\neq\mathbb{S}^{f(a)}0\vdash\neg\psi(\mathbb{S}^{h_{1}(a)}0,\mathbb{S}^{h_{2}(a)}0,v_{2})$ , and equations (6) and (7), by DA5, DA2, DA1 and DMP, imply $A_{E}\vdash\theta_{1}(\mathbb{S}^{a}0,\mathbb{S}^{h_{1}(a)}0)$ and $A_{E}\vdash\theta_{2}(\mathbb{S}^{a}0,\mathbb{S}^{h_{2}(a)}0)$ .

To show $A_{E}\vdash v_{2}=\mathbb{S}^{f(a)}0$ $\rightarrow\forall y_{1}\forall y_{2}[\theta_{1}(\mathbb{S}^{a}0,y_{1})\rightarrow\theta_{2}(\mathbb{S}^{a}0,y_{2})\rightarrow\psi(y_{1},y_{2},v_{2})]$ , by DD and DG, it is sufficient to show that $A_{E};v_{2}=\mathbb{S}^{f(a)}0;\theta_{1}(\mathbb{S}^{a}0,y_{1});\theta_{2}(\mathbb{S}^{a}0,y_{2})\vdash\psi(y_{1},y_{2},v_{2})$ . From (5), by DA1 and DMP, $A_{E};v_{2}=\mathbb{S}^{f(a)}0\vdash\psi(\mathbb{S}^{h_{1}(a)}0,\mathbb{S}^{h_{2}(a)}0,v_{2})$ . Further, by DA2, DA1 and DMP, equations (2) and (3) imply $A_{E};\theta_{1}(\mathbb{S}^{a}0,y_{1})\vdash y_{1}=\mathbb{S}^{h_{1}(a)}0$ and $A_{E};\theta_{2}(\mathbb{S}^{a}0,y_{2})\vdash y_{2}=\mathbb{S}^{h_{2}(a)}0$ , respectively. Moreover, by DA6, $\vdash\forall x(x=y_{1}\rightarrow\psi(x,y_{2},v_{2})\rightarrow\psi(y_{1},y_{2},v_{2}))$ and $\vdash\forall z(z=y_{2}\rightarrow\psi(\mathbb{S}^{h_{1}(a)}0,z,v_{2})\rightarrow\psi(\mathbb{S}^{h_{1}(a)}0,y_{2},v_{2}))$ , from which, by using DA2 and substituting $\mathbb{S}^{h_{1}(a)}0$ for $x$ and $\mathbb{S}^{h_{2}(a)}0$ for $z$ , we obtain $\vdash\mathbb{S}^{h_{1}(a)}0=y_{1}\rightarrow\psi(\mathbb{S}^{h_{1}(a)}0,y_{2},v_{2})\rightarrow\psi(y_{1},y_{2},v_{2})$ and $\vdash\mathbb{S}^{h_{2}(a)}0=y_{2}\rightarrow\psi(\mathbb{S}^{h_{1}(a)}0,\mathbb{S}^{h_{2}(a)}0,v_{2})\rightarrow\psi(\mathbb{S}^{h_{1}(a)}0,y_{2},v_{2})$ . Overall, by DMP, we have $A_{E};v_{2}=\mathbb{S}^{f(a)}0;\theta_{1}(\mathbb{S}^{a}0,y_{1});\theta_{2}(\mathbb{S}^{a}0,y_{2})\vdash\psi(y_{1},y_{2},v_{2})$ .