---

Step * 1 of Lemma full-ss-cat_wf


1. X : SeparationSpace
2. Y : SeparationSpace
3. Z : SeparationSpace
4. ∀f:Point(X) ⟶ Point(Y). (ss-function(X;Y;f) ∈ 𝕌{[1 | i 0]})
5. f : Point(X) ⟶ Point(Y)
6. ss-function(X;Y;f)
7. ∀f:Point(Y) ⟶ Point(Z). (ss-function(Y;Z;f) ∈ 𝕌{[1 | i 0]})
8. g : Point(Y) ⟶ Point(Z)
9. ss-function(Y;Z;g)
10. x : Point(X)
11. x' : Point(X)
12. x ≡ x'
⊢ (g o f) x ≡ (g o f) x'
BY
{ (Reduce 0 THEN RepeatFor 2 (BackThruSomeHyp') THEN Auto) }

---

Latex:

---

Latex:

1.  X  :  SeparationSpace
2.  Y  :  SeparationSpace
3.  Z  :  SeparationSpace
4.  \mforall{}f:Point(X)  {}\mrightarrow{}  Point(Y).  (ss-function(X;Y;f)  \mmember{}  \mBbbU{}\{[1  |  i  0]\})
5.  f  :  Point(X)  {}\mrightarrow{}  Point(Y)
6.  ss-function(X;Y;f)
7.  \mforall{}f:Point(Y)  {}\mrightarrow{}  Point(Z).  (ss-function(Y;Z;f)  \mmember{}  \mBbbU{}\{[1  |  i  0]\})
8.  g  :  Point(Y)  {}\mrightarrow{}  Point(Z)
9.  ss-function(Y;Z;g)
10.  x  :  Point(X)
11.  x'  :  Point(X)
12.  x  \mequiv{}  x'
\mvdash{}  (g  o  f)  x  \mequiv{}  (g  o  f)  x'


By

---

Latex:
(Reduce  0  THEN  RepeatFor  2  (BackThruSomeHyp')  THEN  Auto)

---

Home Index