Lemma 12

Let K be the polynomially convex envelope of Sp$^p(\boldsymbol{f}(\boldsymbol{a}))$. One has $g(\boldsymbol{f}(\boldsymbol{a})) = (g\circ \boldsymbol{f})(\boldsymbol{a})$ for every germ $g\in \mathscr{O}(K; A)$.

Let Ψ be the mapping from $\mathscr{O}(K; A)$ into A such that $\Psi (g) = (g\circ \boldsymbol{f})(\boldsymbol{a})$. It is a continuous unital morphism such that $\Psi (z_j) =f_j(\boldsymbol{a})$, where $z_j$ is the germ of the $j$-th coordinate function on $\mathbf{C}^p$. When $g$ is the germ of a polynomial function, one therefore has $\Psi (g) =g(\boldsymbol{f}(\boldsymbol{a}))$. By th. 2 of I, p. 68, this formula remains valid for every $g\in \mathscr{O}(K; A)$.

Let us now prove the theorem. Let V be an open neighbourhood of Sp$^p(\boldsymbol{f}(\boldsymbol{a}))$ and $\widetilde{g}\in \mathscr{O}(V; A)$ a holomorphic function whose germ in a neighbourhood of Sp$^p(\boldsymbol{f}(\boldsymbol{a}))$ is equal to $g$. Let $\boldsymbol{b}\in \mathbf{C}^{p+q}$ be an envelopment of $(\boldsymbol{f}(\boldsymbol{a}),V)$ (Lemma 11 of I, p. 70) and $\pi : V\times \mathbf{C}^q\rightarrow V$ the canonical projection.

Let $\widetilde{f}_1, . . . ,\widetilde{f}_p$ be holomorphic functions whose germs are $f_1, . . . , f_p$ and let U be an open neighbourhood of Sp$^n(\boldsymbol{a})$ such that $(\widetilde{f}_1, . . . ,\widetilde{f}_p)(U)\subset V$. Let $\pi '$ be the canonical projection of $U\times \mathbf{C}^q$ onto U. Let us denote by $z_{n+1}, . . . , z_{n+q}$ the last $q$ coordinate functions on $\mathbf{C}^{n+q}$. Put $h=\widetilde{g}\circ (\widetilde{f}_1, . . . ,\widetilde{f}_p)$ and

The mapping $\widetilde{g}\circ \pi$ is holomorphic in the open neighbourhood $V\times \mathbf{C}^q$ of the polynomially convex envelope L of Sp$^{p+q}(\boldsymbol{b})$. By Lemma 12, applied to $\boldsymbol{c}$, to the germs in a neighbourhood of L of the functions

and to the germ of $\widetilde{g}\circ \pi$, we have

Since $\pi '(\boldsymbol{c}) =\boldsymbol{a}$, we have $(h\circ \pi ')(\boldsymbol{c}) =h(\boldsymbol{a})$ and $(f_i\circ \pi ')(\boldsymbol{c}) =f_i(\boldsymbol{a})$ for $1\leqslant i\leqslant p$ (property (CF3) of the holomorphic functional calculus). Since, moreover, $z_{n+j}(\boldsymbol{c}) =b_{p+j}$ for $1\leqslant j\leqslant q$ (property (CF2)), we have

whence we deduce $g(f_1(\boldsymbol{a}), . . . , f_p(\boldsymbol{a})) =h(\boldsymbol{a})$ by applying property (CF3) again.