---

Step * of Lemma rng_lsum_cons_lemma

∀f,v,u,r:Top.  (Σ{r} x ∈ [u / v]. f[x] ~ f[u] +r Σ{r} x ∈ v. f[x])
BY
{ (RepUR ``rng_lsum infix_ap`` 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}f,v,u,r:Top.    (\mSigma{}\{r\}  x  \mmember{}  [u  /  v].  f[x]  \msim{}  f[u]  +r  \mSigma{}\{r\}  x  \mmember{}  v.  f[x])


By

---

Latex:
(RepUR  ``rng\_lsum  infix\_ap``  0  THEN  Auto)

---

Home Index