---

Step * of Lemma path-at_functionality

No Annotations
∀[X:SeparationSpace]. ∀[p:Point(Path(X))]. ∀[t,t':{t:ℝ| t ∈ [r0, r1]} ].  p@t ≡ p@t' supposing t = t'
BY
{ (Auto
   THEN (RWO "path-ss-point" 2 THENA Auto)
   THEN Unfold `path-at` 0
   THEN D 2
   THEN Unhide
   THEN Auto
   THEN BackThruSomeHyp) }

1
1. X : SeparationSpace
2. p : {x:ℝ| (r0 ≤ x) ∧ (x ≤ r1)}  ⟶ Point(X)
3. ∀t,t':{x:ℝ| (r0 ≤ x) ∧ (x ≤ r1)} .  (t ≡ t' ⇒ p t ≡ p t')
4. t : {t:ℝ| t ∈ [r0, r1]} 
5. t' : {t:ℝ| t ∈ [r0, r1]} 
6. t = t'
⊢ t ≡ t'

---

Latex:

---

Latex:
No  Annotations
\mforall{}[X:SeparationSpace].  \mforall{}[p:Point(Path(X))].  \mforall{}[t,t':\{t:\mBbbR{}|  t  \mmember{}  [r0,  r1]\}  ].    p@t  \mequiv{}  p@t'  supposing  t  =  t\000C'


By

---

Latex:
(Auto
  THEN  (RWO  "path-ss-point"  2  THENA  Auto)
  THEN  Unfold  `path-at`  0
  THEN  D  2
  THEN  Unhide
  THEN  Auto
  THEN  BackThruSomeHyp)

---

Home Index