---

Step * of Lemma free_abmon_umap_wf

∀S:DSet. ∀f:FAbMon(S).
  (f.umap ∈ mon':AbMon ⟶ f':(|S| ⟶ |mon'|) ⟶ {!g:MonHom(f.mon,mon') | (g o f.inj) = f' ∈ (|S| ⟶ |mon'|)})
BY
{ ModulePiTac 3 ``free_abmon_mon free_abmon_inj free_abmon_umap`` }

---

Latex:

---

Latex:
\mforall{}S:DSet.  \mforall{}f:FAbMon(S).
    (f.umap  \mmember{}  mon':AbMon  {}\mrightarrow{}  f':(|S|  {}\mrightarrow{}  |mon'|)  {}\mrightarrow{}  \{!g:MonHom(f.mon,mon')  |  (g  o  f.inj)  =  f'\})


By

---

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

---

Home Index