the restrictions of $d_1$ and $d_2$ to $Z$ coincide and turn $Z$ into an ${{\ensuremath{F_{\,{\mathbb S}}}}}$-coalgebra.

\[Prod\] Let $Z$ be the subsemimodule of $\mathbb S^{n_1}\times\mathbb S^{n_2}$ generated by the pairs $({{c_1}_{w}}(x_1),{{c_2}_{w}}(x_2))$ for $w \in A^*$. Then $d_1|_Z=d_2|_Z$ and $d_j(Z)\subseteq{{\ensuremath{F_{\,{\mathbb S}}}}}(Z)$.

The significance of Lemma \[Prod\] in the present context is that it leads to the diagram (we denote $d=d_j|_Z$) $$\xymatrix@C=15pt@R=35pt@M=7pt{
    \mathbb S^{n_1} \ar[d]_{c_1}
    && Z \ar[ll]_{\pi_1} \ar[rr]^{\pi_2} \ar[d]^d 
        \save[]+<3pt,10pt>*\txt{\begin{rotate}{90}$\subseteq$\end{rotate}}\restore
        \save[]+<2pt,27pt>*\txt{$\mathbb S^{n_1}\!\!\times\mathbb S^{n_2}$}\restore
    && \mathbb S^{n_2} \ar[d]_{c_2}
    \\
    {{\ensuremath{F_{\,{\mathbb S}}}}}\mathbb S^{n_1} 
    && {{\ensuremath{F_{\,{\mathbb S}}}}}Z \ar[ll]_{{{\ensuremath{F_{\,{\mathbb S}}}}}\pi_1} \ar[rr]^{{{\ensuremath{F_{\,{\mathbb S}}}}}\pi_2}
        \save[]+<-3pt,-10pt>*\txt{\begin{rotate}{-90}$\subseteq$\end{rotate}}\restore
        \save[]+<2pt,-29pt>*\txt{$\mathbb S\!\!\times(\mathbb S^{n_1}\!\!\times\mathbb S^{n_2})^A$}\restore
    && {{\ensuremath{F_{\,{\mathbb S}}}}}\mathbb S^{n_2}
}$$ In other words, it leads to the zig-zag in [[Coalg]{}([${{\ensuremath{F_{\,{\mathbb S}}}}}$]{})]{} $$\label{ZZ}
\xymatrix@C=40pt{
    (\mathbb S^{n_1},c_1) & (Z,d) \ar[l]_{\mkern20mu\pi_1} \ar[r]^{\pi_2\mkern20mu} 
    & (\mathbb S^{n_2},c_2) 
}$$ This zig-zag relates $x_1$ with $x_2$ since $(x_1,x_2)\in Z$. If it can be shown that $Z$ is always finitely generated, it will follow that ${{\ensuremath{F_{\,{\mathbb S}}}}}$ is proper.

Let $\mathbb S$ be a Noetherian semiring, i.e., a semiring such that every $\mathbb S$-subsemimodule of some finitely generated $\mathbb S$-semimodule is itself finitely generated. Then $Z$ is, as an $\mathbb S$-subsemimodule of $\mathbb S^{n_1}\times\mathbb S^{n_2}$ finitely generated. Hence, we reobtain the result [@esik.maletti:2010 Theorem 4.2] of Esik and Maletti.

\[Noetherian\] Every 