---

Step * of Lemma rat_term_to_real_wf

∀[t:rat_term()]. ∀[f:ℤ ⟶ ℝ].  (rat_term_to_real(f;t) ∈ P:ℙ × ℝ supposing P)
BY
{ ProveWfLemma }

---

Latex:

---

Latex:
\mforall{}[t:rat\_term()].  \mforall{}[f:\mBbbZ{}  {}\mrightarrow{}  \mBbbR{}].    (rat\_term\_to\_real(f;t)  \mmember{}  P:\mBbbP{}  \mtimes{}  \mBbbR{}  supposing  P)


By

---

Latex:
ProveWfLemma

---

Home Index