---

Step * of Lemma const-poly-value

∀[n,f:Top].  (int_term_value(f;ipolynomial-term(const-poly(n))) ~ n)
BY
{ (RepUR ``ipolynomial-term const-poly imonomial-term int_term_value`` 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[n,f:Top].    (int\_term\_value(f;ipolynomial-term(const-poly(n)))  \msim{}  n)


By

---

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

---

Home Index