---

Step * 1 1 1 of Lemma mset_for_mset_sum


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 ∈ v1 @ bs. f[x]) = ((For{g} x ∈ v1. f[x]) * (For{g} x ∈ bs. f[x])) ∈ |g|
BY
{ ((BLemma `mon_for_append`) THEN Auto) }

---

Latex:

---

Latex:

1.  s  :  DSet
2.  g  :  IAbMonoid
3.  f  :  |s|  {}\mrightarrow{}  |g|
4.  as  :  |s|  List
5.  bs  :  |s|  List
6.  as  \mequiv{}(|s|)  bs
7.  v  :  |s|  List
8.  v1  :  |s|  List
9.  v  \mequiv{}(|s|)  v1
\mvdash{}  (For\{g\}  x  \mmember{}  v1  @  bs.  f[x])  =  ((For\{g\}  x  \mmember{}  v1.  f[x])  *  (For\{g\}  x  \mmember{}  bs.  f[x]))


By

---

Latex:
((BLemma  `mon\_for\_append`)  THEN  Auto)

---

Home Index