---

Step * of Lemma rng_fset_for_when_eq

∀s:DSet. ∀r:Rng. ∀f:|s| ⟶ |r|. ∀e:|s|. ∀as:FiniteSet{s}.
  ((↑(e ∈b as)) ⇒ ((Σx ∈ as. (when x (=b) e. f[x])) = f[e] ∈ |r|))
BY
{ ProveSpecializedLemma `fset_for_when_eq` 2 [parm{i};s;r↓+gp
] (TryC (FoldsC ``rng_when rng_mssum``) ANDTHENC AbReduceC) }

---

Latex:

---

Latex:
\mforall{}s:DSet.  \mforall{}r:Rng.  \mforall{}f:|s|  {}\mrightarrow{}  |r|.  \mforall{}e:|s|.  \mforall{}as:FiniteSet\{s\}.
    ((\muparrow{}(e  \mmember{}\msubb{}  as))  {}\mRightarrow{}  ((\mSigma{}x  \mmember{}  as.  (when  x  (=\msubb{})  e.  f[x]))  =  f[e]))


By

---

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

---

Home Index