---

Step * of Lemma small-ctrex1_wf

small-ctrex1() ∈ ℝ
BY
{ Unfold `small-ctrex1` 0 }

1
un-ctrex1(un-ctrex1((r1)/10^126)) ∈ ℝ

---

Latex:

---

Latex:
small-ctrex1()  \mmember{}  \mBbbR{}


By

---

Latex:
Unfold  `small-ctrex1`  0

---

Home Index