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" 0 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