---

Step * of Lemma arcsin_functionality

∀[x:{x:ℝ| x ∈ [r(-1), r1]} ]. ∀[x':ℝ].  arcsin(x) = arcsin(x') supposing x = x'
BY
{ (Intros
   THEN (Assert x' ∈ {a:ℝ| (r(-1) ≤ a) ∧ (a ≤ r1)}  BY
               (Unhide THEN DSetVars THEN All Reduce THEN MemTypeCD THEN Auto))
   THEN BLemma `arcsin-unique`
   THEN Auto
   THEN RWO  "rsin-arcsin" 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[x:\{x:\mBbbR{}|  x  \mmember{}  [r(-1),  r1]\}  ].  \mforall{}[x':\mBbbR{}].    arcsin(x)  =  arcsin(x')  supposing  x  =  x'


By

---

Latex:
(Intros
  THEN  (Assert  x'  \mmember{}  \{a:\mBbbR{}|  (r(-1)  \mleq{}  a)  \mwedge{}  (a  \mleq{}  r1)\}    BY
                          (Unhide  THEN  DSetVars  THEN  All  Reduce  THEN  MemTypeCD  THEN  Auto))
  THEN  BLemma  `arcsin-unique`
  THEN  Auto
  THEN  RWO    "rsin-arcsin"  0
  THEN  Auto)

---

Home Index