---

Step * 1 1 of Lemma free_abmon_unique


1. S : DSet
2. M : FAbMon(S)
3. N : FAbMon(S)
⊢ ((N.umap M.mon M.inj) o (M.umap N.mon N.inj)) = Id{|M.mon|} ∈ (|M.mon| ⟶ |M.mon|)
BY
{ ((BLemma `free_abmon_endomorph_is_id`) THENA Auto) }

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

---

Latex:

---

Latex:

1.  S  :  DSet
2.  M  :  FAbMon(S)
3.  N  :  FAbMon(S)
\mvdash{}  ((N.umap  M.mon  M.inj)  o  (M.umap  N.mon  N.inj))  =  Id\{|M.mon|\}


By

---

Latex:
((BLemma  `free\_abmon\_endomorph\_is\_id`)  THENA  Auto)

---

Home Index