---

Step * 1 of Lemma mcopower_umap_comm_tri_a


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|
BY
{ RWH add_composeC 0 
THENM ((RWO "mcopower_umap_comm_tri<" 0) THEN Auto) }

---

Latex:

---

Latex:

1.  s  :  DSet
2.  g  :  AbMon
3.  c  :  MCopower(s;g)
4.  h  :  AbMon
5.  f  :  |s|  {}\mrightarrow{}  MonHom(g,h)
6.  a  :  |g|
7.  j  :  |s|
\mvdash{}  (f  j  a)  =  (c.umap  h  f  (c.inj  j  a))


By

---

Latex:
RWH  add\_composeC  0 
THENM  ((RWO  "mcopower\_umap\_comm\_tri<"  0)  THEN  Auto)

---

Home Index