---

Step * of Lemma weighted-sum_wf

∀[p:ℚ List]. ∀[F:ℕ||p|| ─→ ℚ].  (weighted-sum(p;F) ∈ ℚ)
BY
{ (Unfolds ``weighted-sum`` 0 THEN Auto) }

---

Latex:


\mforall{}[p:\mBbbQ{}  List].  \mforall{}[F:\mBbbN{}||p||  {}\mrightarrow{}  \mBbbQ{}].    (weighted-sum(p;F)  \mmember{}  \mBbbQ{})


By

(Unfolds  ``weighted-sum``  0  THEN  Auto)

---

Home Index