---

Step * of Lemma rpolynomial_functionality

No Annotations
∀[n:ℕ]. ∀[a,b:ℕn + 1 ⟶ ℝ]. ∀[x,y:ℝ].
  ((Σi≤n. a_i * x^i) = (Σi≤n. b_i * y^i)) supposing ((x = y) and a[k] = b[k] for k ∈ [0,n])
BY
{ (Auto
   THEN Unfold `rpolynomial` 0
   THEN BLemma `rsum_functionality`
   THEN Auto
   THEN RepeatFor 2 (ParallelOp -2)
   THEN RepeatFor 2 (ParallelLast)
   THEN BLemma `rmul_functionality`
   THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[n:\mBbbN{}].  \mforall{}[a,b:\mBbbN{}n  +  1  {}\mrightarrow{}  \mBbbR{}].  \mforall{}[x,y:\mBbbR{}].
    ((\mSigma{}i\mleq{}n.  a\_i  *  x\^{}i)  =  (\mSigma{}i\mleq{}n.  b\_i  *  y\^{}i))  supposing  ((x  =  y)  and  a[k]  =  b[k]  for  k  \mmember{}  [0,n])


By

---

Latex:
(Auto
  THEN  Unfold  `rpolynomial`  0
  THEN  BLemma  `rsum\_functionality`
  THEN  Auto
  THEN  RepeatFor  2  (ParallelOp  -2)
  THEN  RepeatFor  2  (ParallelLast)
  THEN  BLemma  `rmul\_functionality`
  THEN  Auto)

---

Home Index