Confusion about the factorial function in lambda calculus

Your formula, with the condensed abstraction syntax, is

$$\text{FAC}=λnf.n\ (λfn.n\ (f\ (λfx.n\ f\ (f\ x))))\ (λx.f)\ (λx.x)$$

The $λfx.n\ f\ (f\ x)$ is of course $\text{SUCC}\ n$, so let's write it this way,

$$\text{FAC}=λnf.n\ (λfn.n\ (f\ (\text{SUCC}\ n)))\ (λx.f)\ (λx.x)$$

and use mnemonic names to guide understanding,

$$\text{FAC}=λnf.n\ (λra.a\ (r\ (\text{SUCC}\ a)))\ (λa. f)\ 1$$

(with $a$ for "accumulator" and $r$ for "recursive part") and now we see clearly that it is indeed correct, transforming e.g. $\text{FAC}\ 4\ f$ into

$ \qquad \begin{align} 0\ f\ x \, = \,\, & x \, \\ 1\ f\ x \, = \,\, & f\ x \, \\ \text{K}\ f\ a = \,\, & f \, \\ \text{R}\ r\ a\ \triangleq & \ a\ (r\ (\text{SUCC}\ a)) \\ \, \\ \text{FAC}\ 4\ f &=_{_{\beta}} 4\ R\ (K\ f)\ 1 \\ &=_{_{\beta}} R\ (R\ (R\ (R\ (K\ f))))\ 1 \\ &=_{_{\beta}} 1\,\ (R\ (R\ (R\ (K\ f)))\ 2) \\ &=_{_{\beta}} 1\,\ (2\,\ (R\ (R\ (K\ f))\ 3)) \\ &=_{_{\beta}} 1\,\ (2\,\ (3\,\ (R\ (K\ f)\ 4))) \\ &=_{_{\beta}} 1\,\ (2\,\ (3\,\ (4\,\ (K\ f\ 5)))) \\ &=_{_{\beta}} 1\,\ (2\,\ (3\,\ (4\,\ f))) \\ &=_{_{\beta}} (1 * (2 * (3 * 4)))\ f \end{align} $

We have $1 = \lambda f x.f x =_{_{\eta}} \lambda f.f$, so that's not a problem.

As can be seen above, doing manual reductions is oftentimes much easier in the equational style, using combinators, i.e. "lifted lambdas" in the programming jargon. Indeed,

$ \qquad \begin{align} \text{FAC}\ 0\ f\ x &=_{_{\beta}} 0\ R\ (K\ f)\ 1\ x \\ &=_{_{\beta}} K\ f\ 1\ x \\ &=_{_{\beta}} f\ x \\ &=_{_{\beta}} 1\ f\ x \\ \, \text{FAC}\ 1\ f\ x &=_{_{\beta}} 1\ R\ (K\ f)\ 1\ x \\ &=_{_{\beta}} R\ (K\ f)\ 1\ x \\ &=_{_{\beta}} 1\ (K\ f\ 2)\ x \\ &=_{_{\beta}} K\ f\ 2\ x \\ &=_{_{\beta}} f\ x \\ &=_{_{\beta}} 1\ f\ x \end{align} $

and so $ \qquad \begin{align} \text{FAC}\ 0 &=_{_{\eta}} 1 \\ \, \text{FAC}\ 1 &=_{_{\eta}} 1 \end{align} $