> [!theoremb] Theorem
>
> Let $E, F, G$ be [[Banach Space|Banach spaces]], $U \subset E$, $V \subset F$ be [[Open Set|open]], and $f: U \times V \to G$ be a [$C^p$](Space%20of%20Continuously%20Differentiable%20Functions) mapping.
>
> Let $(a, b) \in U \times V$ such that $f(a, b) = 0$ and $D_2f(a, b) \in L(F, G)$ is a [[Space of Toplinear Isomorphisms|toplinear isomorphism]], then
> 1. There exists $U_0 \in \cn^o(a)$ and $g \in C(U_0, V)$ such that $g(a) = b$ and $f(x, g(x)) = 0$ on $U_0$.
> 2. There exists $U_1 \in \cn^o(a)$ such that $g|_{U_1} \in C^p(U_1, V)$ and $g|_{V_0}$ is the unique function in $C(U_1, V)$ such that $f(x, g(x)) = 0$ on $U_1$.
>
> *Proof*. $(1)$: Since $T = D_2f(a, b)$ is a toplinear isomorphism, define
> $
> F: U \times T(V) \to G \quad (a, b) \mapsto F(a, T^{-1}(b))
> $
> then $D_2F(a, b) = \text{Id}_G$. Thus we assume without loss of generality that $V \subset G$ and $D_2f(a, b) = \text{Id}_G$.
>
> Define
> $
> \varphi: U \times V \to E \times G \quad (x, y) \mapsto (x, f(x, y))
> $
> then
> $
> D\varphi(a, b) = \begin{bmatrix} \text{Id}_E & 0 \\ D_1f(a, b) & D_2f(a, b) \end{bmatrix} = \begin{bmatrix} \text{Id}_E & 0 \\ D_1f(a, b) & \text{Id}_G \end{bmatrix}
> $
> where
> $
> [D\varphi(a, b)]^{-1} = \begin{bmatrix} \text{Id}_E & 0 \\ -D_1f(a, b) & \text{Id}_G \end{bmatrix}
> $
> By the [[Inverse Function Theorem|inverse function theorem]], there exists $U_0 \in \cn^o(a)$ and $V_0 \in \cn^o(b)$ such that $\varphi|_{U_0 \cap V_0}$ is a $C^p$-isomorphism. Now define $g: U_0 \to V_0$ as the following composition
> $
> \begin{CD}
> U_0 @>x \mapsto (x, 0)>> \varphi(U_0 \times V_0) @>\varphi^{-1}>> U_0 \times V_0 @>\pi_2>> V_0
> \end{CD}
> $
> then $g \in C^p(U_0, V_0)$, and
> $
> \begin{align*}
> (x, f(x, g(x))) &= \varphi(x, g(x)) = \varphi(x, \pi_2 \circ \varphi^{-1}(x, 0)) \\
> &= \varphi(\varphi^{-1}(x, 0)) = (x, 0)
> \end{align*}
> $
> Therefore $f(x, g(x)) = 0$, and $g$ is the desired function.