---

Step * of Lemma rng_mssum_of_plus

∀r:Rng. ∀s:DSet. ∀e,f:|s| ⟶ |r|. ∀a:MSet{s}.  ((Σx ∈ a. (e[x] +r f[x])) = ((Σx ∈ a. e[x]) +r (Σx ∈ a. f[x])) ∈ |r|)
BY
{ ProveSpecializedLemma `mset_for_of_op` 1 [parm{i};r↓+gp] (FoldsC ``rng_when rng_mssum`` ANDTHENC AbReduceC) }

---

Latex:

---

Latex:
\mforall{}r:Rng.  \mforall{}s:DSet.  \mforall{}e,f:|s|  {}\mrightarrow{}  |r|.  \mforall{}a:MSet\{s\}.
    ((\mSigma{}x  \mmember{}  a.  (e[x]  +r  f[x]))  =  ((\mSigma{}x  \mmember{}  a.  e[x])  +r  (\mSigma{}x  \mmember{}  a.  f[x])))


By

---

Latex:
ProveSpecializedLemma  `mset\_for\_of\_op`  1  [parm\{i\};r\mdownarrow{}+gp
]  (FoldsC  ``rng\_when  rng\_mssum``  ANDTHENC  AbReduceC)

---

Home Index