---

Step * of Lemma full-ss-cat_wf

full-ss-cat{i:l}() ∈ SmallCategory'
BY
{ (ProveWfLemma
   THEN Try (((DSetVars THEN Symmetry) THEN EqTypeCD THEN Auto THEN D 0 THEN Reduce 0 THEN Auto))
   THEN Try (((MemTypeCD THEN Auto) THEN D 0 THEN Auto))) }

1
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'

---

Latex:

---

Latex:
full-ss-cat\{i:l\}()  \mmember{}  SmallCategory'


By

---

Latex:
(ProveWfLemma
  THEN  Try  (((DSetVars  THEN  Symmetry)  THEN  EqTypeCD  THEN  Auto  THEN  D  0  THEN  Reduce  0  THEN  Auto))
  THEN  Try  (((MemTypeCD  THEN  Auto)  THEN  D  0  THEN  Auto)))

---

Home Index