---

Step * of Lemma oal_umap_char_a

∀s:LOSet. ∀g:AbDMon. ∀h:AbMon. ∀f:|s| ⟶ MonHom(g,h).
  umap(h,f) = !v:|oal(s;g)| ⟶ |h|
                (IsMonHom{oal_mon(s;g),h}(v) ∧ (∀j:|s|. ((f j) = (v o (λw.inj(j,w))) ∈ (|g| ⟶ |h|))))
BY
{ Unfold `oal_umap` 0 THEN Lemma `oal_umap_char` }

---

Latex:

---

Latex:
\mforall{}s:LOSet.  \mforall{}g:AbDMon.  \mforall{}h:AbMon.  \mforall{}f:|s|  {}\mrightarrow{}  MonHom(g,h).
    umap(h,f)  =  !v:|oal(s;g)|  {}\mrightarrow{}  |h|
                                (IsMonHom\{oal\_mon(s;g),h\}(v)  \mwedge{}  (\mforall{}j:|s|.  ((f  j)  =  (v  o  (\mlambda{}w.inj(j,w))))))


By

---

Latex:
Unfold  `oal\_umap`  0  THEN  Lemma  `oal\_umap\_char`

---

Home Index