Step * 1 1 1 of Lemma free_abmon_unique


1. DSet
2. FAbMon(S)
3. FAbMon(S)
⊢ (((N.umap M.mon M.inj) (M.umap N.mon N.inj)) M.inj) M.inj ∈ (|S| ⟶ |M.mon|)
BY
((RW CompIdNormC 
 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