---

Step * 1 of Lemma imonomial-cons


∀u,a:ℤ. ∀f:ℤ ⟶ ℤ.  (int_term_value(f;imonomial-term(<a, [u]>)) = int_term_value(f;imonomial-term(<a * (f u), []>)) ∈ ℤ)
BY
{ (RepUR ``imonomial-term int_term_value`` 0 THEN Auto) }

---

Latex:

---

Latex:

\mforall{}u,a:\mBbbZ{}.  \mforall{}f:\mBbbZ{}  {}\mrightarrow{}  \mBbbZ{}.    (int\_term\_value(f;imonomial-term(<a,  [u]>))  =  int\_term\_value(f;imonomial-term(<a\000C  *  (f  u),  []>)))


By

---

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

---

Home Index