---

Step * of Lemma free_abmon_endomorph_is_id

∀S:DSet. ∀M:FAbMon(S). ∀f:MonHom(M.mon,M.mon).
  (((f o M.inj) = M.inj ∈ (|S| ⟶ |M.mon|)) ⇒ (f = Id{|M.mon|} ∈ (|M.mon| ⟶ |M.mon|)))
BY
{ ((UnivCD) THENA Auto) }

1
1. S : DSet
2. M : FAbMon(S)
3. f : MonHom(M.mon,M.mon)
4. (f o M.inj) = M.inj ∈ (|S| ⟶ |M.mon|)
⊢ f = Id{|M.mon|} ∈ (|M.mon| ⟶ |M.mon|)

---

Latex:

---

Latex:
\mforall{}S:DSet.  \mforall{}M:FAbMon(S).  \mforall{}f:MonHom(M.mon,M.mon).    (((f  o  M.inj)  =  M.inj)  {}\mRightarrow{}  (f  =  Id\{|M.mon|\}))


By

---

Latex:
((UnivCD)  THENA  Auto)

---

Home Index