---

Step * of Lemma mcopower_properties

∀s:DSet. ∀g:AbMon. ∀c:MCopower(s;g).
  ((∀j:|s|. IsMonHom{g,c.mon}(c.inj j))
  ∧ (∀h:AbMon. ∀f:|s| ⟶ MonHom(g,h).
       (c.umap h f) = !v:|c.mon| ⟶ |h|. (IsMonHom{c.mon,h}(v) ∧ (∀j:|s|. ((f j) = (v o (c.inj j)) ∈ (|g| ⟶ |h|))))))
BY
{ (Auto THEN DVar `c' THEN Auto THEN (Unhide THEN Auto THEN BackThruSomeHyp)⋅) }

---

Latex:

---

Latex:
\mforall{}s:DSet.  \mforall{}g:AbMon.  \mforall{}c:MCopower(s;g).
    ((\mforall{}j:|s|.  IsMonHom\{g,c.mon\}(c.inj  j))
    \mwedge{}  (\mforall{}h:AbMon.  \mforall{}f:|s|  {}\mrightarrow{}  MonHom(g,h).
              (c.umap  h  f)  =  !v:|c.mon|  {}\mrightarrow{}  |h|
                                                (IsMonHom\{c.mon,h\}(v)  \mwedge{}  (\mforall{}j:|s|.  ((f  j)  =  (v  o  (c.inj  j)))))))


By

---

Latex:
(Auto  THEN  DVar  `c'  THEN  Auto  THEN  (Unhide  THEN  Auto  THEN  BackThruSomeHyp)\mcdot{})

---

Home Index