---

Step * 1 1 1 1 of Lemma mul-monomials-req


1. f : ℤ ⟶ ℝ
⊢ ∀as:ℤ List. (real_term_value(f;imonomial-term(<1, merge-int(as;[])>)) = (real_term_value(f;imonomial-term(<1, as>)) * \000Creal_term_value(f;imonomial-term(<1, []>))))
BY
{ ((Unfold `merge-int` 0 THEN Reduce  0 THEN Auto)
   THEN RepUR ``imonomial-term real_term_value`` 0
   THEN Auto
   THEN nRNorm  0
   THEN Auto) }

---

Latex:

---

Latex:

1.  f  :  \mBbbZ{}  {}\mrightarrow{}  \mBbbR{}
\mvdash{}  \mforall{}as:\mBbbZ{}  List.  (real\_term\_value(f;imonomial-term(ə,  merge-int(as;[])>))  =  (real\_term\_value(f;imonomi\000Cal-term(ə,  as>))  *  real\_term\_value(f;imonomial-term(ə,  []>))))


By

---

Latex:
((Unfold  `merge-int`  0  THEN  Reduce    0  THEN  Auto)
  THEN  RepUR  ``imonomial-term  real\_term\_value``  0
  THEN  Auto
  THEN  nRNorm    0
  THEN  Auto)

---

Home Index