---

Step * of Lemma arcsine_functionality

∀[x:{x:ℝ| x ∈ (r(-1), r1)} ]. ∀[y:ℝ].  arcsine(x) = arcsine(y) supposing x = y
BY
{ ((Auto THEN DSetVars THEN All Reduce THEN Auto)
   THEN Unfold `arcsine` 0
   THEN BLemma `integral_functionality_endpoints`
   THEN Auto
   THEN (InstLemma `rmin-rmax-subinterval` [⌜(r(-1), r1)⌝;⌜r0⌝;⌜x⌝]⋅ THEN Auto)
   THEN BLemma `arcsine_deriv_functionality`
   THEN Auto) }

---

Latex:

---

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


By

---

Latex:
((Auto  THEN  DSetVars  THEN  All  Reduce  THEN  Auto)
  THEN  Unfold  `arcsine`  0
  THEN  BLemma  `integral\_functionality\_endpoints`
  THEN  Auto
  THEN  (InstLemma  `rmin-rmax-subinterval`  [\mkleeneopen{}(r(-1),  r1)\mkleeneclose{};\mkleeneopen{}r0\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]\mcdot{}  THEN  Auto)
  THEN  BLemma  `arcsine\_deriv\_functionality`
  THEN  Auto)

---

Home Index