morphisms. Obviously, $M_\iota$ commutes with the forgetful functors $U_\mathbb S: {{\text{\tt{Set}}}^{T_\mathbb S}} \to {{\text{\tt{Set}}}}$ and $U_\mathbb E: {{\text{\tt{Set}}}^{T_\mathbb E}} \to {{\text{\tt{Set}}}}$, i.e., $U_\mathbb S {\mathrel{\circ}}M_\iota = U_\mathbb E$.

Let $(X, \alpha_X) \in {{\text{\tt{Set}}}^{{T_{\mathbb{S}}}}}$ and $(Y, \alpha_Y) \in {{\text{\tt{Set}}}^{{T_{\mathbb{E}}}}}$ where ${T_{\mathbb{S}}}$ and ${T_{\mathbb{E}}}$ are monads with ${T_{\mathbb{S}}}\le {T_{\mathbb{E}}}$ via $\iota\colon {T_{\mathbb{S}}}\Rightarrow {T_{\mathbb{E}}}$. A ${{\text{\tt{Set}}}}$-arrow $h\colon X \to Y$ is a ${T_{\mathbb{S}}}\le {T_{\mathbb{E}}}$-homomorphism from $(X,\alpha_X)$ to $(Y,\alpha_Y)$ if and only if the following diagram commutes (in ${{\text{\tt{Set}}}}$) $$\xymatrix@R=0.7em{
    {T_{\mathbb{S}}}X \ar[rr]^{\iota h} \ar[d]_{\alpha_X}&& {T_{\mathbb{E}}}Y \ar[d]^{\alpha_Y}\\
    X \ar[rr]^{h}&& Y
    }$$ where $\iota h$ denotes the map $\iota h \stackrel{\text{def}}{=} {T_{\mathbb{E}}}h{\mathrel{\circ}}\iota_X \stackrel{\text{nat.}}{=} \iota_Y {\mathrel{\circ}}{T_{\mathbb{S}}}h$. In other words, a ${T_{\mathbb{S}}}\le {T_{\mathbb{E}}}$-homomorphism from $(X,\alpha_X)$ to $(Y,\alpha_Y)$ is a morphism in ${{\text{\tt{Set}}}^{T_\mathbb S}}$ from $(X,\alpha_X)$ to $M(Y,\alpha_Y)$.

Now we can formulate the extension lemma.

\[prop:ext-lem\] For every ${{\ensuremath{F_{\,{\mathbb{S}}}}}}$-coalgebra ${T_{\mathbb{S}}}B \stackrel{c}{\to} {{\ensuremath{F_{\,{\mathbb{S}}}}}}({T_{\mathbb{S}}}B)$ with free finitely generated carrier ${T_{\mathbb{S}}}B$ for a finite set $B$, there exists an ${{\ensuremath{F_{\,{\mathbb{E}}}}}}$-coalgebra ${T_{\mathbb{E}}}B \stackrel{\tilde c}{\to} {{\ensuremath{F_{\,{\mathbb{E}}}}}}({T_{\mathbb{E}}}B)$ with free finitely generated carrier ${T_{\mathbb{E}}}B$ such that $$\xymatrix@R=0.7em{
            {T_{\mathbb{S}}}B \ar[rr]^{\iota_B} \ar[d]_{c}&& {T_{\mathbb{E}}}B \ar[d]^{\tilde c}\\
            {{\ensuremath{F_{\,{\mathbb{S}}}}}}({T_{\mathbb{S}}}B) \ar[rr]^{\iota_1 \times (\iota_B)^A}&& {{\ensuremath{F_{\,{\mathbb{E}}}}}}({T_{\mathbb{E}}}B)
        }$$ where the horizontal arrows ($\iota_B$ and $\iota_1 \times \iota_B^A$) are ${T_{\mathbb{S}}}\le {T_{\mathbb{E}}}$-homomorphisms, and moreover they both amount to inclusion.

*Step 2. The basic diagram:*  Let $n_1,n_2\in\mathbb N$, 