[proofplan]
The composite translation first applies $(-)^M$ and then applies $(-)^N$. Starting from a classical proof of $A$, the $M$-soundness hypothesis gives an intuitionistic proof of $A^M$, and the standard inclusion of intuitionistic derivability into classical derivability lets us regard $A^M$ as classically derivable. The $N$-soundness hypothesis can then be applied to the formula $A^M$, giving an intuitionistic proof of $(A^M)^N=A^{MN}$. Stability follows directly from the stability-of-range hypothesis for $(-)^N$, again applied to the formula $A^M$.
[/proofplan]
[step:Translate the classical proof through $(-)^M$]
Let $A \in \operatorname{Form}(\mathcal L)$ be a formula such that $\vdash_{\mathrm{CL}} A$. By the soundness hypothesis for the translation $(-)^M$, applied to the formula $A$, we obtain
\begin{align*}
\vdash_{\mathrm{IL}} A^M.
\end{align*}
[/step]
[step:Regard the translated theorem as classically derivable]
Since every intuitionistic proof is also a classical proof in the same formal language, the derivability statement $\vdash_{\mathrm{IL}} A^M$ implies
\begin{align*}
\vdash_{\mathrm{CL}} A^M.
\end{align*}
[guided]
At this point we have an intuitionistic proof of $A^M$, but the soundness hypothesis for $(-)^N$ has the form “if a formula is classically derivable, then its $N$-translation is intuitionistically derivable.” Therefore we need to place $A^M$ inside the antecedent of that hypothesis.
The standard inclusion of intuitionistic derivability into classical derivability says that for every formula $C \in \operatorname{Form}(\mathcal L)$,
\begin{align*}
\vdash_{\mathrm{IL}} C \implies \vdash_{\mathrm{CL}} C.
\end{align*}
We apply this inclusion to the specific formula $C:=A^M$. Since the previous step gave
\begin{align*}
\vdash_{\mathrm{IL}} A^M,
\end{align*}
we conclude
\begin{align*}
\vdash_{\mathrm{CL}} A^M.
\end{align*}
This is the bookkeeping point that makes the composition argument work: the output of the first translation becomes a valid input for the classical-to-intuitionistic soundness property of the second translation.
[/guided]
[/step]
[step:Apply the $N$ translation to the formula $A^M$]
Apply the soundness hypothesis for $(-)^N$ to the formula $B:=A^M$. The preceding step gives $\vdash_{\mathrm{CL}} B$, so the hypothesis yields
\begin{align*}
\vdash_{\mathrm{IL}} B^N.
\end{align*}
Substituting back $B=A^M$, this is
\begin{align*}
\vdash_{\mathrm{IL}} (A^M)^N.
\end{align*}
By the definition of the composite translation, $A^{MN}:=(A^M)^N$. Hence
\begin{align*}
\vdash_{\mathrm{IL}} A^{MN}.
\end{align*}
This proves that $\vdash_{\mathrm{CL}} A$ implies $\vdash_{\mathrm{IL}} A^{MN}$.
[/step]
[step:Use the stability of the $N$ translation range]
The stability hypothesis for $(-)^N$ states that for every formula $C \in \operatorname{Form}(\mathcal L)$,
\begin{align*}
\vdash_{\mathrm{IL}} \neg\neg C^N \to C^N.
\end{align*}
Apply this to the formula $C:=A^M$. We obtain
\begin{align*}
\vdash_{\mathrm{IL}} \neg\neg (A^M)^N \to (A^M)^N.
\end{align*}
Using again the definition $A^{MN}:=(A^M)^N$, this becomes
\begin{align*}
\vdash_{\mathrm{IL}} \neg\neg A^{MN} \to A^{MN}.
\end{align*}
Therefore $A^{MN}$ is intuitionistically stable. Combined with the previous step, this proves both asserted properties of the composite translation.
[/step]
