---

Step * 1 of Lemma mset_for_mset_sum


1. s : DSet
2. g : IAbMonoid
3. f : |s| ⟶ |g|
4. a : MSet{s}
5. b : MSet{s}
⊢ (msFor{g} x ∈ a + b. f[x]) = ((msFor{g} x ∈ a. f[x]) * (msFor{g} x ∈ b. f[x])) ∈ |g|
BY
{ ((msetD (-1) THENM msetD 4) THENA Auto) 
THEN Unfolds ``mset_for mset_sum`` 0 }

1
1. s : DSet
2. g : IAbMonoid
3. f : |s| ⟶ |g|
4. as : |s| List
5. bs : |s| List
6. as ≡(|s|) bs
7. v : |s| List
8. v1 : |s| List
9. v ≡(|s|) v1
⊢ (For{g} x ∈ v @ as. f[x]) = ((For{g} x ∈ v1. f[x]) * (For{g} x ∈ bs. f[x])) ∈ |g|

---

Latex:

---

Latex:

1.  s  :  DSet
2.  g  :  IAbMonoid
3.  f  :  |s|  {}\mrightarrow{}  |g|
4.  a  :  MSet\{s\}
5.  b  :  MSet\{s\}
\mvdash{}  (msFor\{g\}  x  \mmember{}  a  +  b.  f[x])  =  ((msFor\{g\}  x  \mmember{}  a.  f[x])  *  (msFor\{g\}  x  \mmember{}  b.  f[x]))


By

---

Latex:
((msetD  (-1)  THENM  msetD  4)  THENA  Auto) 
THEN  Unfolds  ``mset\_for  mset\_sum``  0

---

Home Index