---

Step * of Lemma mset_fmon_wf

∀s:DSet. (mset_fmon(s) ∈ FAbMon(s))
BY
{ % Open definitions and let Auto rip % 
 
((Unfolds ``mset_fmon free_abmonoid`` 0) THEN Auto) 
 
% Only non-trivial goals to check involve the umap % }

1
1. s : DSet
2. m : AbMon
3. f : |s| ⟶ |m|
⊢ λy:MSet{s}. msFor{m} z ∈ y
                (f z) ∈ {!g:MonHom(mset_mon{s},m) | (g o (λx:|s|. mset_inj{s}(x))) = f ∈ (|s| ⟶ |m|)}

---

Latex:

---

Latex:
\mforall{}s:DSet.  (mset\_fmon(s)  \mmember{}  FAbMon(s))


By

---

Latex:
\%  Open  definitions  and  let  Auto  rip  \% 
 
((Unfolds  ``mset\_fmon  free\_abmonoid``  0)  THEN  Auto) 
 
\%  Only  non-trivial  goals  to  check  involve  the  umap  \%

---

Home Index