---

Step * of Lemma mcopower_umap_wf

∀s:DSet. ∀g:AbMon. ∀m:mcopower_sig{i:l}(s;g).  (m.umap ∈ h:AbMon ⟶ (|s| ⟶ |g| ⟶ |h|) ⟶ |m.mon| ⟶ |h|)
BY
{ ModulePiTac 3 ``mcopower_mon mcopower_inj mcopower_umap`` }

---

Latex:

---

Latex:
\mforall{}s:DSet.  \mforall{}g:AbMon.  \mforall{}m:mcopower\_sig\{i:l\}(s;g).
    (m.umap  \mmember{}  h:AbMon  {}\mrightarrow{}  (|s|  {}\mrightarrow{}  |g|  {}\mrightarrow{}  |h|)  {}\mrightarrow{}  |m.mon|  {}\mrightarrow{}  |h|)


By

---

Latex:
ModulePiTac  3  ``mcopower\_mon  mcopower\_inj  mcopower\_umap``

---

Home Index