---

Step * of Lemma mcopower_umap_comm_tri_a

∀s:DSet. ∀g:AbMon. ∀c:MCopower(s;g). ∀h:AbMon. ∀f:|s| ⟶ MonHom(g,h). ∀a:|g|. ∀j:|s|.
  ((f j a) = (c.umap h f (c.inj j a)) ∈ |h|)
BY
{ ((RepD) THENA Auto) }

1
1. s : DSet
2. g : AbMon
3. c : MCopower(s;g)
4. h : AbMon
5. f : |s| ⟶ MonHom(g,h)
6. a : |g|
7. j : |s|
⊢ (f j a) = (c.umap h f (c.inj j a)) ∈ |h|

---

Latex:

---

Latex:
\mforall{}s:DSet.  \mforall{}g:AbMon.  \mforall{}c:MCopower(s;g).  \mforall{}h:AbMon.  \mforall{}f:|s|  {}\mrightarrow{}  MonHom(g,h).  \mforall{}a:|g|.  \mforall{}j:|s|.
    ((f  j  a)  =  (c.umap  h  f  (c.inj  j  a)))


By

---

Latex:
((RepD)  THENA  Auto)

---

Home Index