Step
*
1
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)) o M.inj) = M.inj ∈ (|S| ⟶ |M.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{}  (((N.umap  M.mon  M.inj)  o  (M.umap  N.mon  N.inj))  o  M.inj)  =  M.inj
By
Latex:
((RW  CompIdNormC  0 
  THENM  RewriteWith  []  ``free\_abmon\_umap\_properties\_1``  0)  THEN  Auto)
Home
Index