---

Step * of Lemma ss-ap_functionality

∀[X,Y:SeparationSpace]. ∀[f,g:Point(X ⟶ Y)]. ∀[x,x':Point(X)].  (f(x) ≡ g(x')) supposing (x ≡ x' and f ≡ g)
BY
{ ((Auto THEN RWO "ss-fun-eq" (-2) THEN Auto) THEN (D -2 With ⌜x⌝  THENA Auto)) }

1
1. X : SeparationSpace
2. Y : SeparationSpace
3. f : Point(X ⟶ Y)
4. g : Point(X ⟶ Y)
5. x : Point(X)
6. x' : Point(X)
7. x ≡ x'
8. f(x) ≡ g(x)
⊢ f(x) ≡ g(x')

---

Latex:

---

Latex:
\mforall{}[X,Y:SeparationSpace].  \mforall{}[f,g:Point(X  {}\mrightarrow{}  Y)].  \mforall{}[x,x':Point(X)].
    (f(x)  \mequiv{}  g(x'))  supposing  (x  \mequiv{}  x'  and  f  \mequiv{}  g)


By

---

Latex:
((Auto  THEN  RWO  "ss-fun-eq"  (-2)  THEN  Auto)  THEN  (D  -2  With  \mkleeneopen{}x\mkleeneclose{}    THENA  Auto))

---

Home Index