 In the general case there is indeed no guarantee that there will exist a unique extensional function satisfying such a definition. But in the case of this example it can be shown that \(2 \times x\) is the unique function of type \(\mathbb{N} \rightarrow \mathbb{N}\) satisfying \(\phi(x)\) in the system of equations (\ref{genrecex}). This may be illustrated by considering the following calculation of \(\phi(2)\):