The countable-product cylinder premeasure is countably additive

Every coordinate space is nonempty because it carries a probability measure. By [F4], the coordinate product is therefore nonempty, so the finitely additive cylinder law is well-defined. Let $C_n\downarrow \mathrm{\varnothing }$ be cylinders and suppose that ${\mu }_0(C_n)\ge \eta >0$ for every $n$. By [F5], enumerate the countable union of their finite supports. After enlarging supports, take $C_n$ to be determined by the first $k_n$ active coordinates, with $(k_n)$ nondecreasing. Recursively regarding each finite product as a two-factor product, [F2] expresses each cylinder mass as the integral of its measurable next-coordinate section-mass function.

The finite-stage section argument recursively maintains the following invariant after $m$ coordinates have been chosen: every remaining $C_n$-section has tail-cylinder mass at least $\eta \mathrm{/}{2}^m$. For a prefix with this invariant, let $D_n$ be the measurable set of possible next coordinates whose further section has mass at least $\eta \mathrm{/}{2}^{m+1}$. The $D_n$ decrease with $n$. The section formula and the bound by $1$ give the next-coordinate measure of $D_n$ at least $\eta \mathrm{/}{2}^{m+1}$; [F3] therefore makes ${\bigcap }_n{D}_n$ nonempty. Every choice from this intersection extends the prefix and preserves the invariant.

By [F6], make the recursively compatible selections from step 2.1. For each $n$, once the first $k_n$ active coordinates have been selected, they lie in the finite base of $C_n$ because its remaining section has positive mass. Fill any inactive coordinates with the product point supplied by [F4]. The resulting point lies in every $C_n$, contradicting ${\bigcap }_n{C}_n=\mathrm{\varnothing }$. Thus ${\mu }_0(C_n)\downarrow 0$.

Finite additivity plus continuity at the empty set gives countable additivity whenever a disjoint union remains a cylinder: apply it to the decreasing remainders. Hence ${\mu }_0$ is a premeasure.