---

Step * of Lemma free_abmon_mon_wf

∀S:DSet. ∀f:FAbMon(S).  (f.mon ∈ AbMon)
BY
{ ModulePiTac 3 ``free_abmon_mon free_abmon_inj free_abmon_umap`` }

---

Latex:

---

Latex:
\mforall{}S:DSet.  \mforall{}f:FAbMon(S).    (f.mon  \mmember{}  AbMon)


By

---

Latex:
ModulePiTac  3  ``free\_abmon\_mon  free\_abmon\_inj  free\_abmon\_umap``

---

Home Index