---

Step * 2 1 1 1 of Lemma vs-map-bag-add

.....assertion..... 
1. K : Rng
2. vs : VectorSpace(K)
3. ws : VectorSpace(K)
4. g : vs ⟶ ws
5. S : Type
6. f : S ⟶ Point(vs)
7. u : S
8. v : S List
9. (g Σ{f[b] | b ∈ v}) = Σ{g f[b] | b ∈ v} ∈ Point(ws)
10. v1 : Point(vs)
11. Σ{f[b] | b ∈ v} = v1 ∈ Point(vs)
⊢ (g Σ{f[b] | b ∈ {u}}) = Σ{g f[b] | b ∈ {u}} ∈ Point(ws)
BY
{ (RepUR ``vs-bag-add`` 0
   THEN RWO  "bag-summation-single" 0⋅
   THEN Auto
   THEN RepeatFor 2 ((D 0 THEN Reduce 0 THEN Auto))) }

---

Latex:

---

Latex:
.....assertion..... 
1.  K  :  Rng
2.  vs  :  VectorSpace(K)
3.  ws  :  VectorSpace(K)
4.  g  :  vs  {}\mrightarrow{}  ws
5.  S  :  Type
6.  f  :  S  {}\mrightarrow{}  Point(vs)
7.  u  :  S
8.  v  :  S  List
9.  (g  \mSigma{}\{f[b]  |  b  \mmember{}  v\})  =  \mSigma{}\{g  f[b]  |  b  \mmember{}  v\}
10.  v1  :  Point(vs)
11.  \mSigma{}\{f[b]  |  b  \mmember{}  v\}  =  v1
\mvdash{}  (g  \mSigma{}\{f[b]  |  b  \mmember{}  \{u\}\})  =  \mSigma{}\{g  f[b]  |  b  \mmember{}  \{u\}\}


By

---

Latex:
(RepUR  ``vs-bag-add``  0
  THEN  RWO    "bag-summation-single"  0\mcdot{}
  THEN  Auto
  THEN  RepeatFor  2  ((D  0  THEN  Reduce  0  THEN  Auto)))

---

Home Index