The holomorphic inverse function theorem in several complex variables

By [L1], every component of $F$ is holomorphic and therefore smooth as a real-valued pair of functions on ${\mathbb{R}}^{2m}$. Hence the underlying real map $F:U\subseteq {\mathbb{R}}^{2m}\to {\mathbb{R}}^{2m}$ is $C^1$ on a neighbourhood of $a$.

The real derivative $DF(a)$ is the same linear map as the complex differential, now read over $\mathbb{R}$. Since $\det J_{\mathbb{C}}F(a)\mathrm{\ne }0$, [L2] gives ${\det }_{\mathbb{R}}DF(a)\mathrm{\ne }0$, so $DF(a)$ is invertible as a real linear map.

Apply [L3] to the real map from step 1.1 and the invertible derivative from step 1.2. This gives open neighbourhoods $U_0$ of $a$ and $V_0$ of $F(a)$ such that $F{\mathrm{\mid }}_{U_0}:U_0\to V_0$ is bijective and has a $C^1$ inverse $G:V_0\to U_0$. Moreover, $DG(w)=DF(G(w){)}^{-1}(w\in V_0)\mathrm{.}$

For each $w\in V_0$, the linear map $DF(G(w))$ is $\mathbb{C}$-linear because $F$ is holomorphic, so its inverse $DG(w)$ is also $\mathbb{C}$-linear. Step 2.1 already gives $G$ real differentiable at every point with that differential, hence the defining linear approximation for holomorphy uses a $\mathbb{C}$-linear derivative. Therefore $G$ is holomorphic on $V_0$. Together with the holomorphy of $F{\mathrm{\mid }}_{U_0}$, [F1] makes $F{\mathrm{\mid }}_{U_0}$ biholomorphic.