The Souslin operation preserves Lebesgue measurability

For any sequence of measurable sets, disjointize it by removing preceding finite unions; the disjoint pieces are measurable and contained in the original sets. Countable additivity in F4 and monotonicity then give countable subadditivity. In particular a countable union of null measurable sets is null, and every subset of it is measurable and null by completeness F4. These uses are licensed by A1.

Put $Q_j=(-j,j{]}^d$ for positive integers j and $E_j=E\cap Q_j$. These boxes cover ${\mathbb{R}}^d$ and have finite measure $(2j{)}^d$ by F4. By F3 and A1 choose measurable $G_j\supseteq E_j$ with $\lambda (G_j)={\lambda }^{\ast }(E_j)$; the value is finite by containment of E_j in Q_j and monotonicity. Set $H_j=G_j\cap Q_j$. Then $E_j\subseteq H_j\subseteq G_j$ implies $\lambda (H_j)={\lambda }^{\ast }(E_j)$. If D is measurable and contains E, then $E_j\subseteq H_j\cap D$ implies $\lambda (H_j\cap D)\ge {\lambda }^{\ast }(E_j)=\lambda (H_j)$. Equality follows by the reverse monotonicity. F6's splitting of the finite-measure H_j at D gives $\lambda (H_j\setminus D)=0$. Thus $H={\bigcup }_j{H}_j$ is measurable, contains E, and $H\setminus D$ is null by step 1.1. No subtraction of infinite quantities occurred.

Normalize the measurable scheme $(A_s)$ using F1 and finite intersection closure from F4. Set $E_s={\bigcup }_{f\supseteq s}{\bigcap }_n{A}_{f\upharpoonright n}$, so $E_s\subseteq A_s$ and $E_s={\bigcup }_k{E}_{s^{⌢}k}$. Step 2.1 and A1 select measurable envelopes H_s. Put $B_s=A_s\cap {\bigcap }_{t\subseteq s}{H}_t$. These are measurable, decreasing, contain E_s, and are contained in H_s, so retain its envelope property. The measurable set ${\bigcup }_k{B}_{s^{⌢}k}$ contains E_s; hence $C_s=B_s\setminus {\bigcup }_k{B}_{s^{⌢}k}$ is null. The union C of these defects over all finite words is null by step 1.1.

For $x\in B_{\mathrm{\varnothing }}\setminus C$ the exclusion of each defect lets us recursively choose the least child index retaining membership in B. The resulting branch f has $x\in A_{f\upharpoonright n}$ for all n, so $x\in \mathsf{S}(A)$. Conversely $\mathsf{S}(A)=E_{\mathrm{\varnothing }}\subseteq B_{\mathrm{\varnothing }}$. Their difference is therefore a subset of null C. Completeness F4 proves $\mathsf{S}(A)$ measurable, including schemes with empty root. Finally F2 with A1 represents analytic sets by closed schemes, whose entries are measurable by F5 with A1; the proved preservation applies. QED.