---

Step * of Lemma inv-sinh_wf

∀[x:ℝ]. (inv-sinh(x) ∈ ℝ)
BY
{ (Auto THEN (InstLemma `inv-sinh-domain` [⌜x⌝]⋅ THENA Auto) THEN ProveWfLemma) }

---

Latex:

---

Latex:
\mforall{}[x:\mBbbR{}].  (inv-sinh(x)  \mmember{}  \mBbbR{})


By

---

Latex:
(Auto  THEN  (InstLemma  `inv-sinh-domain`  [\mkleeneopen{}x\mkleeneclose{}]\mcdot{}  THENA  Auto)  THEN  ProveWfLemma)

---

Home Index