---

Step * 2 of Lemma real_term_polynomial


1. var : ℤ
⊢ ipolynomial-term([<1, [var]>]) ≡ vvar
BY
{ (RepUR ``ipolynomial-term imonomial-term`` 0 THEN ((D 0 THEN Auto) THEN RepUR ``int_term_value`` 0) THEN Auto) }

1
1. var : ℤ
2. f : ℤ ⟶ ℝ
⊢ real_term_value(f;"1" (*) vvar) = real_term_value(f;vvar)

---

Latex:

---

Latex:

1.  var  :  \mBbbZ{}
\mvdash{}  ipolynomial-term([ə,  [var]>])  \mequiv{}  vvar


By

---

Latex:
(RepUR  ``ipolynomial-term  imonomial-term``  0
  THEN  ((D  0  THEN  Auto)  THEN  RepUR  ``int\_term\_value``  0)
  THEN  Auto)

---

Home Index