---

Step * of Lemma vs-map-bag-add

∀[K:Rng]. ∀[vs,ws:VectorSpace(K)]. ∀[g:vs ⟶ ws]. ∀[S:Type]. ∀[f:S ⟶ Point(vs)]. ∀[bs:bag(S)].
  ((g Σ{f[b] | b ∈ bs}) = Σ{g f[b] | b ∈ bs} ∈ Point(ws))
BY
{ (Auto THEN BagInd (-1) THEN Auto) }

1
1. K : Rng
2. vs : VectorSpace(K)
3. ws : VectorSpace(K)
4. g : vs ⟶ ws
5. S : Type
6. f : S ⟶ Point(vs)
⊢ (g Σ{f[b] | b ∈ []}) = Σ{g f[b] | b ∈ []} ∈ Point(ws)

2
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)
⊢ (g Σ{f[b] | b ∈ [u / v]}) = Σ{g f[b] | b ∈ [u / v]} ∈ Point(ws)

---

Latex:

---

Latex:
\mforall{}[K:Rng].  \mforall{}[vs,ws:VectorSpace(K)].  \mforall{}[g:vs  {}\mrightarrow{}  ws].  \mforall{}[S:Type].  \mforall{}[f:S  {}\mrightarrow{}  Point(vs)].  \mforall{}[bs:bag(S)].
    ((g  \mSigma{}\{f[b]  |  b  \mmember{}  bs\})  =  \mSigma{}\{g  f[b]  |  b  \mmember{}  bs\})


By

---

Latex:
(Auto  THEN  BagInd  (-1)  THEN  Auto)

---

Home Index