---

Step * of Lemma mod_mssum_functionality

∀s:DSet. ∀r:Rng. ∀m:r-Module. ∀f,f':|s| ⟶ m.car. ∀a,a':MSet{s}.
  ((a = a' ∈ MSet{s})
  ⇒ (∀x:|s|. ((↑(x ∈b a)) ⇒ (f[x] = f'[x] ∈ m.car)))
  ⇒ ((Σm x ∈ a. f[x]) = (Σm x ∈ a'. f'[x]) ∈ m.car))
BY
{ ProveSpecializedLemma `mset_for_functionality` 3 [parm{i};s;m↓grp
] ((TryC (FoldsC ``mod_mssum``) ANDTHENC AbReduceC)) }

---

Latex:

---

Latex:
\mforall{}s:DSet.  \mforall{}r:Rng.  \mforall{}m:r-Module.  \mforall{}f,f':|s|  {}\mrightarrow{}  m.car.  \mforall{}a,a':MSet\{s\}.
    ((a  =  a')  {}\mRightarrow{}  (\mforall{}x:|s|.  ((\muparrow{}(x  \mmember{}\msubb{}  a))  {}\mRightarrow{}  (f[x]  =  f'[x])))  {}\mRightarrow{}  ((\mSigma{}m  x  \mmember{}  a.  f[x])  =  (\mSigma{}m  x  \mmember{}  a'.  f'[x])))


By

---

Latex:
ProveSpecializedLemma  `mset\_for\_functionality`  3  [parm\{i\};s;m\mdownarrow{}grp
]  ((TryC  (FoldsC  ``mod\_mssum``)  ANDTHENC  AbReduceC))

---

Home Index