---

Step * of Lemma free_abmon_inj_wf

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

---

Latex:

---

Latex:
\mforall{}S:DSet.  \mforall{}f:FAbMon(S).    (f.inj  \mmember{}  |S|  {}\mrightarrow{}  |f.mon|)


By

---

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

---

Home Index