Global length of a plane complete intersection equals the degree product

Given: AC, an algebraically closed field $k$, plane projective curves $C=V(F)$, $D=V(G)$ of degrees $d,e\ge 1$ with no common component, and $X=\mathrm{Proj}(k[x_0,x_1,x_2]\mathrm{/}(F,G))$.

$F$ and $G$ are nonzero homogeneous forms of positive degrees $d,e$ and have no common nonconstant factor: a common nonconstant factor would have an irreducible factor $h$, and then $V(h)$ would be a component of both $C$ and $D$ Plane projective curves and their components.

For nonzero plane forms of positive degrees with no common nonconstant factor, $X$ is nonempty and finite, its charts are zero-dimensional, and its total length in the sense of Total length of a zero-dimensional projective scheme equals $de$: ${\mathrm{len}}_k(X)=de$ Two coprime projective plane forms meet in total length equal to their degree product. Equivalently ${\mathrm{len}}_k(X)={\sum }_{x\in X}{\mathrm{\ell }}_{{\mathcal{O}}_{X,x}}({\mathcal{O}}_{X,x})[\kappa (x):k]=de$ Algebraic Bezout formula as a sum of local scheme lengths.

For each $x\in X$ the residue field $\kappa (x)$ is a finite extension of $k$ The residue field at a point of an affine scheme, The degree $[K:F]={\dim }_{F}K$ of a finite field extension, and a finite extension of an algebraically closed field is trivial, i.e. $\kappa (x)=k$ A field is algebraically closed exactly when every nonconstant polynomial splits, equivalently when it has no nontrivial finite extension, An algebraically closed field: every nonconstant polynomial has a root in the field.

AC is assumed; it is used through the complete-intersection length theorem and the projective-scheme construction The Axiom of Choice. No further choice enters.