[proofplan]
Use the recursive order of the original structural causal model to construct the intervened endogenous variables one at a time. At an intervened variable, insert the assigned value from $x_I$; at a non-intervened variable, evaluate the original measurable structural function using the exogenous realization and the endogenous values already constructed. Induction gives existence, uniqueness, and measurability of the intervened solution map. The interventional law is then the pushforward of $P_U$ under this map, and the law of any subcollection is obtained by coordinate projection.
[/proofplan]
[step:Construct the intervened endogenous solution along the recursive order]
Write $x_I=(x_j)_{X_j\in I}$, where $x_j\in\mathcal X_{X_j}$ denotes the assigned value for the intervened variable $X_j$. Define maps
\begin{align*}
F_j^{I,x_I}:\mathcal X_U\to \mathcal X_{X_j}
\end{align*}
recursively as follows. If $X_j\in I$, set
\begin{align*}
F_j^{I,x_I}(u)=x_j.
\end{align*}
If $X_j\notin I$, set
\begin{align*}
F_j^{I,x_I}(u)=f_j(u,F_1^{I,x_I}(u),\dots,F_{j-1}^{I,x_I}(u)).
\end{align*}
This construction is legitimate because the recursive order ensures that $f_j$ only uses exogenous variables and endogenous variables earlier than $X_j$.
[guided]
We build the post-intervention endogenous values in the same order in which the recursive SCM is solved before intervention. The assigned value $x_I$ is an element of the product state space over the intervened variables, so for each $X_j\in I$ there is a corresponding value $x_j\in\mathcal X_{X_j}$.
For each index $j\in\{1,\dots,n\}$, define a map
\begin{align*}
F_j^{I,x_I}:\mathcal X_U\to \mathcal X_{X_j}.
\end{align*}
This map sends an exogenous realization $u\in\mathcal X_U$ to the value of the endogenous variable $X_j$ after the intervention $do(I=x_I)$.
There are two cases. If $X_j$ is intervened on, the structural equation for $X_j$ is replaced by the constant assignment:
\begin{align*}
F_j^{I,x_I}(u)=x_j.
\end{align*}
If $X_j$ is not intervened on, we keep its original structural equation and evaluate it using the values already constructed:
\begin{align*}
F_j^{I,x_I}(u)=f_j(u,F_1^{I,x_I}(u),\dots,F_{j-1}^{I,x_I}(u)).
\end{align*}
The recursive order is exactly what makes this definition well-founded: when we define $F_j^{I,x_I}$, all maps $F_1^{I,x_I},\dots,F_{j-1}^{I,x_I}$ have already been defined, and no later endogenous value is needed.
[/guided]
[/step]
[step:Prove existence and uniqueness of the intervened solution]
Define the product measurable space
\begin{align*}
(\mathcal X_V,\mathcal E_V):=\left(\prod_{j=1}^n\mathcal X_{X_j},\bigotimes_{j=1}^n\mathcal E_{X_j}\right).
\end{align*}
Define the intervened solution map $F_M^{I,x_I}:\mathcal X_U\to\mathcal X_V$ by the rule
\begin{align*}
F_M^{I,x_I}(u)=(F_1^{I,x_I}(u),\dots,F_n^{I,x_I}(u))
\end{align*}
for each $u\in\mathcal X_U$. The preceding recursive construction gives an endogenous assignment satisfying the intervened structural equations, so existence holds for every $u\in\mathcal X_U$.
To prove uniqueness, fix $u\in\mathcal X_U$ and let
\begin{align*}
z=(z_1,\dots,z_n)\in\prod_{j=1}^n\mathcal X_{X_j}
\end{align*}
be any solution of the intervened structural equations at $u$. We prove by induction on $j$ that $z_j=F_j^{I,x_I}(u)$. If $X_j\in I$, then the intervened equation imposes $z_j=x_j=F_j^{I,x_I}(u)$. If $X_j\notin I$, then the intervened equation gives
\begin{align*}
z_j=f_j(u,z_1,\dots,z_{j-1}).
\end{align*}
By the induction hypothesis, $z_i=F_i^{I,x_I}(u)$ for each $i<j$, hence
\begin{align*}
z_j=f_j(u,F_1^{I,x_I}(u),\dots,F_{j-1}^{I,x_I}(u))=F_j^{I,x_I}(u).
\end{align*}
Thus $z=F_M^{I,x_I}(u)$. Since $u$ was arbitrary, the intervened model has a unique endogenous solution for every exogenous realization, and therefore for $P_U$-almost every exogenous realization.
[/step]
[step:Verify measurability of the intervened solution map]
For each $j$, the map $F_j^{I,x_I}$ is measurable. Indeed, if $X_j\in I$, then $F_j^{I,x_I}$ is a constant map into the measurable space $(\mathcal X_{X_j},\mathcal E_{X_j})$. If $X_j\notin I$, assume inductively that $F_i^{I,x_I}$ is measurable for every $i<j$. The map
\begin{align*}
G_j:\mathcal X_U\to \mathcal X_U\times \prod_{i<j}\mathcal X_{X_i}
\end{align*}
defined by
\begin{align*}
G_j(u)=(u,F_1^{I,x_I}(u),\dots,F_{j-1}^{I,x_I}(u))
\end{align*}
is measurable by the defining property of product measurable spaces. Since $f_j$ is measurable, the composition
\begin{align*}
F_j^{I,x_I}=f_j\circ G_j
\end{align*}
is measurable. By finite induction, every coordinate map $F_j^{I,x_I}$ is measurable, and therefore
\begin{align*}
F_M^{I,x_I}:\mathcal X_U\to \prod_{j=1}^n\mathcal X_{X_j}
\end{align*}
is measurable.
[/step]
[step:Define the interventional distribution as a pushforward measure]
Because $F_M^{I,x_I}$ is measurable, the pushforward measure
\begin{align*}
P_M(V\in B\mid do(I=x_I)):=P_U((F_M^{I,x_I})^{-1}(B))
\end{align*}
is well-defined for every measurable set
\begin{align*}
B\in \bigotimes_{j=1}^n\mathcal E_{X_j}.
\end{align*}
Equivalently,
\begin{align*}
P_M(V\in \cdot\mid do(I=x_I))=P_U\circ (F_M^{I,x_I})^{-1}.
\end{align*}
This is a probability measure on $\prod_{j=1}^n\mathcal X_{X_j}$, since it is the pushforward of the probability measure $P_U$ under the measurable map $F_M^{I,x_I}$.
[/step]
[step:Obtain subcollection laws by coordinate projection]
Let $Y\subset V$ be a subcollection of endogenous variables, and let
\begin{align*}
\pi_Y:\prod_{X_j\in V}\mathcal X_{X_j}\to \prod_{X_j\in Y}\mathcal X_{X_j}
\end{align*}
be the coordinate projection. The projection $\pi_Y$ is measurable with respect to the corresponding product $\sigma$-algebras. Therefore the interventional distribution of $Y$ is the pushforward marginal
\begin{align*}
P_M(Y\in C\mid do(I=x_I)):=P_M(V\in \pi_Y^{-1}(C)\mid do(I=x_I))
\end{align*}
for every measurable set
\begin{align*}
C\in \bigotimes_{X_j\in Y}\mathcal E_{X_j}.
\end{align*}
Equivalently,
\begin{align*}
P_M(Y\in \cdot\mid do(I=x_I))=P_M(V\in \cdot\mid do(I=x_I))\circ \pi_Y^{-1}.
\end{align*}
Thus the law of every endogenous subcollection is precisely the marginal of the full interventional law, completing the proof.
[/step]
