Let $\mathbb{N}$ be the D225: Set of natural numbers.
The natural number factorial function is the D4949: Natural number function \begin{equation} \mathbb{N} \to \mathbb{N}, \quad N \mapsto I_{N > 0} \left( \prod_{n = 1}^N n \right) + I_{N = 0} \end{equation}