This question is a sort of follow-up of a previous one. Again, I just do not really see how the $\lambda$-calculus actually works. Now, the problem is with Example 2.13 at page 12 of Introduction to Lambda Calculus.
The authors write (I write the conditionals in the inverse order):
$\exists G \ \forall X \ GX= \mathbf{S}GX$. Indeed,
$$\begin{align} G \equiv \mathbf{Y} ( \lambda gx.\mathbf{S}gx) & \overset{?}{\Rightarrow} G = ( \lambda gx.\mathbf{S}gx)G\\ & \Rightarrow G = \lambda x.\mathbf{S}Gx\\ & \overset{?}{\Rightarrow} Gx = \mathbf{S}Gx\\ & \Rightarrow GX = {S}GX. \end{align} $$
where $\mathbf{Y} \equiv \lambda f.(\lambda x. f(xx)) (\lambda x. f(xx))$ and $\mathbf{S} \equiv \lambda xyz. xz(yz)$.
I think the last conditional comes form the fact that $x$ is arbitrary. Still, the question marks point out the steps that are really mysterious for me.
Also, the authors close the example by writing that the same result is obtained with $G \equiv \mathbf{Y}\mathbf{S}$. I simply have no idea how to manipulate this object.
Any feedback will be greatly appreciated.
Thank you for your time.
First, as stated in Theorem 2.12 of your notes, ${\bf Y}F = F({\bf Y}F)$ for any term $F$. Therefore, \begin{align} G \equiv {\bf Y} (\lambda gx.{\bf S} gx) = (\lambda gx.{\bf S} gx)({\bf Y} (\lambda gx.{\bf S} gx)) \equiv (\lambda gx.{\bf S} gx)G \end{align} This explains the first step you marked. Concerning the second step you marked, from $G = \lambda x.{\bf S} Gx$, by applying the $\beta$-rule (Definition 2.7 in your notes) and the first compatibility rule (Definition 2.7 in your notes), it follows that
\begin{align} Gx = (\lambda x.{\bf S} Gx)x = ({\bf S} Gx)[x := x] \equiv {\bf S} Gx. \end{align}
Finally, I show that even when you set $G \equiv {\bf YS}$, you get that $GX= \mathbf{S}GX$ for any term $X$. As above, by Theorem 2.12, \begin{align} G \equiv {\bf YS} = {\bf S}({\bf YS}) \equiv {\bf S} G \end{align} and so $GX = {\bf S}GX$ for any term $X$.