---

Step * of Lemma rprod-single

∀[n:ℤ]. ∀[x:{n..n + 1-} ⟶ ℝ].  (rprod(n;n;k.x[k]) = x[n])
BY
{ (Auto THEN RepeatFor 2 ((Unfold `rprod` 0 THEN AutoSplit))) }

---

Latex:

---

Latex:
\mforall{}[n:\mBbbZ{}].  \mforall{}[x:\{n..n  +  1\msupminus{}\}  {}\mrightarrow{}  \mBbbR{}].    (rprod(n;n;k.x[k])  =  x[n])


By

---

Latex:
(Auto  THEN  RepeatFor  2  ((Unfold  `rprod`  0  THEN  AutoSplit)))

---

Home Index