---

Step * of Lemma rng_mssum_functionality_wrt_equal

∀s:DSet. ∀r:Rng. ∀f,f':|s| ⟶ |r|. ∀a,a':MSet{s}.
  ((a = a' ∈ MSet{s}) ⇒ (∀x:|s|. ((↑(x ∈b a)) ⇒ (f[x] = f'[x] ∈ |r|))) ⇒ ((Σx ∈ a. f[x]) = (Σx ∈ a'. f'[x]) ∈ |r|))
BY
{ ((Unfold `rng_mssum` 0 
THEN Backchain ``mset_for_functionality new_hyps``) THEN Auto) }

---

Latex:

---

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


By

---

Latex:
((Unfold  `rng\_mssum`  0 
THEN  Backchain  ``mset\_for\_functionality  new\_hyps``)  THEN  Auto)

---

Home Index