If $h$ is from $\cal
S_B$, then we proceed by induction on the complexity of $h$, by using the Frobenius equations and the equations $(\delta^\Diamond)$ and ($\delta^\Diamond$ [*nat*]{}) of Section 2. Note that if $h$ is from $\cal S_B$, then $Jh$ can be neither $\varepsilon^\Box_k$ nor $\varepsilon^\Diamond_k$. We proceed analogously for $$J(\gamma_m\cirk h)=J(FFh\cirk \gamma_n).$$ To verify ${Jh_1=Jh_2}$ for ${h_1=h_2}$ a triangular equation, we use the equations $(\Box\beta)$, $(\Box\eta)$, $(\Diamond\beta)$ and $(\Diamond\eta)$ of Section 2.

There is an obvious functor $J_{\cal A}$ from $\cal S_A$ to *Frob* obtained by restricting $J$, and it is straightforward to verify by induction on the complexity of arrow terms that $I$ and $J_{\cal A}$ are inverse to each other. So the categories *Frob* and $\cal S_A$ are isomorphic.$\dashv$

From this proposition and from the Proposition of the preceding section we can conclude that *Frob* is isomorphic to the category $\cal A$ of the bijunction freely generated by a single object on the $\cal A$ side, but the isomorphism we have established in this section is more interesting for us, as it will become clear in the next section.

Coherence for Frobenius monads
==============================

Out of the category $\cal S$ of the free self-adjunction of Section 