---

Step * of Lemma free_abmon_umap_properties_1

∀S:DSet. ∀M:FAbMon(S). ∀N:AbMon. ∀p:|S| ⟶ |N|.  (((M.umap N p) o M.inj) = p ∈ (|S| ⟶ |N|))
BY
{ ((UnivCD) THENA Auto) }

1
1. S : DSet
2. M : FAbMon(S)
3. N : AbMon
4. p : |S| ⟶ |N|
⊢ ((M.umap N p) o M.inj) = p ∈ (|S| ⟶ |N|)

---

Latex:

---

Latex:
\mforall{}S:DSet.  \mforall{}M:FAbMon(S).  \mforall{}N:AbMon.  \mforall{}p:|S|  {}\mrightarrow{}  |N|.    (((M.umap  N  p)  o  M.inj)  =  p)


By

---

Latex:
((UnivCD)  THENA  Auto)

---

Home Index