---

Step * 2 of Lemma ss-comp_wf

.....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))
BY
{ ((D 0 THENW Auto) THEN RepUR ``ss-comp`` 0 THEN Auto) }

---

Latex:

---

Latex:
.....set  predicate..... 
1.  X  :  SeparationSpace
2.  Y  :  SeparationSpace
3.  Z  :  SeparationSpace
4.  f  :  Point(Y)  {}\mrightarrow{}  Point(Z)
5.  ss-function(Y;Z;f)
6.  g  :  Point(X)  {}\mrightarrow{}  Point(Y)
7.  ss-function(X;Y;g)
\mvdash{}  ss-function(X;Z;ss-comp(f;g))


By

---

Latex:
((D  0  THENW  Auto)  THEN  RepUR  ``ss-comp``  0  THEN  Auto)

---

Home Index