From page 26 of Lambda-Calculus and Combinators:Definition 2.18 (Abstraction) For every CL-term $M$ and every variable $x$, a CL-term called $[x].M$ is defined by induction on $M$,  thus:(a) $[x].M \equiv \mathbf{K}M$ if $x \notin FV(M)$;(b) $[x].x \equiv \mathbf{I}$;(c) $[x]Ux \equiv U$ if $x \notin FV(U)$(f) $[x]UV \equiv \mathbf{S}([x]U)([x].V)$ if neither (a) nor (c)  applies.Here $\mathbf{I}$ is meant to denote the identity operator, $\mathbf{K}$ the constant operator, and $\mathbf{S}$ the stronger composition operator where in mathematical notation:$$\mathbf{S}(f,g))(x) = f(x, g(x)) \text{ for functions $f$, $g$}$$Question: It seems that (f) of this definition just comes out of nowhere. I have no idea what is motivating it behind the scenes. Does anybody have any insight on where this definition comes from?
Understanding A Recursive Definition of CL-Terms in Combinatory Logic
lambda calculus;combinatory logic