The Factorial as a Map on the Natural Numbers with Zero

In the setting of The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion, let maps and their values be as in Sets and Maps: Ordinary Notation §maps, and for $n\in\mathbb{N}_{0}$ let $n!$ be the factorial of $n$.

¶ There is exactly one map $F:\mathbb{N}_{0}\to\mathbb{N}_{0}$ with $F(n)=n!$ for every $n\in\mathbb{N}_{0}$.

¶ The map $F$ of the clause map satisfies $F(0)=1$ and $F(n+1)=(n+1)\cdot F(n)$ for every $n\in\mathbb{N}_{0}$.