[proofplan]
We prove existence and uniqueness of the Weierstrass factorisation by applying [the argument principle](/theorems/356) in the $z_n$-variable. Since $z_n \mapsto f(0, \dots, 0, z_n)$ has a zero of order $k$ at the origin, for small $r > 0$ this function has no zeros on $|z_n| = r$ and exactly $k$ zeros (counted with multiplicity) inside $|z_n| < r$. By continuity, for $z'$ sufficiently small, the function $z_n \mapsto f(z', z_n)$ retains exactly $k$ zeros inside the circle. We define the Weierstrass polynomial $w(z', z_n)$ as the monic polynomial whose roots are these $k$ zeros, construct the unit $u = f/w$, verify holomorphicity of both factors via the [argument principle](/page/Argument%20Principle) and symmetric function formulas, and prove uniqueness by the irreducibility structure of $\mathcal{O}_n$.
[/proofplan]
[step:Locate the $k$ zeros of $z_n \mapsto f(z', z_n)$ for small $z'$ via the argument principle]
Since $z_n \mapsto f(0, z_n)$ has a zero of order $k$ at $z_n = 0$ and is not identically zero, there exists $r > 0$ such that $f(0, z_n) \neq 0$ for all $0 < |z_n| \leq r$. Set $m := \min_{|z_n| = r} |f(0, z_n)| > 0$. By continuity of $f$, there exists $\delta > 0$ such that for all $|z'| < \delta$ and $|z_n| = r$:
\begin{align*}
|f(z', z_n) - f(0, z_n)| < m \leq |f(0, z_n)|.
\end{align*}
By [Rouché's Theorem](/theorems/???), the functions $z_n \mapsto f(z', z_n)$ and $z_n \mapsto f(0, z_n)$ have the same number of zeros (counted with multiplicity) inside $|z_n| < r$. Since $f(0, z_n)$ has exactly $k$ zeros there (all at $z_n = 0$), the function $z_n \mapsto f(z', z_n)$ has exactly $k$ zeros $\zeta_1(z'), \dots, \zeta_k(z')$ (counted with multiplicity) inside $|z_n| < r$ for each $|z'| < \delta$.
[guided]
The starting point is the hypothesis that $z_n \mapsto f(0, \dots, 0, z_n)$ vanishes to order $k$ at the origin. This means $f(0, z_n) = z_n^k g(z_n)$ where $g: \mathbb{D}(0, R) \to \mathbb{C}$ is holomorphic with $g(0) \neq 0$. In particular, $f(0, z_n) \neq 0$ for $z_n$ in some punctured disc $0 < |z_n| \leq r$.
Choose $r > 0$ small enough that $f(0, z_n) \neq 0$ on the circle $|z_n| = r$, and set $m := \min_{|z_n| = r} |f(0, z_n)| > 0$. Since $f$ is continuous on the compact set $\{|z'| \leq \delta\} \times \{|z_n| = r\}$ for some $\delta > 0$, we can choose $\delta$ so that $|f(z', z_n) - f(0, z_n)| < m$ whenever $|z'| < \delta$ and $|z_n| = r$.
Why does this help? Because [Rouché's Theorem](/theorems/???) says: if $h_1$ and $h_2$ are holomorphic on a neighbourhood of $\overline{\mathbb{D}(0,r)}$ and $|h_1 - h_2| < |h_2|$ on $|z_n| = r$, then $h_1$ and $h_2$ have the same number of zeros (with multiplicity) inside $|z_n| < r$. Applying this with $h_1(\zeta) = f(z', \zeta)$ and $h_2(\zeta) = f(0, \zeta)$, we conclude that for each $|z'| < \delta$, the map $z_n \mapsto f(z', z_n)$ has exactly $k$ zeros $\zeta_1(z'), \dots, \zeta_k(z')$ inside $|z_n| < r$. These zeros move continuously with $z'$ and all tend to $0$ as $z' \to 0$.
[/guided]
[/step]
[step:Define the Weierstrass polynomial $w$ via the elementary symmetric functions of the zeros]
Define the Weierstrass polynomial as the monic polynomial in $z_n$ whose roots are the $k$ zeros:
\begin{align*}
w(z', z_n) := \prod_{j=1}^{k} (z_n - \zeta_j(z')) = z_n^k + c_{k-1}(z') z_n^{k-1} + \cdots + c_0(z').
\end{align*}
The coefficients $c_j(z')$ are (up to sign) the elementary symmetric polynomials of $\zeta_1(z'), \dots, \zeta_k(z')$. We express these using [the argument principle](/theorems/356). The Newton power sums
\begin{align*}
p_m: \{|z'| < \delta\} &\to \mathbb{C} \\
z' &\mapsto \sum_{j=1}^k \zeta_j(z')^m = \frac{1}{2\pi i} \oint_{|z_n| = r} \frac{z_n^m \, \partial_{z_n} f(z', z_n)}{f(z', z_n)} \, dz_n
\end{align*}
are holomorphic in $z'$ for each $m \geq 0$, because the integrand is continuous on $\{|z'| < \delta\} \times \{|z_n| = r\}$ (where $f(z', z_n) \neq 0$ by the choice of $\delta$ and $r$) and holomorphic in $z'$ for each fixed $z_n$ on the circle, so differentiation under the integral sign applies. By Newton's identities, the elementary symmetric functions $c_j(z')$ are polynomial expressions in $p_1(z'), \dots, p_k(z')$, and hence $c_j \in \mathcal{O}(\{|z'| < \delta\})$ for each $j$. Moreover, $c_j(0) = 0$ for all $j$ because all $k$ zeros coalesce at $z_n = 0$ when $z' = 0$.
[guided]
The zeros $\zeta_j(z')$ themselves need not depend holomorphically on $z'$ (they may permute as $z'$ varies), but their symmetric functions always depend holomorphically. The elegant tool here is the [argument principle](/page/Argument%20Principle) in one complex variable: the [Generalized Argument Principle](/theorems/3359) tells us that if $g$ is holomorphic on a neighbourhood of $\overline{\mathbb{D}(0, r)}$ with no zeros on $|z_n| = r$, then
\begin{align*}
\sum_{g(a_j) = 0} h(a_j) = \frac{1}{2\pi i} \oint_{|z_n| = r} h(z_n) \frac{g'(z_n)}{g(z_n)} \, dz_n,
\end{align*}
where the sum is over zeros $a_j$ of $g$ inside $|z_n| < r$, counted with multiplicity, and $h$ is any [holomorphic function](/page/Holomorphic%20Function). Apply this with $g(\zeta) = f(z', \zeta)$ and $h(\zeta) = \zeta^m$ to obtain the power sum $p_m(z') = \sum_{j=1}^k \zeta_j(z')^m$ as a contour integral.
Why is $p_m$ holomorphic in $z'$? The integrand $z_n^m \cdot \partial_{z_n} f(z', z_n) / f(z', z_n)$ is a continuous function of $(z', z_n)$ on $\{|z'| < \delta\} \times \{|z_n| = r\}$ (where $f$ is guaranteed nonzero), and for fixed $z_n$ it is holomorphic in $z'$ (since $f$ and $\partial_{z_n} f$ are both holomorphic in all variables, and $f \neq 0$ on the circle). Differentiation under the integral sign is justified by the uniform boundedness of the integrand on compact subsets.
Newton's identities express the elementary symmetric polynomials $e_1, \dots, e_k$ of $\zeta_1, \dots, \zeta_k$ in terms of the power sums $p_1, \dots, p_k$ via
\begin{align*}
e_1 &= p_1, \\
2e_2 &= e_1 p_1 - p_2, \\
3e_3 &= e_2 p_1 - e_1 p_2 + p_3,
\end{align*}
and so on. Since each $p_m$ is holomorphic, each $e_m$ is holomorphic. The coefficients of the Weierstrass polynomial are $c_{k-j}(z') = (-1)^j e_j(z')$, so $c_j \in \mathcal{O}(\{|z'| < \delta\})$. At $z' = 0$, all zeros are $\zeta_j(0) = 0$, so $e_j(0) = 0$ for all $j \geq 1$, giving $c_j(0) = 0$.
[/guided]
[/step]
[step:Define the unit $u = f/w$ and verify it is holomorphic and nowhere vanishing]
On the set $\{|z'| < \delta, |z_n| < r\}$, define
\begin{align*}
u: \{|z'| < \delta\} \times \mathbb{D}(0, r) &\to \mathbb{C} \\
(z', z_n) &\mapsto \frac{f(z', z_n)}{w(z', z_n)}.
\end{align*}
For each fixed $z'$ with $|z'| < \delta$, the zeros of $z_n \mapsto f(z', z_n)$ inside $|z_n| < r$ are exactly $\zeta_1(z'), \dots, \zeta_k(z')$ (with the correct multiplicities), and these are exactly the zeros of $z_n \mapsto w(z', z_n)$. Therefore $z_n \mapsto u(z', z_n)$ extends to a [holomorphic function](/page/Holomorphic%20Function) of $z_n$ with no zeros in $|z_n| < r$, by the removable singularity theorem in one variable.
To verify joint holomorphicity of $u$, we express it via a contour integral. For $|z_n| < r$:
\begin{align*}
u(z', z_n) = \frac{1}{2\pi i} \oint_{|\zeta| = r} \frac{f(z', \zeta)}{w(z', \zeta)} \cdot \frac{1}{\zeta - z_n} \, d\zeta.
\end{align*}
This representation is valid because on $|\zeta| = r$, both $f(z', \zeta) \neq 0$ and $w(z', \zeta) \neq 0$ (all zeros of $w$ in $z_n$ lie strictly inside $|z_n| < r$, and $f$ is nonzero on the circle by Rouché). The integrand is continuous in $(z', z_n, \zeta)$ and holomorphic in $(z', z_n)$ for fixed $\zeta$, so differentiation under the integral sign gives $u \in \mathcal{O}(\{|z'| < \delta\} \times \mathbb{D}(0, r))$. Since $u(z', z_n) \neq 0$ for all $(z', z_n)$ in this neighbourhood (as $f$ and $w$ have identical zero sets), $u$ is a unit.
[guided]
The quotient $f/w$ might appear to have singularities where $w = 0$, but this cannot happen because $f$ vanishes at exactly the same points as $w$ in the $z_n$-variable, with the same multiplicities. For a fixed $z'$, the one-variable function $z_n \mapsto f(z', z_n) / w(z', z_n)$ has removable singularities at each $\zeta_j(z')$: the zero of $f$ at $\zeta_j(z')$ has multiplicity at least equal to that of $w$ (by construction), so the quotient extends holomorphically and is nonzero (if $f$ vanished to higher order, there would be more than $k$ zeros counted with multiplicity, contradicting [the argument principle](/theorems/356) count).
To confirm that $u$ is jointly holomorphic (not just separately), we use a Cauchy-type integral representation. The one-variable Cauchy formula applied to the [holomorphic function](/page/Holomorphic%20Function) $z_n \mapsto u(z', z_n)$ gives the contour integral representation above. Since $w(z', \zeta) \neq 0$ on $|\zeta| = r$ (all $k$ roots of $w$ in $z_n$ lie strictly inside the circle, as they are the zeros $\zeta_j(z')$ which satisfy $|\zeta_j(z')| < r$), the integrand is well-defined and continuous. Holomorphicity in $z'$ follows from differentiation under the integral sign, exactly as in the proof of the [Cauchy Integral Formula on Polydiscs](/theorems/3398).
[/guided]
[/step]
[step:Prove uniqueness of the factorisation]
Suppose $f = u_1 w_1 = u_2 w_2$ are two such factorisations, with $u_1, u_2$ units and $w_1, w_2$ Weierstrass polynomials of degree $k$ in $z_n$. Then $u_1 w_1 = u_2 w_2$, so $w_1 = (u_1^{-1} u_2) w_2$. For each fixed $z'$ near $0$, the function $z_n \mapsto w_1(z', z_n)$ is a monic polynomial of degree $k$ whose zeros are the zeros of $z_n \mapsto f(z', z_n)$ inside $|z_n| < r$ (since $u_1$ is nonvanishing). The same holds for $w_2$. Two monic polynomials of the same degree with the same roots (counted with multiplicity) are identical, so $w_1(z', \cdot) = w_2(z', \cdot)$ as polynomials for each fixed $z'$. Since this holds for all $|z'| < \delta$, we have $w_1 = w_2$, and consequently $u_1 = f/w_1 = f/w_2 = u_2$.
[guided]
The uniqueness argument is purely algebraic at the level of one-variable polynomials. For each fixed $z'$, both $w_1(z', z_n)$ and $w_2(z', z_n)$ are monic polynomials of degree $k$ in $z_n$. Since $u_1$ and $u_2$ are nowhere-vanishing, the zeros of $w_1(z', \cdot)$ are exactly the zeros of $f(z', \cdot)$ in $|z_n| < r$, and likewise for $w_2(z', \cdot)$. A monic polynomial is uniquely determined by its roots (with multiplicity), so $w_1(z', \cdot) = w_2(z', \cdot)$ for every fixed $z'$. Comparing coefficients, $c_j^{(1)}(z') = c_j^{(2)}(z')$ for all $j$ and all $|z'| < \delta$, giving $w_1 = w_2$ identically. Dividing $f = u_1 w_1 = u_2 w_1$ by $w_1$ (which is permissible since $u = f/w$ is well-defined), $u_1 = u_2$.
[/guided]
[/step]