---

Step * 1 2 1 of Lemma free_abmon_unique


1. S : DSet
2. M : FAbMon(S)
3. N : FAbMon(S)
⊢ (((M.umap N.mon N.inj) o (N.umap M.mon M.inj)) o N.inj) = N.inj ∈ (|S| ⟶ |N.mon|)
BY
{ ((RW CompIdNormC 0 
 THENM RewriteWith [] ``free_abmon_umap_properties_1`` 0) THEN Auto) }

---

Latex:

---

Latex:

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


By

---

Latex:
((RW  CompIdNormC  0 
  THENM  RewriteWith  []  ``free\_abmon\_umap\_properties\_1``  0)  THEN  Auto)

---

Home Index