---

Step * of Lemma qsum_wf

∀[a,b:ℤ]. ∀[E:{a..b-} ⟶ ℚ].  (Σa ≤ j < b. E[j] ∈ ℚ)
BY
{ (Unfold `qsum` 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[a,b:\mBbbZ{}].  \mforall{}[E:\{a..b\msupminus{}\}  {}\mrightarrow{}  \mBbbQ{}].    (\mSigma{}a  \mleq{}  j  <  b.  E[j]  \mmember{}  \mBbbQ{})


By

---

Latex:
(Unfold  `qsum`  0  THEN  Auto)

---

Home Index