[proofplan] We first pass to arbitrary holomorphic coordinates near $p$ and $F(p)$ and translate them so that both distinguished points have coordinate value $0$. The submersion hypothesis says that the coordinate Jacobian has rank $n$, so after reordering the source coordinates one can find an invertible $n \times n$ minor. We then build an auxiliary holomorphic map whose first $n$ components are the coordinate components of $F$ and whose remaining components are the unused source coordinates. Its derivative is invertible at $0$, so the [holomorphic inverse function theorem](/theorems/4950) gives a new holomorphic coordinate system in which $F$ is exactly projection onto the first $n$ coordinates. [/proofplan]

[step:Pass to centered holomorphic coordinate charts] Let $(U_0,\varphi)$ be a holomorphic coordinate chart on $X$ with $p \in U_0$, where \begin{align*} \varphi: U_0 \to \Omega_0 \subseteq \mathbb C^m \end{align*} is biholomorphic onto the [open set](/page/Open%20Set) $\Omega_0 := \varphi(U_0)$. Let $(V_0,\psi)$ be a holomorphic coordinate chart on $Y$ with $F(p) \in V_0$, where \begin{align*} \psi: V_0 \to \Lambda_0 \subseteq \mathbb C^n \end{align*} is biholomorphic onto the open set $\Lambda_0 := \psi(V_0)$. Since $F$ is continuous and $V_0$ is open, after replacing $U_0$ by the open neighbourhood $U_0 \cap F^{-1}(V_0)$ of $p$, we may assume $F(U_0) \subseteq V_0$. Define centered coordinate maps \begin{align*} \zeta: U_0 \to \Omega \subseteq \mathbb C^m, \qquad \zeta(q) := \varphi(q) - \varphi(p) \end{align*} and \begin{align*} \eta: V_0 \to \Lambda \subseteq \mathbb C^n, \qquad \eta(y) := \psi(y) - \psi(F(p)). \end{align*} Then $\zeta(p)=0$, $\eta(F(p))=0$, and $\zeta,\eta$ are holomorphic coordinate maps. Define the coordinate representative of $F$ by \begin{align*} f: \Omega \to \Lambda, \qquad f := \eta \circ F \circ \zeta^{-1}. \end{align*} This is a holomorphic map between open subsets of Euclidean complex spaces, and $f(0)=0$. [/step]

[step:Choose source coordinates with an invertible Jacobian minor]The differential $dF_p: T_pX \to T_{F(p)}Y$ is surjective by hypothesis. Under the coordinate identifications induced by $d\zeta_p: T_pX \to \mathbb C^m$ and $d\eta_{F(p)}: T_{F(p)}Y \to \mathbb C^n$, the [linear map](/page/Linear%20Map) $dF_p$ is represented by the complex Jacobian matrix $Jf_0 \in \mathbb C^{n \times m}$ of $f$ at $0$. Hence $Jf_0$ has rank $n$. In particular, $m \geq n$. Since $Jf_0$ has rank $n$, some collection of $n$ columns is linearly independent. Reordering the source coordinate functions $\zeta_1,\dots,\zeta_m$ if necessary, we may assume that the first $n$ columns are linearly independent. Define the matrix $A \in \mathbb C^{n \times n}$ by \begin{align*} A_{ij} := \frac{\partial f_i}{\partial \zeta_j}(0) \quad \text{for } 1 \leq i,j \leq n. \end{align*} Then $\det A \neq 0$.[/step]

[guided]The submersion condition is the point at which the local normal form enters. In coordinates, the differential of $F$ at $p$ becomes the Jacobian matrix $Jf_0$ of the coordinate map $f = \eta \circ F \circ \zeta^{-1}$ at $0$. Because changing coordinates composes $dF_p$ with complex-linear isomorphisms $d\zeta_p$ and $d\eta_{F(p)}$, surjectivity of $dF_p$ is equivalent to surjectivity of the linear map represented by $Jf_0: \mathbb C^m \to \mathbb C^n$. A surjective complex-linear map $\mathbb C^m \to \mathbb C^n$ has rank $n$. This immediately forces $m \geq n$. It also means that among the $m$ columns of $Jf_0$, there are $n$ linearly independent columns. Reordering the source coordinates only permutes the columns of $Jf_0$, so we may arrange that these independent columns are the first $n$ columns. After this reordering, define $A \in \mathbb C^{n \times n}$ by \begin{align*} A_{ij} := \frac{\partial f_i}{\partial \zeta_j}(0) \quad \text{for } 1 \leq i,j \leq n. \end{align*} The columns of $A$ are exactly the first $n$ columns of $Jf_0$, restricted to the $n$ target components. Since those columns are linearly independent in $\mathbb C^n$, the square matrix $A$ is invertible, equivalently $\det A \neq 0$.[/guided]

[step:Build a holomorphic map whose first coordinates are the components of $F$] Define a holomorphic map \begin{align*} G: \Omega \to \mathbb C^m, \qquad G(\zeta_1,\dots,\zeta_m) := (f_1(\zeta),\dots,f_n(\zeta),\zeta_{n+1},\dots,\zeta_m). \end{align*} Here $\zeta=(\zeta_1,\dots,\zeta_m) \in \Omega$. The map $G$ is holomorphic because its first $n$ component functions are the holomorphic component functions of $f$, and its last $m-n$ component functions are coordinate projections. [/step]

[step:Verify that the auxiliary map has invertible derivative] Let $JG_0 \in \mathbb C^{m \times m}$ be the complex Jacobian matrix of $G$ at $0$. We prove that $JG_0$ is invertible. Let $v=(v_1,\dots,v_m) \in \mathbb C^m$ satisfy $JG_0v=0$. The last $m-n$ components of $G$ are $\zeta_{n+1},\dots,\zeta_m$, so the last $m-n$ equations in $JG_0v=0$ give \begin{align*} v_{n+1}=\cdots=v_m=0. \end{align*} The first $n$ equations then reduce to \begin{align*} A(v_1,\dots,v_n)=0. \end{align*} Since $\det A \neq 0$, the matrix $A$ is invertible, and hence \begin{align*} v_1=\cdots=v_n=0. \end{align*} Thus $v=0$, so $JG_0$ has trivial kernel. As a complex-linear map from $\mathbb C^m$ to itself, $JG_0$ is therefore invertible. [/step]

[step:Use the inverse function theorem to make the auxiliary map a source coordinate chart] By the holomorphic [inverse function theorem](/theorems/51) applied to $G$ at $0$ (citing a result not yet in the wiki: Holomorphic Inverse Function Theorem), there exists an open neighbourhood $\Omega_1 \subseteq \Omega$ of $0$ such that $G(\Omega_1)$ is open in $\mathbb C^m$ and \begin{align*} G|_{\Omega_1}: \Omega_1 \to G(\Omega_1) \end{align*} is biholomorphic. Set $U := \zeta^{-1}(\Omega_1)$. Define a holomorphic coordinate map \begin{align*} z: U \to G(\Omega_1), \qquad z := G \circ \zeta. \end{align*} Then $z(p)=G(0)=0$, and $z$ is a holomorphic coordinate chart on $X$ about $p$. [/step]

[step:Read the map in the new source coordinates] Keep the target coordinate map \begin{align*} w: V_0 \to \Lambda, \qquad w := \eta. \end{align*} After replacing $U$ by the open neighbourhood $U \cap F^{-1}(V_0)$ if needed, we still have $F(U) \subseteq V_0$. Let $z=(z_1,\dots,z_m) \in z(U)=G(\Omega_1)$, and let $\zeta := G^{-1}(z) \in \Omega_1$. By the definition of $G$, \begin{align*} z = G(\zeta) = (f_1(\zeta),\dots,f_n(\zeta),\zeta_{n+1},\dots,\zeta_m). \end{align*} Therefore the first $n$ components of $z$ are exactly the components of $f(\zeta)$. Since $f=\eta \circ F \circ \zeta^{-1}$ and $w=\eta$, we obtain \begin{align*} (w \circ F \circ z^{-1})(z_1,\dots,z_m) = f(\zeta) = (z_1,\dots,z_n). \end{align*} This is the desired local coordinate expression for $F$, and the proof is complete. [/step]