---

Step * of Lemma free_abmon_unique

∀S:DSet. ∀M,N:FAbMon(S).  ∃f:MonHom(M.mon,N.mon). ∃g:MonHom(N.mon,M.mon). InvFuns(|M.mon|;|N.mon|;f;g)
BY
{ ((UnivCD) THENA Auto) }

1
1. S : DSet
2. M : FAbMon(S)
3. N : FAbMon(S)
⊢ ∃f:MonHom(M.mon,N.mon). ∃g:MonHom(N.mon,M.mon). InvFuns(|M.mon|;|N.mon|;f;g)

---

Latex:

---

Latex:
\mforall{}S:DSet.  \mforall{}M,N:FAbMon(S).
    \mexists{}f:MonHom(M.mon,N.mon).  \mexists{}g:MonHom(N.mon,M.mon).  InvFuns(|M.mon|;|N.mon|;f;g)


By

---

Latex:
((UnivCD)  THENA  Auto)

---

Home Index