---

Step * of Lemma rng_mssum_functionality_wrt_bsubmset

∀s:DSet. ∀r:Rng. ∀f,f':|s| ⟶ |r|. ∀p,q:MSet{s}.
  ((∀x:|s|. ((↑(x ∈b q - p)) ⇒ (f'[x] = 0 ∈ |r|)))
  ⇒ (↑(p ⊆b q))
  ⇒ (∀x:|s|. ((↑(x ∈b p)) ⇒ (f[x] = f'[x] ∈ |r|)))
  ⇒ ((Σx ∈ p. f[x]) = (Σx ∈ q. f'[x]) ∈ |r|))
BY
{ ProveSpecializedLemma `mset_for_functionality_wrt_bsubmset` 2 [parm{i};s;r↓+gp
] (TryC (FoldsC ``rng_when rng_mssum``) ANDTHENC AbReduceC) }

---

Latex:

---

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


By

---

Latex:
ProveSpecializedLemma  `mset\_for\_functionality\_wrt\_bsubmset`  2  [parm\{i\};s;r\mdownarrow{}+gp
]  (TryC  (FoldsC  ``rng\_when  rng\_mssum``)  ANDTHENC  AbReduceC)

---

Home Index