The Conway polynomial

Form the coefficientwise formal expression $C_D(z)={\sum }_{j\ge 0}{c}_j(D)z^j$ from [F1]. It is a diagram invariant, has value $1$ on an unknot, and satisfies $C_{D_{+}}-C_{D_{-}}=z{C}_{D_0}$ coefficientwise. A local positive and negative curl on any component of the $r$-component unlink are both that unlink; the oriented smoothing is the $(r+1)$-component unlink. Thus $c_j(U_r)-c_j(U_r)=c_{j-1}(U_{r+1})$ for every $j\ge 1$. All coefficients of $U_{r+1}$ vanish. Therefore the unlink values of the formal expression are $1$ for one component and $0$ for more than one. This is also the forced unlink value for ANY polynomial-valued invariant satisfying the Definition.

Here is the finite argument that the expression is actually in $\mathbb{Z}[z]$. In a diagram choose finitely many component basepoints and an order. Call a crossing bad when its first encounter in this traversal is the underpass. If none is bad, the first component passes over every later component and has a descending self-diagram. Pull its successive arcs above everything they first encounter to isolate a round circle; repeat for the remaining components. Thus a descending diagram is an unlink. At a bad crossing the skein relation writes its value as the value of the switched diagram, plus or minus $z$ times its oriented smoothing. The switched diagram has one fewer bad crossing and the same number $N$ of crossings; the smoothing has $N-1$ crossings. Reset the finite component data on a smoothing if necessary. The nonnegative integer $N(N+1)\mathrm{/}2+b$, with $b$ the number of bad crossings, decreases in each branch. Hence this is a FINITE resolution tree. Its leaves have values $0$ or $1$ by step1.1. Working back through the tree uses only integer addition/subtraction and multiplication by $z$, so $C_D\in \mathbb{Z}[z]$. In fact every branch has at most $N$ smoothing operations, giving degree at most $N$. This proves finiteness and integrality without assuming an integer-valued formal sequence theorem or making an infinite selection.

Apply the SAME finite tree to any two polynomial-valued invariants satisfying the stated normalization and skein relation. Their unlink leaves agree by step1.1, and each internal skein relation then forces agreement. Their values agree on every diagram. Existence follows from [F1], step 2.1 and the ambient-link interpretation [F2], and this argument proves uniqueness. The separately fixed empty-link extension is unique as well, since its prescribed value is zero. Consequently the separate existence/uniqueness obligation mentioned in the Definition is now discharged: the resulting actual link invariant is exactly $\mathrm{\nabla }$, and its coefficient $[z^k]{\mathrm{\nabla }}_L$ is well-defined for every $k$. The finite local arguments use no choice axiom; the external constructive coefficient/diagram inputs are explicitly distinguished from them.