---

Step * 2 of Lemma ring_term_polynomial


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

1
1. r : CRng
2. var : ℤ
3. f : ℤ ⟶ |r|
⊢ ring_term_value(f;"1" (*) vvar) = ring_term_value(f;vvar) ∈ |r|

---

Latex:

---

Latex:

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


By

---

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

---

Home Index