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
\begin{cases}
\prod_{n = 1}^N n, \quad & N > 0 \\
1, \quad & N = 0
\end{cases}
\end{equation}