---

Step * of Lemma ss-fun-eq

∀[X,Y:SeparationSpace]. ∀[f,g:Point(X ⟶ Y)].  uiff(f ≡ g;∀a:Point(X). f(a) ≡ g(a))
BY
{ (Intros
   THEN RepUR ``ss-eq`` 0
   THEN (RWO "ss-fun-sep" 0 THENA Auto)
   THEN Fold `ss-ap` 0
   THEN Auto
   THEN (D 0 THENA Auto)
   THEN D -1) }

1
1. X : SeparationSpace
2. Y : SeparationSpace
3. f : Point(X ⟶ Y)
4. g : Point(X ⟶ Y)
5. ∀a:Point(X). (¬f(a) # g(a))
6. a : Point(X)
7. f(a) # g(a)
⊢ False

---

Latex:

---

Latex:
\mforall{}[X,Y:SeparationSpace].  \mforall{}[f,g:Point(X  {}\mrightarrow{}  Y)].    uiff(f  \mequiv{}  g;\mforall{}a:Point(X).  f(a)  \mequiv{}  g(a))


By

---

Latex:
(Intros
  THEN  RepUR  ``ss-eq``  0
  THEN  (RWO  "ss-fun-sep"  0  THENA  Auto)
  THEN  Fold  `ss-ap`  0
  THEN  Auto
  THEN  (D  0  THENA  Auto)
  THEN  D  -1)

---

Home Index