---

Step * of Lemma ss-comp_wf

∀[X,Y,Z:SeparationSpace]. ∀[f:Point(Y ⟶ Z)]. ∀[g:Point(X ⟶ Y)].  (ss-comp(f;g) ∈ Point(X ⟶ Z))
BY
{ (Auto THEN (All (RWO "ss-fun-point") THENA Auto) THEN DSetVars THEN MemTypeCD THEN Auto) }

1
1. X : SeparationSpace
2. Y : SeparationSpace
3. Z : SeparationSpace
4. f : Point(Y) ⟶ Point(Z)
5. ss-function(Y;Z;f)
6. g : Point(X) ⟶ Point(Y)
7. ss-function(X;Y;g)
⊢ ss-comp(f;g) ∈ Point(X) ⟶ Point(Z)

2
.....set predicate..... 
1. X : SeparationSpace
2. Y : SeparationSpace
3. Z : SeparationSpace
4. f : Point(Y) ⟶ Point(Z)
5. ss-function(Y;Z;f)
6. g : Point(X) ⟶ Point(Y)
7. ss-function(X;Y;g)
⊢ ss-function(X;Z;ss-comp(f;g))

---

Latex:

---

Latex:
\mforall{}[X,Y,Z:SeparationSpace].  \mforall{}[f:Point(Y  {}\mrightarrow{}  Z)].  \mforall{}[g:Point(X  {}\mrightarrow{}  Y)].    (ss-comp(f;g)  \mmember{}  Point(X  {}\mrightarrow{}  Z))


By

---

Latex:
(Auto  THEN  (All  (RWO  "ss-fun-point")  THENA  Auto)  THEN  DSetVars  THEN  MemTypeCD  THEN  Auto)

---

Home Index