Fixed point combinator (Y) and fixed point equation

In Hindley (Lambda-Calculus and Combinators, an Introduction), Corollary 3.3.1 to the fixed-point theorem states:

In $\lambda$ and CL: for every $Z$ and $n \ge 0$ the equation $$xy_1..y_n = Z$$
can be solved for $x$. That is, there is a term $X$ such that $$Xy_1..y_n =_{\beta,w} [X/x]Z$$

I dont understand how to even think about it. I was thinking that $y_1…y_n$ could be thought of as a function on which $X$ acts so $X$ is the fixed point I would like to find. Is that right?

And I dont even understand the proof a little bit, which is – Choose $X = \mathbf{Y}(\lambda x y_1…y_n.Z)$ What does it mean? How is it a solution? Can someone explain?

Note that $\mathbf{Y}$ here means any fixed-point combinator, i.e. $\mathbf{Y}X =_{\beta, w}X$ for any expression $X$.

Solutions Collecting From Web of "Fixed point combinator (Y) and fixed point equation"

Just apply equational reasoning starting from the provided solution
$$ X = \mathbf{Y}(\lambda x y_1 \ldots y_n.Z ) $$
Recall that $\mathbf{Y}F = F(\mathbf{Y}F)$ for any $\lambda$-term $F$, since $\mathbf{Y}$ is a fixed point combinator. In particular
$$
\mathbf{Y}(\lambda x y_1 \ldots y_n.Z ) =
(\lambda x y_1 \ldots y_n.Z ) (\mathbf{Y}(\lambda x y_1 \ldots y_n.Z ))
$$
Then we just compute:

$$
\begin{array}{ll}
& X y_1 \ldots y_n \\
= & \mbox{\{definition of $X$\}} \\
& \mathbf{Y}(\lambda x y_1 \ldots y_n.Z ) y_1 \ldots y_n \\
= & \mbox{\{fixed point property\}} \\
& (\lambda x y_1 \ldots y_n.Z ) (\mathbf{Y}(\lambda x y_1 \ldots y_n.Z )) y_1 \ldots y_n \\
= & \mbox{\{definition of $X$\}} \\
& (\lambda x y_1 \ldots y_n.Z ) X y_1 \ldots y_n \\
= & \mbox{\{$\beta$ reduction, applied $n+1$ times\}} \\
& [y_n / y_n] \ldots [ y_1 / y_1 ] [X/x] Z \\
= & \mbox{\{substituting a variable for itself has no effect\}} \\
& [X/x] Z \\
\end{array}
$$
Q.E.D.

Let me add some intuition about how one can find the proposed solution. Recall the equation
$$ x y_1 \ldots y_n = Z $$
and consider the easy case where $x \notin {\sf free}(Z)$. In this case there’s a trivial solution: $x$ can just take $n$ arguments $y_1 \ldots y_n$ and output $Z$:
$$
x = \lambda y_1 \ldots y_n. Z
$$
Hence, the above solves the easy case. What about the general one? There, the above equation does not provide a solution, since $x$ is present in the right hand side. However, we can apply a “reverse $\beta$ reduction step” to isolate such $x$:
$$
x = (\lambda x y_1 \ldots y_n. Z) x
$$
We can rewrite the above as
$$
x = F x \qquad\mbox{where } F = (\lambda x y_1 \ldots y_n. Z)
$$
Now, $F$ is a well-defined $\lambda$-term not involving $x$ as a free variable. All that is left is to solve the equation $x = F x$, but this is a fixed point equation so we can simply take $x = \mathbf{Y} F$ for this. Hence, we obtain the proposed solution.