The countable-product cylinder premeasure is countably additive

Index the given coordinates by $0,1,\dots$. Each coordinate space is nonempty since its measure has total mass one. Countable choice in [F4] supplies a point of their product, and [F5] gives the finitely additive cylinder law. Finite product laws are consistent: projecting away a factor preserves the rectangle values because that factor has mass one, and uniqueness in [F1] gives equality on the finite product sigma-algebra. This also justifies regrouping any finite block into two factors.

For a cylinder $C$ and a prefix $p=(x_0,\dots ,x_{m-1})$, define $h_C(p)$ using only finite products: represent $C$ on coordinates $0,\dots ,k-1$ with $k\ge m$, fix the prefix in its measurable base, and measure the remaining section with ${⨂}_{m\le j<k}{\mu }_j$. For $k=m$ this is the indicator of membership in the base. Enlarging $k$ leaves the value unchanged by the mass-one rectangle formula; two representations agree after enlargement, using the product point of step 1.1. Thus $h_C(p)$ is well-defined and lies in $[0,1]$. By choosing $k\ge m+1$, [F2] gives a measurable function $z\mapsto h_C(p,z)$ and $h_C(p)={\int }_{E_m}{h}_C(p,z)d{\mu }_m(z)\mathrm{.}$ Inclusion of cylinders gives pointwise inequality of these functions by finite-product monotonicity. No measure on an infinite tail is used.

Let $C_n\downarrow \mathrm{\varnothing }$ and suppose their masses do not tend to zero. Finite additivity makes the masses decreasing in $[0,1]$, so there is $\eta >0$ with ${\mu }_0(C_n)\ge \eta$ for all $n$. Call a prefix $p$ of length $m$ admissible if $h_{C_n}(p)\ge \eta \mathrm{/}{2}^m$ for every $n$; the empty prefix is admissible. Given one, put $t=\eta \mathrm{/}{2}^{m+1}$ and $D_n=\{z\in E_m:h_{C_n}(p,z)\ge t\}\mathrm{.}$ These sets are measurable and decrease. Step 2.1 and the bound $0\le h_{C_n}\le 1$ yield $2t\le h_{C_n}(p)\le {\mu }_m(D_n)+t{\mu }_m(E_m\setminus D_n)\le {\mu }_m(D_n)+t\mathrm{.}$ Hence ${\mu }_m(D_n)\ge t$, and [F3] implies ${\mu }_m({\bigcap }_n{D}_n)\ge t>0$. Any point in this intersection extends $p$ to an admissible prefix.

The admissible finite prefixes form a nonempty set. Relate a prefix to its admissible one-coordinate extensions; step 3.1 proves this relation is entire. Dependent choice in [F6], starting at the empty prefix, gives a compatible chain, whose union is a point $x$ of the original coordinate product. For each $n$, choose a finite initial block determining $C_n$. Once that block is fixed, $h_{C_n}$ is its membership indicator; admissibility makes it positive, so $x\in C_n$. This contradicts the empty intersection. Thus ${\mu }_0(C_n)\to 0$. Using all original coordinates also handles cylinders with empty or finitely many active coordinates; there is no terminal-prefix exception.

If disjoint cylinders $A_j$ have union a cylinder $A$, then $R_N=A\setminus {\bigcup }_{j<N}{A}_j$ decreases to the empty set and remains in the cylinder algebra. Finite additivity gives ${\mu }_0(A)={\sum }_{j<N}{\mu }_0(A_j)+{\mu }_0(R_N)\mathrm{.}$ Step 4.1 sends the remainder to zero, proving countable additivity for every such union. Hence ${\mu }_0$ is a premeasure.