---

Step * of Lemma bag-summation-minus

∀[T:Type]. ∀[r:Rng]. ∀[b:bag(T)]. ∀[f:T ⟶ |r|].  (Σ(x∈b). -r f[x] = (-r Σ(x∈b). f[x]) ∈ |r|)
BY
{ Auto }

1
1. T : Type
2. r : Rng
3. b : bag(T)
4. f : T ⟶ |r|
⊢ Σ(x∈b). -r f[x] = (-r Σ(x∈b). f[x]) ∈ |r|

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[r:Rng].  \mforall{}[b:bag(T)].  \mforall{}[f:T  {}\mrightarrow{}  |r|].    (\mSigma{}(x\mmember{}b).  -r  f[x]  =  (-r  \mSigma{}(x\mmember{}b).  f[x]))


By

---

Latex:
Auto

---

Home Index