S}}}}}(Y_1\times Y_2)$.

Using this, yields $$\begin{aligned}
        d\big(Z\cap(X_1\times X_2)\big)\subseteq &\, 
        {{\ensuremath{F_{\,{\mathbb E}}}}}Z\cap({{\ensuremath{F_{\,{\mathbb E}}}}}\pi_1)^{-1}\big({{\ensuremath{F_{\,{\mathbb S}}}}}X_1)
        \cap({{\ensuremath{F_{\,{\mathbb E}}}}}\pi_2)^{-1}\big({{\ensuremath{F_{\,{\mathbb S}}}}}X_2)
        \\
        = &\, {{\ensuremath{F_{\,{\mathbb E}}}}}Z\cap{{\ensuremath{F_{\,{\mathbb S}}}}}(X_1\times X_2)={{\ensuremath{F_{\,{\mathbb S}}}}}\big(Z\cap(X_1\times X_2)\big)
        .
    \end{aligned}$$ This shows that $Z\cap(X_1\times X_2)$ becomes an ${{\ensuremath{F_{\,{\mathbb S}}}}}$-coalgebra with the restriction $d|_{Z\cap(X_1\times X_2)}$. Again referring to the basic diagram, we have the following zig-zag in [[Coalg]{}([$F_{\mathbb S}$]{})]{} (to shorten notation, denote the restrictions of $d,\pi_1,\pi_2$ to $Z\cap(X_1\times X_2)$ again as $d,\pi_1,\pi_2$): $$\label{4}
        \xymatrix@C=40pt{
        (X_1,c_1) & \big(Z\cap(X_1\times X_2),d\big) 
            \ar[l]_{\pi_1\mkern50mu} \ar[r]^{\mkern60mu\pi_2} 
        & (X_2,c_2)
        }$$ This zig-zag relates $x_1$ with $x_2$ since $(x_1,x_2)\in Z\cap(X_1\times X_2)$.

*Step 3. The reduction lemma:*  In view of the zig-zag , the proof of Theorem \[CubProp\] can be completed by showing that $Z\cap(X_1\times X_2)$ is finitely generated as an algebra in . Since $Z$ is a submodule of the finitely generated module $\mathbb E^{n_1}\times\mathbb E^{n_2}$ over the Noetherian ring $\mathbb E$, it is finitely generated as an $\mathbb E$-module. The task thus is to show that being finitely generated is preserved when reducing scalars.

This is done by what we call the *reduction lemma*. Contrasting the extension lemma, the reduction lemma is not a general categorical fact, and requires specific proof in each situation.

\[RedLem\] Let $n_1,n_2\in\mathbb N$, let $B_j$ 