Step * of Lemma ss-const_wf

[X,Y:SeparationSpace]. ∀[c:Point(Y)].  (ss-const(c) ∈ Point(X ⟶ Y))
BY
(Auto
   THEN (RWO "ss-fun-point" THENA Auto)
   THEN MemTypeCD
   THEN Auto
   THEN RepUR ``ss-const ss-function`` 0
   THEN Auto) }


Latex:


Latex:
\mforall{}[X,Y:SeparationSpace].  \mforall{}[c:Point(Y)].    (ss-const(c)  \mmember{}  Point(X  {}\mrightarrow{}  Y))


By


Latex:
(Auto
  THEN  (RWO  "ss-fun-point"  0  THENA  Auto)
  THEN  MemTypeCD
  THEN  Auto
  THEN  RepUR  ``ss-const  ss-function``  0
  THEN  Auto)




Home Index