@famesyasd: By the way, if you use choice or prove uniqueness of the function given by the recursion theorem, then it becomes even easier, because for each x you can define the function h = ( N y ↦ y=0 ? 1 : x·h(y−1) ) by recursion, and if it is unique then you can define the function that maps each x to the corresponding h, and hence obtain the desired function ^.

@LeakyNun: You never answered my last email. Let me know about it.

^ Not directly related to logic, but it is an example of unfolding a proof of a theorem applied to a specific situation to give a more concrete explanation.