---

Step * 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 ∈ v @ as. f[x]) = ((For{g} x ∈ v1. f[x]) * (For{g} x ∈ bs. f[x])) ∈ |g|
BY
{ ((RewriteWith [-1;-4] [] 0) THENA Auto) }

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 ∈ v1 @ bs. 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.  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{}  v  @  as.  f[x])  =  ((For\{g\}  x  \mmember{}  v1.  f[x])  *  (For\{g\}  x  \mmember{}  bs.  f[x]))


By

---

Latex:
((RewriteWith  [-1;-4]  []  0)  THENA  Auto)

---

Home Index