---

Step * of Lemma imonomial-term-add-req

∀vs:ℤ List. ∀a,b:ℤ-o. ∀f:ℤ ⟶ ℝ.  ((real_term_value(f;imonomial-term(<a, vs>)) + real_term_value(f;imonomial-term(<b, vs\000C>))) = real_term_value(f;imonomial-term(<a + b, vs>)))
BY
{ ((Auto THEN RWO "imonomial-term-linear-req" 0 THEN Auto) THEN RWW "rmul-distrib.2< radd-int" 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}vs:\mBbbZ{}  List.  \mforall{}a,b:\mBbbZ{}\msupminus{}\msupzero{}.  \mforall{}f:\mBbbZ{}  {}\mrightarrow{}  \mBbbR{}.
    ((real\_term\_value(f;imonomial-term(<a,  vs>))  +  real\_term\_value(f;imonomial-term(<b,  vs>)))  =  real\_\000Cterm\_value(f;imonomial-term(<a  +  b,  vs>)))


By

---

Latex:
((Auto  THEN  RWO  "imonomial-term-linear-req"  0  THEN  Auto)
  THEN  RWW  "rmul-distrib.2<  radd-int"  0
  THEN  Auto)

---

Home Index