---

Step * of Lemma circle-param-one-one

∀[t1,t2:ℝ].  t1 = t2 supposing req-vec(2;circle-param(t1);circle-param(t2))
BY
{ (Auto
   THEN DupHyp (-1)
   THEN (D -2 With ⌜0⌝  THENA Auto)
   THEN (D -2 With ⌜1⌝  THENA Auto)
   THEN All (RepUR ``circle-param``)) }

1
1. t1 : ℝ
2. t2 : ℝ
3. (r1 - t1 * t1/r1 + (t1 * t1)) = (r1 - t2 * t2/r1 + (t2 * t2))
4. (r(2) * t1/r1 + (t1 * t1)) = (r(2) * t2/r1 + (t2 * t2))
⊢ t1 = t2

---

Latex:

---

Latex:
\mforall{}[t1,t2:\mBbbR{}].    t1  =  t2  supposing  req-vec(2;circle-param(t1);circle-param(t2))


By

---

Latex:
(Auto
  THEN  DupHyp  (-1)
  THEN  (D  -2  With  \mkleeneopen{}0\mkleeneclose{}    THENA  Auto)
  THEN  (D  -2  With  \mkleeneopen{}1\mkleeneclose{}    THENA  Auto)
  THEN  All  (RepUR  ``circle-param``))

---

Home Index