---

Step * of Lemma mset_for_mset_inj

∀s:DSet. ∀g:IAbMonoid. ∀f:|s| ⟶ |g|. ∀u:|s|.  ((msFor{g} x ∈ mset_inj{s}(u). f[x]) = f[u] ∈ |g|)
BY
{ ((UnivCD) THENA Auto) THEN RepUnfolds ``mset_for mset_inj mk_mset`` 0 
THEN AbReduce 0 }

1
1. s : DSet
2. g : IAbMonoid
3. f : |s| ⟶ |g|
4. u : |s|
⊢ (f[u] * e) = f[u] ∈ |g|

---

Latex:

---

Latex:
\mforall{}s:DSet.  \mforall{}g:IAbMonoid.  \mforall{}f:|s|  {}\mrightarrow{}  |g|.  \mforall{}u:|s|.    ((msFor\{g\}  x  \mmember{}  mset\_inj\{s\}(u).  f[x])  =  f[u])


By

---

Latex:
((UnivCD)  THENA  Auto)  THEN  RepUnfolds  ``mset\_for  mset\_inj  mk\_mset``  0 
THEN  AbReduce  0

---

Home Index