Question regarding Karp-Lipton theorem
The subformula $s(y) = \exists z V(x,y,z)$ is a Boolean function which depends on $x$ and $y$. In this context we can assume that $x$ is fixed, so we only show the dependence on $s(y)$. Here $\exists z V(x,y,z)$ is the definition of the function: the value of $s$ on an input $y$ equals the truth value of the formula $\exists z V(x,y,z)$ (recall we're assuming that $x$ is fixed).

Since $V$ runs in polynomial time, as in Cook's theorem we can encode $V(x,y,z)$ is a polynomial size formula in the variables $x,y,z$. Given the fixed input $x$ and an input $y$, we can substitute $x$ and $y$ in the formula for $V(x,y,z)$ to get a formula $\varphi_{x,y}$ depending only on $z$. We can also convert this formula to CNF. The new formula is satisfiable, i.e. $s(y)$ is true, iff $\varphi_{x,y} \in SAT$.

If we have a circuit $C$ solving SAT we can use it to check whether $\varphi_{x,y}$ is satisfiable. That's what Wikipedia means when it writes $C(s(y))$: write $s(y)$ as an instance $\varphi_{x,y}$ of SAT, and then run $C$ on the instance to get the truth value of $s(y)$. Since $C$ solves SAT, $C(s(y)) = s(y)$, that is, on input $\varphi_{x,y}$ the circuit $C$ will output the truth value of $s(y)$.