REAL is non empty non finite V213() V214() V215() V219() V317() V318() V320() set
NAT is V213() V214() V215() V216() V217() V218() V219() V317() Element of bool REAL
bool REAL is non empty set
I[01] is non empty strict TopSpace-like T_0 T_1 T_2 connected compact V302() pathwise_connected SubSpace of R^1
R^1 is non empty strict TopSpace-like V302() first-countable Frechet sequential TopStruct
the carrier of I[01] is non empty V213() V214() V215() set
bool REAL is non empty Element of bool (bool REAL)
bool (bool REAL) is non empty set
[:I[01],I[01]:] is non empty strict TopSpace-like T_0 T_1 T_2 connected TopStruct
the carrier of [:I[01],I[01]:] is non empty set
COMPLEX is non empty non finite V213() V219() set
RAT is non empty non finite V213() V214() V215() V216() V219() set
INT is non empty non finite V213() V214() V215() V216() V217() V219() set
[:COMPLEX,COMPLEX:] is non empty V203() set
bool [:COMPLEX,COMPLEX:] is non empty set
[:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty V203() set
bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty set
[:REAL,REAL:] is non empty V203() V204() V205() set
bool [:REAL,REAL:] is non empty set
[:[:REAL,REAL:],REAL:] is non empty V203() V204() V205() set
bool [:[:REAL,REAL:],REAL:] is non empty set
[:RAT,RAT:] is non empty RAT -valued V203() V204() V205() set
bool [:RAT,RAT:] is non empty set
[:[:RAT,RAT:],RAT:] is non empty RAT -valued V203() V204() V205() set
bool [:[:RAT,RAT:],RAT:] is non empty set
[:INT,INT:] is non empty RAT -valued INT -valued V203() V204() V205() set
bool [:INT,INT:] is non empty set
[:[:INT,INT:],INT:] is non empty RAT -valued INT -valued V203() V204() V205() set
bool [:[:INT,INT:],INT:] is non empty set
[:NAT,NAT:] is RAT -valued INT -valued V203() V204() V205() V206() set
[:[:NAT,NAT:],NAT:] is RAT -valued INT -valued V203() V204() V205() V206() set
bool [:[:NAT,NAT:],NAT:] is non empty set
omega is V213() V214() V215() V216() V217() V218() V219() V317() set
bool omega is non empty set
bool NAT is non empty set
K250() is set
1 is non empty ordinal natural V11() ext-real positive non negative real integer V34() V213() V214() V215() V216() V217() V218() V315() V317() Element of NAT
[:NAT,REAL:] is V203() V204() V205() set
bool [:NAT,REAL:] is non empty set
[:NAT,COMPLEX:] is V203() set
bool [:NAT,COMPLEX:] is non empty set
{} is empty Function-like functional FinSequence-membered V213() V214() V215() V216() V217() V218() V219() V317() V320() set
the empty Function-like functional FinSequence-membered V213() V214() V215() V216() V217() V218() V219() V317() V320() set is empty Function-like functional FinSequence-membered V213() V214() V215() V216() V217() V218() V219() V317() V320() set
{{},1} is non empty set
INT.Group is non empty strict V184() V185() V186() V188() cyclic V235() V236() V237() V238() V239() V240() multMagma
K166() is non empty Relation-like [:INT,INT:] -defined INT -valued Function-like V26([:INT,INT:]) quasi_total V203() V204() V205() Element of bool [:[:INT,INT:],INT:]
multMagma(# INT,K166() #) is strict multMagma
the carrier of INT.Group is non empty V213() V214() V215() V216() V217() set
K581() is non empty strict V184() V185() V186() V188() V235() V236() V237() V238() V239() V240() multMagma
K582() is non empty strict V184() V185() V186() V188() cyclic V235() V236() V237() V238() V239() V240() M35(K581())
K583() is non empty strict V184() V186() V188() V238() V239() V240() V241() M38(K581(),K582())
K585() is non empty strict V184() V186() V188() multMagma
K586() is non empty strict V184() V186() V188() V241() M35(K585())
[:1,1:] is non empty RAT -valued INT -valued V203() V204() V205() V206() set
bool [:1,1:] is non empty set
[:[:1,1:],1:] is non empty RAT -valued INT -valued V203() V204() V205() V206() set
bool [:[:1,1:],1:] is non empty set
[:[:1,1:],REAL:] is non empty V203() V204() V205() set
bool [:[:1,1:],REAL:] is non empty set
2 is non empty ordinal natural V11() ext-real positive non negative real integer V34() V213() V214() V215() V216() V217() V218() V315() V317() Element of NAT
[:2,2:] is non empty RAT -valued INT -valued V203() V204() V205() V206() set
[:[:2,2:],REAL:] is non empty V203() V204() V205() set
bool [:[:2,2:],REAL:] is non empty set
TOP-REAL 2 is non empty TopSpace-like right_complementable V138() V139() V140() V141() V142() V143() V144() V225() V226() V290() L20()
the carrier of (TOP-REAL 2) is non empty set
I[01] is non empty strict TopSpace-like T_0 T_1 T_2 connected compact V302() pathwise_connected TopStruct
the carrier of I[01] is non empty V213() V214() V215() set
RealSpace is non empty strict Reflexive discerning symmetric triangle Discerning V302() MetrStruct
[:I[01],I[01]:] is non empty strict TopSpace-like T_0 T_1 T_2 connected TopStruct
the carrier of [:I[01],I[01]:] is non empty set
R^1 is non empty strict TopSpace-like connected V302() pathwise_connected interval first-countable Frechet sequential SubSpace of R^1
the carrier of R^1 is non empty V213() V214() V215() set
bool the carrier of R^1 is non empty set
bool (bool the carrier of R^1) is non empty set
Tunit_circle 2 is non empty TopSpace-like connected compact pathwise_connected being_simple_closed_curve SubSpace of TOP-REAL 2
the carrier of (Tunit_circle 2) is non empty set
[: the carrier of R^1, the carrier of (Tunit_circle 2):] is non empty set
bool [: the carrier of R^1, the carrier of (Tunit_circle 2):] is non empty set
CircleMap is non empty Relation-like the carrier of R^1 -defined the carrier of R^1 -defined the carrier of (Tunit_circle 2) -valued the carrier of (Tunit_circle 2) -valued Function-like V26( the carrier of R^1) V26( the carrier of R^1) quasi_total quasi_total onto continuous Element of bool [: the carrier of R^1, the carrier of (Tunit_circle 2):]
c[10] is Element of the carrier of (Tunit_circle 2)
Topen_unit_circle c[10] is non empty strict TopSpace-like open SubSpace of Tunit_circle 2
the carrier of (Topen_unit_circle c[10]) is non empty set
0 is empty ordinal natural V11() ext-real non positive non negative real Function-like functional integer V34() FinSequence-membered V213() V214() V215() V216() V217() V218() V219() V317() V320() Element of NAT
].0,1.[ is non empty V213() V214() V215() V315() V316() V317() V318() V319() V320() Element of bool REAL
R^1 ].0,1.[ is non empty connected V213() V214() V215() V320() Element of bool the carrier of R^1
R^1 | (R^1 ].0,1.[) is non empty strict TopSpace-like connected V302() pathwise_connected interval SubSpace of R^1
the carrier of (R^1 | (R^1 ].0,1.[)) is non empty V213() V214() V215() set
[: the carrier of (Topen_unit_circle c[10]), the carrier of (R^1 | (R^1 ].0,1.[)):] is non empty V203() V204() V205() set
bool [: the carrier of (Topen_unit_circle c[10]), the carrier of (R^1 | (R^1 ].0,1.[)):] is non empty set
c[-10] is Element of the carrier of (Tunit_circle 2)
Topen_unit_circle c[-10] is non empty strict TopSpace-like open SubSpace of Tunit_circle 2
the carrier of (Topen_unit_circle c[-10]) is non empty set
1 / 2 is V11() ext-real non negative real Element of REAL
3 is non empty ordinal natural V11() ext-real positive non negative real integer V34() V213() V214() V215() V216() V217() V218() V315() V317() Element of NAT
3 / 2 is V11() ext-real non negative real Element of REAL
].(1 / 2),(3 / 2).[ is non empty V213() V214() V215() V315() V316() V317() V318() V319() V320() Element of bool REAL
R^1 ].(1 / 2),(3 / 2).[ is non empty connected V213() V214() V215() V320() Element of bool the carrier of R^1
R^1 | (R^1 ].(1 / 2),(3 / 2).[) is non empty strict TopSpace-like connected V302() pathwise_connected interval SubSpace of R^1
the carrier of (R^1 | (R^1 ].(1 / 2),(3 / 2).[)) is non empty V213() V214() V215() set
[: the carrier of (Topen_unit_circle c[-10]), the carrier of (R^1 | (R^1 ].(1 / 2),(3 / 2).[)):] is non empty V203() V204() V205() set
bool [: the carrier of (Topen_unit_circle c[-10]), the carrier of (R^1 | (R^1 ].(1 / 2),(3 / 2).[)):] is non empty set
[: the carrier of I[01], the carrier of I[01]:] is non empty V203() V204() V205() set
bool [: the carrier of I[01], the carrier of I[01]:] is non empty set
bool the carrier of [:I[01],I[01]:] is non empty set
[:COMPLEX,REAL:] is non empty V203() V204() V205() set
bool [:COMPLEX,REAL:] is non empty set
[.0,1.] is V213() V214() V215() V320() Element of bool REAL
0[01] is V11() ext-real real Element of the carrier of I[01]
1[01] is V11() ext-real real Element of the carrier of I[01]
cos 0 is V11() ext-real real Element of REAL
sin 0 is V11() ext-real real Element of REAL
0. (TOP-REAL 2) is Relation-like NAT -defined Function-like finite V44(2) FinSequence-like FinSubsequence-like V67( TOP-REAL 2) V203() V204() V205() Element of the carrier of (TOP-REAL 2)
the ZeroF of (TOP-REAL 2) is Relation-like NAT -defined Function-like finite V44(2) FinSequence-like FinSubsequence-like V203() V204() V205() Element of the carrier of (TOP-REAL 2)
|[0,0]| is non empty Relation-like NAT -defined Function-like finite V44(2) FinSequence-like FinSubsequence-like V203() V204() V205() Element of the carrier of (TOP-REAL 2)
sqrt 1 is V11() ext-real real Element of REAL
the carrier of R^1 is non empty V213() V214() V215() set
Closed-Interval-TSpace (0,1) is non empty strict TopSpace-like V302() SubSpace of R^1
bool the carrier of I[01] is non empty set
PI is V11() ext-real real Element of REAL
2 * PI is V11() ext-real real Element of REAL
|[1,0]| is non empty Relation-like NAT -defined Function-like finite V44(2) FinSequence-like FinSubsequence-like V203() V204() V205() Element of the carrier of (TOP-REAL 2)
{c[10]} is non empty connected compact Element of bool the carrier of (Tunit_circle 2)
bool the carrier of (Tunit_circle 2) is non empty set
CircleMap " {c[10]} is V213() V214() V215() Element of bool the carrier of R^1
bool (bool the carrier of (Tunit_circle 2)) is non empty set
CircleMap .: ].0,1.[ is Element of bool the carrier of (Tunit_circle 2)
CircleMap .: ].(1 / 2),(3 / 2).[ is Element of bool the carrier of (Tunit_circle 2)
{(CircleMap .: ].0,1.[),(CircleMap .: ].(1 / 2),(3 / 2).[)} is non empty Element of bool (bool the carrier of (Tunit_circle 2))
IntIntervals (0,1) is non empty open Element of bool (bool the carrier of R^1)
union (IntIntervals (0,1)) is V213() V214() V215() Element of bool the carrier of R^1
IntIntervals ((1 / 2),(3 / 2)) is non empty open Element of bool (bool the carrier of R^1)
union (IntIntervals ((1 / 2),(3 / 2))) is V213() V214() V215() Element of bool the carrier of R^1
the carrier of RealSpace is non empty V213() V214() V215() set
len {} is V42() set
[: the carrier of R^1, the carrier of R^1:] is non empty V203() V204() V205() set
bool [: the carrier of R^1, the carrier of R^1:] is non empty set
{0} is non empty V213() V214() V215() V216() V217() V218() V315() V317() Element of bool REAL
[#] I[01] is non empty non proper open closed dense non boundary compact V213() V214() V215() Element of bool the carrier of I[01]
I[01] | ([#] I[01]) is non empty strict TopSpace-like T_0 T_1 T_2 V302() SubSpace of I[01]
1 - 0 is non empty V11() ext-real positive non negative real integer Element of REAL
(3 / 2) - (1 / 2) is V11() ext-real real Element of REAL
TUC is V11() ext-real real set
cS1 is V11() ext-real real set
Closed-Interval-MSpace (TUC,cS1) is non empty strict Reflexive discerning symmetric triangle Discerning V302() SubSpace of RealSpace
the carrier of (Closed-Interval-MSpace (TUC,cS1)) is non empty V213() V214() V215() set
[.TUC,cS1.] is V213() V214() V215() V320() Element of bool REAL
S is V11() ext-real real set
y is V11() ext-real real Element of the carrier of (Closed-Interval-MSpace (TUC,cS1))
Ball (y,S) is V213() V214() V215() Element of bool the carrier of (Closed-Interval-MSpace (TUC,cS1))
bool the carrier of (Closed-Interval-MSpace (TUC,cS1)) is non empty set
y + S is V11() ext-real real set
[.TUC,(y + S).[ is V213() V214() V215() V316() V317() V318() V319() V320() Element of bool REAL
y - S is V11() ext-real real set
].(y - S),cS1.] is V213() V214() V215() V315() V317() V318() V319() V320() Element of bool REAL
].(y - S),(y + S).[ is V213() V214() V215() V315() V316() V317() V318() V319() V320() Element of bool REAL
x is V11() ext-real real Element of the carrier of RealSpace
Ball (x,S) is V213() V214() V215() Element of bool the carrier of RealSpace
bool the carrier of RealSpace is non empty set
(Ball (x,S)) /\ the carrier of (Closed-Interval-MSpace (TUC,cS1)) is V213() V214() V215() Element of bool the carrier of RealSpace
x - S is V11() ext-real real set
x + S is V11() ext-real real set
].(x - S),(x + S).[ is V213() V214() V215() V315() V316() V317() V318() V319() V320() Element of bool REAL
[.TUC,(x + S).[ is V213() V214() V215() V316() V317() V318() V319() V320() Element of bool REAL
ftm is set
yt is V11() ext-real real Element of Ball (y,S)
ftm is set
yt is V11() ext-real real Element of REAL
ftm is set
yt is V11() ext-real real Element of REAL
ftm is set
yt is V11() ext-real real Element of REAL
].(x - S),cS1.] is V213() V214() V215() V315() V317() V318() V319() V320() Element of bool REAL
ftm is set
yt is V11() ext-real real Element of Ball (y,S)
ftm is set
yt is V11() ext-real real Element of REAL
TUC is V11() ext-real real set
cS1 is V11() ext-real real set
Closed-Interval-TSpace (TUC,cS1) is non empty strict TopSpace-like V302() SubSpace of R^1
the carrier of (Closed-Interval-TSpace (TUC,cS1)) is non empty V213() V214() V215() set
bool the carrier of (Closed-Interval-TSpace (TUC,cS1)) is non empty set
bool (bool the carrier of (Closed-Interval-TSpace (TUC,cS1))) is non empty set
Closed-Interval-MSpace (TUC,cS1) is non empty strict Reflexive discerning symmetric triangle Discerning V302() SubSpace of RealSpace
the carrier of (Closed-Interval-MSpace (TUC,cS1)) is non empty V213() V214() V215() set
TopSpaceMetr (Closed-Interval-MSpace (TUC,cS1)) is TopStruct
y is set
S is V11() ext-real real Element of the carrier of (Closed-Interval-TSpace (TUC,cS1))
the carrier of (TopSpaceMetr (Closed-Interval-MSpace (TUC,cS1))) is set
F is Element of the carrier of (TopSpaceMetr (Closed-Interval-MSpace (TUC,cS1)))
Balls F is countable V242( TopSpaceMetr (Closed-Interval-MSpace (TUC,cS1)),F) open Element of bool (bool the carrier of (TopSpaceMetr (Closed-Interval-MSpace (TUC,cS1))))
bool the carrier of (TopSpaceMetr (Closed-Interval-MSpace (TUC,cS1))) is non empty set
bool (bool the carrier of (TopSpaceMetr (Closed-Interval-MSpace (TUC,cS1)))) is non empty set
x is V11() ext-real real Element of the carrier of (Closed-Interval-MSpace (TUC,cS1))
{ (Ball (x,(1 / b1))) where b1 is ordinal natural V11() ext-real non negative real integer V34() V213() V214() V215() V216() V217() V218() V317() Element of NAT : not b1 = 0 } is set
yt is non empty V242( Closed-Interval-TSpace (TUC,cS1),S) open Element of bool (bool the carrier of (Closed-Interval-TSpace (TUC,cS1)))
Pt is V11() ext-real real Element of the carrier of (Closed-Interval-MSpace (TUC,cS1))
{ (Ball (Pt,(1 / b1))) where b1 is ordinal natural V11() ext-real non negative real integer V34() V213() V214() V215() V216() V217() V218() V317() Element of NAT : not b1 = 0 } is set
y is Relation-like the carrier of (Closed-Interval-TSpace (TUC,cS1)) -defined Function-like V26( the carrier of (Closed-Interval-TSpace (TUC,cS1))) set
S is V11() ext-real real Element of the carrier of (Closed-Interval-TSpace (TUC,cS1))
y . S is set
x is V11() ext-real real Element of the carrier of (Closed-Interval-TSpace (TUC,cS1))
F is V11() ext-real real Element of the carrier of (Closed-Interval-MSpace (TUC,cS1))
ftm is non empty V242( Closed-Interval-TSpace (TUC,cS1),x) open Element of bool (bool the carrier of (Closed-Interval-TSpace (TUC,cS1)))
{ (Ball (F,(1 / b1))) where b1 is ordinal natural V11() ext-real non negative real integer V34() V213() V214() V215() V216() V217() V218() V317() Element of NAT : not b1 = 0 } is set
Union y is set
S is quasi_basis open Element of bool (bool the carrier of (Closed-Interval-TSpace (TUC,cS1)))
[.TUC,cS1.] is V213() V214() V215() V320() Element of bool REAL
F is V11() ext-real real Element of the carrier of (Closed-Interval-MSpace (TUC,cS1))
x is Relation-like the carrier of (Closed-Interval-TSpace (TUC,cS1)) -defined Function-like V26( the carrier of (Closed-Interval-TSpace (TUC,cS1))) set
x . F is set
{ (Ball (F,(1 / b1))) where b1 is ordinal natural V11() ext-real non negative real integer V34() V213() V214() V215() V216() V217() V218() V317() Element of NAT : not b1 = 0 } is set
Union x is set
ftm is V11() ext-real real Element of the carrier of (Closed-Interval-TSpace (TUC,cS1))
yt is V11() ext-real real Element of the carrier of (Closed-Interval-MSpace (TUC,cS1))
Pt is non empty V242( Closed-Interval-TSpace (TUC,cS1),ftm) open Element of bool (bool the carrier of (Closed-Interval-TSpace (TUC,cS1)))
{ (Ball (yt,(1 / b1))) where b1 is ordinal natural V11() ext-real non negative real integer V34() V213() V214() V215() V216() V217() V218() V317() Element of NAT : not b1 = 0 } is set
x is V213() V214() V215() Element of bool the carrier of (Closed-Interval-TSpace (TUC,cS1))
rng y is set
union (rng y) is set
F is set
dom y is V213() V214() V215() Element of bool the carrier of (Closed-Interval-TSpace (TUC,cS1))
ftm is set
y . ftm is set
yt is V11() ext-real real Element of the carrier of (Closed-Interval-TSpace (TUC,cS1))
Pt is V11() ext-real real Element of the carrier of (Closed-Interval-MSpace (TUC,cS1))
Qt is non empty V242( Closed-Interval-TSpace (TUC,cS1),yt) open Element of bool (bool the carrier of (Closed-Interval-TSpace (TUC,cS1)))
{ (Ball (Pt,(1 / b1))) where b1 is ordinal natural V11() ext-real non negative real integer V34() V213() V214() V215() V216() V217() V218() V317() Element of NAT : not b1 = 0 } is set
Ft is ordinal natural V11() ext-real non negative real integer V34() V213() V214() V215() V216() V217() V218() V317() Element of NAT
1 / Ft is V11() ext-real non negative real Element of REAL
Ball (Pt,(1 / Ft)) is V213() V214() V215() Element of bool the carrier of (Closed-Interval-MSpace (TUC,cS1))
bool the carrier of (Closed-Interval-MSpace (TUC,cS1)) is non empty set
Pt + (1 / Ft) is V11() ext-real real Element of REAL
[.TUC,(Pt + (1 / Ft)).[ is V213() V214() V215() V316() V317() V318() V319() V320() Element of bool REAL
Pt - (1 / Ft) is V11() ext-real real Element of REAL
].(Pt - (1 / Ft)),cS1.] is V213() V214() V215() V315() V317() V318() V319() V320() Element of bool REAL
].(Pt - (1 / Ft)),(Pt + (1 / Ft)).[ is V213() V214() V215() V315() V316() V317() V318() V319() V320() Element of bool REAL
ft0 is V213() V214() V215() Element of bool the carrier of R^1
TUC is TopStruct
the carrier of TUC is set
bool the carrier of TUC is non empty set
cS1 is Element of bool the carrier of TUC
S is Element of the carrier of TUC
Component_of (S,cS1) is Element of bool the carrier of TUC
Down (S,cS1) is Element of the carrier of (TUC | cS1)
TUC | cS1 is strict SubSpace of TUC
the carrier of (TUC | cS1) is set
Component_of (Down (S,cS1)) is Element of bool the carrier of (TUC | cS1)
bool the carrier of (TUC | cS1) is non empty set
TUC is TopSpace-like TopStruct
the carrier of TUC is set
bool the carrier of TUC is non empty set
cS1 is open Element of bool the carrier of TUC
TUC | cS1 is strict TopSpace-like SubSpace of TUC
S is Element of bool the carrier of TUC
the carrier of (TUC | cS1) is set
TUC is TopSpace-like TopStruct
the carrier of TUC is set
bool the carrier of TUC is non empty set
cS1 is TopSpace-like SubSpace of TUC
the carrier of cS1 is set
bool the carrier of cS1 is non empty set
S is Element of bool the carrier of TUC
TUC | S is strict TopSpace-like SubSpace of TUC
x is Element of bool the carrier of cS1
cS1 | x is strict TopSpace-like SubSpace of cS1
[#] (cS1 | x) is non proper open closed dense Element of bool the carrier of (cS1 | x)
the carrier of (cS1 | x) is set
bool the carrier of (cS1 | x) is non empty set
cS1 is TopSpace-like TopStruct
the carrier of cS1 is set
bool the carrier of cS1 is non empty set
TUC is TopSpace-like TopStruct
the carrier of TUC is set
bool the carrier of TUC is non empty set
the topology of TUC is non empty open Element of bool (bool the carrier of TUC)
bool (bool the carrier of TUC) is non empty set
TopStruct(# the carrier of TUC, the topology of TUC #) is strict TopSpace-like TopStruct
the topology of cS1 is non empty open Element of bool (bool the carrier of cS1)
bool (bool the carrier of cS1) is non empty set
TopStruct(# the carrier of cS1, the topology of cS1 #) is strict TopSpace-like TopStruct
S is Element of bool the carrier of cS1
x is Element of bool the carrier of cS1
y is Element of bool the carrier of TUC
S is Element of bool the carrier of TUC
Cl S is closed Element of bool the carrier of cS1
Cl x is closed Element of bool the carrier of cS1
Cl y is closed Element of bool the carrier of TUC
Cl S is closed Element of bool the carrier of TUC
TUC is TopSpace-like TopStruct
the carrier of TUC is set
the topology of TUC is non empty open Element of bool (bool the carrier of TUC)
bool the carrier of TUC is non empty set
bool (bool the carrier of TUC) is non empty set
TopStruct(# the carrier of TUC, the topology of TUC #) is strict TopSpace-like TopStruct
cS1 is TopSpace-like TopStruct
the carrier of cS1 is set
the topology of cS1 is non empty open Element of bool (bool the carrier of cS1)
bool the carrier of cS1 is non empty set
bool (bool the carrier of cS1) is non empty set
TopStruct(# the carrier of cS1, the topology of cS1 #) is strict TopSpace-like TopStruct
[#] cS1 is non proper open closed dense Element of bool the carrier of cS1
S is Element of bool the carrier of cS1
x is Element of bool the carrier of cS1
S \/ x is Element of bool the carrier of cS1
{} cS1 is empty Function-like functional FinSequence-membered open closed boundary nowhere_dense connected compact V213() V214() V215() V216() V217() V218() V219() V317() V320() Element of bool the carrier of cS1
[#] TUC is non proper open closed dense Element of bool the carrier of TUC
y is Element of bool the carrier of TUC
S is Element of bool the carrier of TUC
{} TUC is empty Function-like functional FinSequence-membered open closed boundary nowhere_dense connected compact V213() V214() V215() V216() V217() V218() V219() V317() V320() Element of bool the carrier of TUC
TUC is TopSpace-like TopStruct
the carrier of TUC is set
bool the carrier of TUC is non empty set
cS1 is TopSpace-like TopStruct
the carrier of cS1 is set
bool the carrier of cS1 is non empty set
the topology of TUC is non empty open Element of bool (bool the carrier of TUC)
bool (bool the carrier of TUC) is non empty set
TopStruct(# the carrier of TUC, the topology of TUC #) is strict TopSpace-like TopStruct
the topology of cS1 is non empty open Element of bool (bool the carrier of cS1)
bool (bool the carrier of cS1) is non empty set
TopStruct(# the carrier of cS1, the topology of cS1 #) is strict TopSpace-like TopStruct
S is Element of bool the carrier of TUC
x is Element of bool the carrier of cS1
y is Element of bool the carrier of cS1
S is Element of bool the carrier of cS1
y \/ S is Element of bool the carrier of cS1
x is Element of bool the carrier of TUC
F is Element of bool the carrier of TUC
{} TUC is empty Function-like functional FinSequence-membered open closed boundary nowhere_dense connected compact V213() V214() V215() V216() V217() V218() V219() V317() V320() Element of bool the carrier of TUC
{} cS1 is empty Function-like functional FinSequence-membered open closed boundary nowhere_dense connected compact V213() V214() V215() V216() V217() V218() V219() V317() V320() Element of bool the carrier of cS1
TUC is non empty TopSpace-like TopStruct
the carrier of TUC is non empty set
cS1 is non empty TopSpace-like TopStruct
the carrier of cS1 is non empty set
the topology of TUC is non empty open Element of bool (bool the carrier of TUC)
bool the carrier of TUC is non empty set
bool (bool the carrier of TUC) is non empty set
TopStruct(# the carrier of TUC, the topology of TUC #) is non empty strict TopSpace-like TopStruct
the topology of cS1 is non empty open Element of bool (bool the carrier of cS1)
bool the carrier of cS1 is non empty set
bool (bool the carrier of cS1) is non empty set
TopStruct(# the carrier of cS1, the topology of cS1 #) is non empty strict TopSpace-like TopStruct
S is Element of the carrier of TUC
x is Element of the carrier of cS1
y is a_neighborhood of S
Int y is open Element of bool the carrier of TUC
S is Element of bool the carrier of cS1
Int S is open Element of bool the carrier of cS1
TUC is non empty TopSpace-like TopStruct
the carrier of TUC is non empty set
bool the carrier of TUC is non empty set
cS1 is non empty TopSpace-like TopStruct
the carrier of cS1 is non empty set
bool the carrier of cS1 is non empty set
the topology of TUC is non empty open Element of bool (bool the carrier of TUC)
bool (bool the carrier of TUC) is non empty set
TopStruct(# the carrier of TUC, the topology of TUC #) is non empty strict TopSpace-like TopStruct
the topology of cS1 is non empty open Element of bool (bool the carrier of cS1)
bool (bool the carrier of cS1) is non empty set
TopStruct(# the carrier of cS1, the topology of cS1 #) is non empty strict TopSpace-like TopStruct
S is Element of bool the carrier of TUC
x is Element of bool the carrier of cS1
y is a_neighborhood of S
Int y is open Element of bool the carrier of TUC
S is Element of bool the carrier of cS1
Int S is open Element of bool the carrier of cS1
cS1 is non empty TopSpace-like TopStruct
the carrier of cS1 is non empty set
bool the carrier of cS1 is non empty set
TUC is non empty TopSpace-like TopStruct
the carrier of TUC is non empty set
[: the carrier of TUC, the carrier of cS1:] is non empty set
bool [: the carrier of TUC, the carrier of cS1:] is non empty set
x is Element of bool the carrier of cS1
S is Element of bool the carrier of cS1
y is non empty Relation-like the carrier of TUC -defined the carrier of cS1 -valued Function-like V26( the carrier of TUC) quasi_total Element of bool [: the carrier of TUC, the carrier of cS1:]
y " x is Element of bool the carrier of TUC
bool the carrier of TUC is non empty set
y " S is Element of bool the carrier of TUC
rng y is Element of bool the carrier of cS1
[#] cS1 is non empty non proper open closed dense non boundary Element of bool the carrier of cS1
cS1 | x is strict TopSpace-like SubSpace of cS1
the carrier of (cS1 | x) is set
bool the carrier of (cS1 | x) is non empty set
x is Element of bool the carrier of (cS1 | x)
y " x is Element of bool the carrier of TUC
TUC | (y " x) is strict TopSpace-like SubSpace of TUC
the carrier of (TUC | (y " x)) is set
bool the carrier of (TUC | (y " x)) is non empty set
F is Element of bool the carrier of (TUC | (y " x))
ftm is Element of bool the carrier of (TUC | (y " x))
y .: F is Element of bool the carrier of cS1
y .: ftm is Element of bool the carrier of cS1
y .: (y " x) is Element of bool the carrier of cS1
dom y is Element of bool the carrier of TUC
Pt is Element of bool the carrier of TUC
y .: Pt is Element of bool the carrier of cS1
yt is Element of bool the carrier of (cS1 | x)
TUC is non empty TopSpace-like TopStruct
the carrier of TUC is non empty set
bool the carrier of TUC is non empty set
cS1 is non empty TopSpace-like SubSpace of TUC
the carrier of cS1 is non empty set
bool the carrier of cS1 is non empty set
S is non empty Element of bool the carrier of TUC
x is non empty Element of bool the carrier of cS1
TUC | S is non empty strict TopSpace-like SubSpace of TUC
cS1 | x is non empty strict TopSpace-like SubSpace of cS1
TUC is non empty TopSpace-like TopStruct
the carrier of TUC is non empty set
the topology of TUC is non empty open Element of bool (bool the carrier of TUC)
bool the carrier of TUC is non empty set
bool (bool the carrier of TUC) is non empty set
TopStruct(# the carrier of TUC, the topology of TUC #) is non empty strict TopSpace-like TopStruct
cS1 is non empty TopSpace-like TopStruct
the carrier of cS1 is non empty set
the topology of cS1 is non empty open Element of bool (bool the carrier of cS1)
bool the carrier of cS1 is non empty set
bool (bool the carrier of cS1) is non empty set
TopStruct(# the carrier of cS1, the topology of cS1 #) is non empty strict TopSpace-like TopStruct
S is Element of the carrier of cS1
y is Element of bool the carrier of cS1
S is Element of bool the carrier of TUC
x is Element of the carrier of TUC
x is Element of bool the carrier of TUC
F is Element of bool the carrier of cS1
TUC is non empty TopSpace-like TopStruct
[#] TUC is non empty non proper open closed dense non boundary Element of bool the carrier of TUC
the carrier of TUC is non empty set
bool the carrier of TUC is non empty set
the topology of TUC is non empty open Element of bool (bool the carrier of TUC)
bool (bool the carrier of TUC) is non empty set
TopStruct(# the carrier of TUC, the topology of TUC #) is non empty strict TopSpace-like TopStruct
TUC | ([#] TUC) is non empty strict TopSpace-like open SubSpace of TUC
the carrier of (TUC | ([#] TUC)) is non empty set
the topology of (TUC | ([#] TUC)) is non empty open Element of bool (bool the carrier of (TUC | ([#] TUC)))
bool the carrier of (TUC | ([#] TUC)) is non empty set
bool (bool the carrier of (TUC | ([#] TUC))) is non empty set
TopStruct(# the carrier of (TUC | ([#] TUC)), the topology of (TUC | ([#] TUC)) #) is non empty strict TopSpace-like TopStruct
TUC is non empty TopSpace-like TopStruct
cS1 is non empty TopSpace-like open SubSpace of TUC
the carrier of cS1 is non empty set
the topology of cS1 is non empty open Element of bool (bool the carrier of cS1)
bool the carrier of cS1 is non empty set
bool (bool the carrier of cS1) is non empty set
TopStruct(# the carrier of cS1, the topology of cS1 #) is non empty strict TopSpace-like TopStruct
the carrier of TUC is non empty set
bool the carrier of TUC is non empty set
[#] cS1 is non empty non proper open closed dense non boundary Element of bool the carrier of cS1
S is non empty Element of bool the carrier of TUC
[#] TopStruct(# the carrier of cS1, the topology of cS1 #) is non empty non proper open closed dense non boundary Element of bool the carrier of TopStruct(# the carrier of cS1, the topology of cS1 #)
the carrier of TopStruct(# the carrier of cS1, the topology of cS1 #) is non empty set
bool the carrier of TopStruct(# the carrier of cS1, the topology of cS1 #) is non empty set
TopStruct(# the carrier of cS1, the topology of cS1 #) | ([#] TopStruct(# the carrier of cS1, the topology of cS1 #)) is non empty strict TopSpace-like open SubSpace of TopStruct(# the carrier of cS1, the topology of cS1 #)
TUC is non empty TopSpace-like TopStruct
cS1 is non empty TopSpace-like open SubSpace of TUC
the carrier of cS1 is non empty set
the topology of cS1 is non empty open Element of bool (bool the carrier of cS1)
bool the carrier of cS1 is non empty set
bool (bool the carrier of cS1) is non empty set
TopStruct(# the carrier of cS1, the topology of cS1 #) is non empty strict TopSpace-like TopStruct
TUC is non empty TopSpace-like TopStruct
cS1 is non empty TopSpace-like TopStruct
the carrier of TUC is non empty set
the carrier of cS1 is non empty set
[: the carrier of TUC, the carrier of cS1:] is non empty set
bool [: the carrier of TUC, the carrier of cS1:] is non empty set
S is non empty Relation-like the carrier of TUC -defined the carrier of cS1 -valued Function-like V26( the carrier of TUC) quasi_total Element of bool [: the carrier of TUC, the carrier of cS1:]
bool the carrier of cS1 is non empty set
x is non empty Element of bool the carrier of cS1
y is Element of bool the carrier of cS1
S " x is Element of bool the carrier of TUC
bool the carrier of TUC is non empty set
S " y is Element of bool the carrier of TUC
rng S is Element of bool the carrier of cS1
[#] cS1 is non empty non proper open closed dense non boundary Element of bool the carrier of cS1
TUC is non empty TopSpace-like TopStruct
the carrier of TUC is non empty set
bool the carrier of TUC is non empty set
bool (bool the carrier of TUC) is non empty set
cS1 is quasi_basis open Element of bool (bool the carrier of TUC)
S is Element of the carrier of TUC
x is Element of bool the carrier of TUC
Int x is open Element of bool the carrier of TUC
the topology of TUC is non empty open Element of bool (bool the carrier of TUC)
UniCl cS1 is Element of bool (bool the carrier of TUC)
y is Element of bool (bool the carrier of TUC)
union y is Element of bool the carrier of TUC
S is set
x is Element of bool the carrier of TUC
Int x is open Element of bool the carrier of TUC
TUC is V11() ext-real real set
cS1 is V11() ext-real real set
Closed-Interval-TSpace (TUC,cS1) is non empty strict TopSpace-like V302() SubSpace of R^1
the carrier of (Closed-Interval-TSpace (TUC,cS1)) is non empty V213() V214() V215() set
bool the carrier of (Closed-Interval-TSpace (TUC,cS1)) is non empty set
bool (bool the carrier of (Closed-Interval-TSpace (TUC,cS1))) is non empty set
Closed-Interval-MSpace (TUC,cS1) is non empty strict Reflexive discerning symmetric triangle Discerning V302() SubSpace of RealSpace
the carrier of (Closed-Interval-MSpace (TUC,cS1)) is non empty V213() V214() V215() set
x is Relation-like the carrier of (Closed-Interval-TSpace (TUC,cS1)) -defined Function-like V26( the carrier of (Closed-Interval-TSpace (TUC,cS1))) set
S is quasi_basis open Element of bool (bool the carrier of (Closed-Interval-TSpace (TUC,cS1)))
Union x is set
TUC is non empty open V213() V214() V215() Element of bool the carrier of I[01]
I[01] | TUC is non empty strict TopSpace-like T_0 T_1 T_2 open V302() SubSpace of I[01]
[: the carrier of I[01], the carrier of R^1:] is non empty V203() V204() V205() set
bool [: the carrier of I[01], the carrier of R^1:] is non empty set
TUC is V11() ext-real real set
cS1 is V11() ext-real real Element of the carrier of I[01]
TUC * cS1 is V11() ext-real real set
cS1 is non empty Relation-like the carrier of I[01] -defined the carrier of R^1 -valued Function-like V26( the carrier of I[01]) quasi_total V203() V204() V205() Element of bool [: the carrier of I[01], the carrier of R^1:]
cS1 is non empty Relation-like the carrier of I[01] -defined the carrier of R^1 -valued Function-like V26( the carrier of I[01]) quasi_total V203() V204() V205() Element of bool [: the carrier of I[01], the carrier of R^1:]
S is non empty Relation-like the carrier of I[01] -defined the carrier of R^1 -valued Function-like V26( the carrier of I[01]) quasi_total V203() V204() V205() Element of bool [: the carrier of I[01], the carrier of R^1:]
x is V11() ext-real real Element of the carrier of I[01]
cS1 . x is V11() ext-real real Element of the carrier of R^1
S . x is V11() ext-real real Element of the carrier of R^1
TUC * x is V11() ext-real real set
TUC is V11() ext-real real set
(TUC) is non empty Relation-like the carrier of I[01] -defined the carrier of R^1 -valued Function-like V26( the carrier of I[01]) quasi_total V203() V204() V205() Element of bool [: the carrier of I[01], the carrier of R^1:]
id I[01] is non empty Relation-like the carrier of I[01] -defined the carrier of I[01] -valued Function-like V26( the carrier of I[01]) quasi_total continuous V203() V204() V205() V271( I[01] , I[01] ) Element of bool [: the carrier of I[01], the carrier of I[01]:]
id the carrier of I[01] is non empty Relation-like the carrier of I[01] -defined the carrier of I[01] -valued Function-like one-to-one V26( the carrier of I[01]) quasi_total V203() V204() V205() increasing V209() Element of bool [: the carrier of I[01], the carrier of I[01]:]
cS1 is non empty Relation-like the carrier of I[01] -defined the carrier of R^1 -valued Function-like V26( the carrier of I[01]) quasi_total V203() V204() V205() Element of bool [: the carrier of I[01], the carrier of R^1:]
S is non empty Relation-like the carrier of I[01] -defined the carrier of R^1 -valued Function-like V26( the carrier of I[01]) quasi_total V203() V204() V205() Element of bool [: the carrier of I[01], the carrier of R^1:]
x is V11() ext-real real Element of the carrier of I[01]
S . x is V11() ext-real real Element of the carrier of R^1
(TUC) . x is V11() ext-real real Element of the carrier of R^1
cS1 . x is V11() ext-real real Element of the carrier of R^1
TUC * (cS1 . x) is V11() ext-real real set
TUC * x is V11() ext-real real set
TUC is V11() ext-real real set
(TUC) is non empty Relation-like the carrier of I[01] -defined the carrier of R^1 -valued Function-like V26( the carrier of I[01]) quasi_total continuous V203() V204() V205() Element of bool [: the carrier of I[01], the carrier of R^1:]
R^1 0 is V11() ext-real real Element of the carrier of R^1
R^1 TUC is V11() ext-real real Element of the carrier of R^1
(TUC) . 0 is V11() ext-real real set
(TUC) . 1 is V11() ext-real real set
(TUC) . 0 is V11() ext-real real Element of REAL
TUC * 0 is V11() ext-real real Element of REAL
(TUC) . 1 is V11() ext-real real Element of REAL
TUC * 1 is V11() ext-real real Element of REAL
TUC is non empty TopSpace-like TopStruct
cS1 is non empty TopSpace-like TopStruct
[:TUC,cS1:] is non empty strict TopSpace-like TopStruct
the carrier of [:TUC,cS1:] is non empty set
S is non empty TopSpace-like TopStruct
the carrier of S is non empty set
[: the carrier of [:TUC,cS1:], the carrier of S:] is non empty set
bool [: the carrier of [:TUC,cS1:], the carrier of S:] is non empty set
the carrier of cS1 is non empty set
the carrier of TUC is non empty set
[: the carrier of TUC, the carrier of S:] is non empty set
bool [: the carrier of TUC, the carrier of S:] is non empty set
x is non empty Relation-like the carrier of [:TUC,cS1:] -defined the carrier of S -valued Function-like V26( the carrier of [:TUC,cS1:]) quasi_total Element of bool [: the carrier of [:TUC,cS1:], the carrier of S:]
y is Element of the carrier of cS1
S is non empty Relation-like the carrier of TUC -defined the carrier of S -valued Function-like V26( the carrier of TUC) quasi_total Element of bool [: the carrier of TUC, the carrier of S:]
x is Element of the carrier of TUC
S . x is Element of the carrier of S
x . (x,y) is set
[x,y] is set
{x,y} is non empty set
{x} is non empty set
{{x,y},{x}} is non empty set
x . [x,y] is set
S is non empty Relation-like the carrier of TUC -defined the carrier of S -valued Function-like V26( the carrier of TUC) quasi_total Element of bool [: the carrier of TUC, the carrier of S:]
x is non empty Relation-like the carrier of TUC -defined the carrier of S -valued Function-like V26( the carrier of TUC) quasi_total Element of bool [: the carrier of TUC, the carrier of S:]
F is Element of the carrier of TUC
S . F is Element of the carrier of S
x . (F,y) is set
[F,y] is set
{F,y} is non empty set
{F} is non empty set
{{F,y},{F}} is non empty set
x . [F,y] is set
x . F is Element of the carrier of S
TUC is non empty TopSpace-like TopStruct
cS1 is non empty TopSpace-like TopStruct
[:TUC,cS1:] is non empty strict TopSpace-like TopStruct
the carrier of [:TUC,cS1:] is non empty set
S is non empty TopSpace-like TopStruct
the carrier of S is non empty set
[: the carrier of [:TUC,cS1:], the carrier of S:] is non empty set
bool [: the carrier of [:TUC,cS1:], the carrier of S:] is non empty set
the carrier of TUC is non empty set
the carrier of cS1 is non empty set
[: the carrier of cS1, the carrier of S:] is non empty set
bool [: the carrier of cS1, the carrier of S:] is non empty set
x is non empty Relation-like the carrier of [:TUC,cS1:] -defined the carrier of S -valued Function-like V26( the carrier of [:TUC,cS1:]) quasi_total Element of bool [: the carrier of [:TUC,cS1:], the carrier of S:]
y is Element of the carrier of TUC
S is non empty Relation-like the carrier of cS1 -defined the carrier of S -valued Function-like V26( the carrier of cS1) quasi_total Element of bool [: the carrier of cS1, the carrier of S:]
x is Element of the carrier of cS1
S . x is Element of the carrier of S
x . (y,x) is set
[y,x] is set
{y,x} is non empty set
{y} is non empty set
{{y,x},{y}} is non empty set
x . [y,x] is set
S is non empty Relation-like the carrier of cS1 -defined the carrier of S -valued Function-like V26( the carrier of cS1) quasi_total Element of bool [: the carrier of cS1, the carrier of S:]
x is non empty Relation-like the carrier of cS1 -defined the carrier of S -valued Function-like V26( the carrier of cS1) quasi_total Element of bool [: the carrier of cS1, the carrier of S:]
F is Element of the carrier of cS1
S . F is Element of the carrier of S
x . (y,F) is set
[y,F] is set
{y,F} is non empty set
{y} is non empty set
{{y,F},{y}} is non empty set
x . [y,F] is set
x . F is Element of the carrier of S
TUC is non empty TopSpace-like TopStruct
cS1 is non empty TopSpace-like TopStruct
[:TUC,cS1:] is non empty strict TopSpace-like TopStruct
the carrier of [:TUC,cS1:] is non empty set
S is non empty TopSpace-like TopStruct
the carrier of S is non empty set
[: the carrier of [:TUC,cS1:], the carrier of S:] is non empty set
bool [: the carrier of [:TUC,cS1:], the carrier of S:] is non empty set
the carrier of cS1 is non empty set
x is non empty Relation-like the carrier of [:TUC,cS1:] -defined the carrier of S -valued Function-like V26( the carrier of [:TUC,cS1:]) quasi_total continuous Element of bool [: the carrier of [:TUC,cS1:], the carrier of S:]
y is Element of the carrier of cS1
(TUC,cS1,S,x,y) is non empty Relation-like the carrier of TUC -defined the carrier of S -valued Function-like V26( the carrier of TUC) quasi_total Element of bool [: the carrier of TUC, the carrier of S:]
the carrier of TUC is non empty set
[: the carrier of TUC, the carrier of S:] is non empty set
bool [: the carrier of TUC, the carrier of S:] is non empty set
bool the carrier of S is non empty set
bool the carrier of TUC is non empty set
S is Element of the carrier of TUC
(TUC,cS1,S,x,y) . S is Element of the carrier of S
x is Element of bool the carrier of S
x . (S,y) is set
[S,y] is set
{S,y} is non empty set
{S} is non empty set
{{S,y},{S}} is non empty set
x . [S,y] is set
bool the carrier of [:TUC,cS1:] is non empty set
[S,y] is Element of the carrier of [:TUC,cS1:]
F is Element of bool the carrier of [:TUC,cS1:]
x .: F is Element of bool the carrier of S
bool (bool the carrier of [:TUC,cS1:]) is non empty set
bool the carrier of cS1 is non empty set
ftm is Element of bool (bool the carrier of [:TUC,cS1:])
union ftm is Element of bool the carrier of [:TUC,cS1:]
yt is set
Pt is Element of bool the carrier of TUC
Qt is Element of bool the carrier of cS1
[:Pt,Qt:] is Element of bool the carrier of [:TUC,cS1:]
(TUC,cS1,S,x,y) .: Pt is Element of bool the carrier of S
Ft is set
ft0 is Element of the carrier of TUC
(TUC,cS1,S,x,y) . ft0 is Element of the carrier of S
[ft0,y] is Element of the carrier of [:TUC,cS1:]
{ft0,y} is non empty set
{ft0} is non empty set
{{ft0,y},{ft0}} is non empty set
x . [ft0,y] is Element of the carrier of S
x . (ft0,y) is set
[ft0,y] is set
x . [ft0,y] is set
TUC is non empty TopSpace-like TopStruct
cS1 is non empty TopSpace-like TopStruct
[:TUC,cS1:] is non empty strict TopSpace-like TopStruct
the carrier of [:TUC,cS1:] is non empty set
S is non empty TopSpace-like TopStruct
the carrier of S is non empty set
[: the carrier of [:TUC,cS1:], the carrier of S:] is non empty set
bool [: the carrier of [:TUC,cS1:], the carrier of S:] is non empty set
the carrier of TUC is non empty set
x is non empty Relation-like the carrier of [:TUC,cS1:] -defined the carrier of S -valued Function-like V26( the carrier of [:TUC,cS1:]) quasi_total continuous Element of bool [: the carrier of [:TUC,cS1:], the carrier of S:]
y is Element of the carrier of TUC
(TUC,cS1,S,x,y) is non empty Relation-like the carrier of cS1 -defined the carrier of S -valued Function-like V26( the carrier of cS1) quasi_total Element of bool [: the carrier of cS1, the carrier of S:]
the carrier of cS1 is non empty set
[: the carrier of cS1, the carrier of S:] is non empty set
bool [: the carrier of cS1, the carrier of S:] is non empty set
bool the carrier of S is non empty set
bool the carrier of cS1 is non empty set
S is Element of the carrier of cS1
(TUC,cS1,S,x,y) . S is Element of the carrier of S
x is Element of bool the carrier of S
x . (y,S) is set
[y,S] is set
{y,S} is non empty set
{y} is non empty set
{{y,S},{y}} is non empty set
x . [y,S] is set
bool the carrier of [:TUC,cS1:] is non empty set
[y,S] is Element of the carrier of [:TUC,cS1:]
F is Element of bool the carrier of [:TUC,cS1:]
x .: F is Element of bool the carrier of S
bool (bool the carrier of [:TUC,cS1:]) is non empty set
bool the carrier of TUC is non empty set
ftm is Element of bool (bool the carrier of [:TUC,cS1:])
union ftm is Element of bool the carrier of [:TUC,cS1:]
yt is set
Pt is Element of bool the carrier of TUC
Qt is Element of bool the carrier of cS1
[:Pt,Qt:] is Element of bool the carrier of [:TUC,cS1:]
(TUC,cS1,S,x,y) .: Qt is Element of bool the carrier of S
Ft is set
ft0 is Element of the carrier of cS1
(TUC,cS1,S,x,y) . ft0 is Element of the carrier of S
[y,ft0] is Element of the carrier of [:TUC,cS1:]
{y,ft0} is non empty set
{{y,ft0},{y}} is non empty set
x . [y,ft0] is Element of the carrier of S
x . (y,ft0) is set
[y,ft0] is set
x . [y,ft0] is set
TUC is non empty TopSpace-like TopStruct
the carrier of TUC is non empty set
cS1 is Element of the carrier of TUC
S is Element of the carrier of TUC
x is non empty Relation-like the carrier of I[01] -defined the carrier of TUC -valued Function-like V26( the carrier of I[01]) quasi_total Path of cS1,S
y is non empty Relation-like the carrier of I[01] -defined the carrier of TUC -valued Function-like V26( the carrier of I[01]) quasi_total Path of cS1,S
S is non empty Relation-like the carrier of [:I[01],I[01]:] -defined the carrier of TUC -valued Function-like V26( the carrier of [:I[01],I[01]:]) quasi_total Homotopy of x,y
x is V11() ext-real real Element of the carrier of I[01]
(I[01],I[01],TUC,S,x) is non empty Relation-like the carrier of I[01] -defined the carrier of TUC -valued Function-like V26( the carrier of I[01]) quasi_total Element of bool [: the carrier of I[01], the carrier of TUC:]
[: the carrier of I[01], the carrier of TUC:] is non empty set
bool [: the carrier of I[01], the carrier of TUC:] is non empty set
TUC is non empty TopSpace-like TopStruct
the carrier of TUC is non empty set
cS1 is Element of the carrier of TUC
S is Element of the carrier of TUC
x is non empty Relation-like the carrier of I[01] -defined the carrier of TUC -valued Function-like V26( the carrier of I[01]) quasi_total Path of cS1,S
y is non empty Relation-like the carrier of I[01] -defined the carrier of TUC -valued Function-like V26( the carrier of I[01]) quasi_total Path of cS1,S
S is non empty Relation-like the carrier of [:I[01],I[01]:] -defined the carrier of TUC -valued Function-like V26( the carrier of [:I[01],I[01]:]) quasi_total Homotopy of x,y
x is V11() ext-real real Element of the carrier of I[01]
(I[01],I[01],TUC,S,x) is non empty Relation-like the carrier of I[01] -defined the carrier of TUC -valued Function-like V26( the carrier of I[01]) quasi_total Element of bool [: the carrier of I[01], the carrier of TUC:]
[: the carrier of I[01], the carrier of TUC:] is non empty set
bool [: the carrier of I[01], the carrier of TUC:] is non empty set
Tcircle ((0. (TOP-REAL 2)),1) is non empty strict TopSpace-like connected compact pathwise_connected being_simple_closed_curve SubSpace of TOP-REAL 2
Sphere (|[0,0]|,1) is Element of bool the carrier of (TOP-REAL 2)
bool the carrier of (TOP-REAL 2) is non empty set
dom CircleMap is V213() V214() V215() Element of bool the carrier of R^1
[: the carrier of I[01], the carrier of (Tunit_circle 2):] is non empty set
bool [: the carrier of I[01], the carrier of (Tunit_circle 2):] is non empty set
S is V11() ext-real real set
(2 * PI) * S is V11() ext-real real Element of REAL
x is V11() ext-real real Element of the carrier of I[01]
((2 * PI) * S) * x is V11() ext-real real Element of REAL
cos (((2 * PI) * S) * x) is V11() ext-real real Element of REAL
sin (((2 * PI) * S) * x) is V11() ext-real real Element of REAL
|[(cos (((2 * PI) * S) * x)),(sin (((2 * PI) * S) * x))]| is non empty Relation-like NAT -defined Function-like finite V44(2) FinSequence-like FinSubsequence-like V203() V204() V205() Element of the carrier of (TOP-REAL 2)
|[(cos (((2 * PI) * S) * x)),(sin (((2 * PI) * S) * x))]| - |[0,0]| is Relation-like NAT -defined Function-like finite V44(2) FinSequence-like FinSubsequence-like V203() V204() V205() Element of the carrier of (TOP-REAL 2)
- |[0,0]| is Relation-like NAT -defined Function-like finite V44(2) FinSequence-like FinSubsequence-like V203() V204() V205() Element of the carrier of (TOP-REAL 2)
K557(|[0,0]|) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V203() V204() V205() FinSequence of REAL
|[(cos (((2 * PI) * S) * x)),(sin (((2 * PI) * S) * x))]| + (- |[0,0]|) is Relation-like NAT -defined Function-like finite V44(2) FinSequence-like FinSubsequence-like V203() V204() V205() Element of the carrier of (TOP-REAL 2)
the addF of (TOP-REAL 2) is non empty Relation-like [: the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2):] -defined the carrier of (TOP-REAL 2) -valued Function-like V26([: the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2):]) quasi_total Element of bool [:[: the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2):], the carrier of (TOP-REAL 2):]
[: the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2):] is non empty set
[:[: the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2):], the carrier of (TOP-REAL 2):] is non empty set
bool [:[: the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2):], the carrier of (TOP-REAL 2):] is non empty set
the addF of (TOP-REAL 2) . (|[(cos (((2 * PI) * S) * x)),(sin (((2 * PI) * S) * x))]|,(- |[0,0]|)) is Relation-like NAT -defined Function-like finite V44(2) FinSequence-like FinSubsequence-like V203() V204() V205() Element of the carrier of (TOP-REAL 2)
[|[(cos (((2 * PI) * S) * x)),(sin (((2 * PI) * S) * x))]|,(- |[0,0]|)] is set
{|[(cos (((2 * PI) * S) * x)),(sin (((2 * PI) * S) * x))]|,(- |[0,0]|)} is non empty functional set
{|[(cos (((2 * PI) * S) * x)),(sin (((2 * PI) * S) * x))]|} is non empty functional set
{{|[(cos (((2 * PI) * S) * x)),(sin (((2 * PI) * S) * x))]|,(- |[0,0]|)},{|[(cos (((2 * PI) * S) * x)),(sin (((2 * PI) * S) * x))]|}} is non empty set
the addF of (TOP-REAL 2) . [|[(cos (((2 * PI) * S) * x)),(sin (((2 * PI) * S) * x))]|,(- |[0,0]|)] is set
K555(|[(cos (((2 * PI) * S) * x)),(sin (((2 * PI) * S) * x))]|,(- |[0,0]|)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V203() V204() V205() FinSequence of REAL
K559(|[(cos (((2 * PI) * S) * x)),(sin (((2 * PI) * S) * x))]|,|[0,0]|) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V203() V204() V205() FinSequence of REAL
|.(|[(cos (((2 * PI) * S) * x)),(sin (((2 * PI) * S) * x))]| - |[0,0]|).| is V11() ext-real non negative real Element of REAL
|.|[(cos (((2 * PI) * S) * x)),(sin (((2 * PI) * S) * x))]|.| is V11() ext-real non negative real Element of REAL
|[(cos (((2 * PI) * S) * x)),(sin (((2 * PI) * S) * x))]| `1 is V11() ext-real real Element of REAL
(|[(cos (((2 * PI) * S) * x)),(sin (((2 * PI) * S) * x))]| `1) ^2 is V11() ext-real real Element of REAL
|[(cos (((2 * PI) * S) * x)),(sin (((2 * PI) * S) * x))]| `2 is V11() ext-real real Element of REAL
(|[(cos (((2 * PI) * S) * x)),(sin (((2 * PI) * S) * x))]| `2) ^2 is V11() ext-real real Element of REAL
((|[(cos (((2 * PI) * S) * x)),(sin (((2 * PI) * S) * x))]| `1) ^2) + ((|[(cos (((2 * PI) * S) * x)),(sin (((2 * PI) * S) * x))]| `2) ^2) is V11() ext-real real Element of REAL
sqrt (((|[(cos (((2 * PI) * S) * x)),(sin (((2 * PI) * S) * x))]| `1) ^2) + ((|[(cos (((2 * PI) * S) * x)),(sin (((2 * PI) * S) * x))]| `2) ^2)) is V11() ext-real real Element of REAL
(cos (((2 * PI) * S) * x)) ^2 is V11() ext-real real Element of REAL
((cos (((2 * PI) * S) * x)) ^2) + ((|[(cos (((2 * PI) * S) * x)),(sin (((2 * PI) * S) * x))]| `2) ^2) is V11() ext-real real Element of REAL
sqrt (((cos (((2 * PI) * S) * x)) ^2) + ((|[(cos (((2 * PI) * S) * x)),(sin (((2 * PI) * S) * x))]| `2) ^2)) is V11() ext-real real Element of REAL
(sin (((2 * PI) * S) * x)) ^2 is V11() ext-real real Element of REAL
((cos (((2 * PI) * S) * x)) ^2) + ((sin (((2 * PI) * S) * x)) ^2) is V11() ext-real real Element of REAL
sqrt (((cos (((2 * PI) * S) * x)) ^2) + ((sin (((2 * PI) * S) * x)) ^2)) is V11() ext-real real Element of REAL
S is Element of the carrier of (Tunit_circle 2)
x is non empty Relation-like the carrier of I[01] -defined the carrier of (Tunit_circle 2) -valued Function-like V26( the carrier of I[01]) quasi_total Element of bool [: the carrier of I[01], the carrier of (Tunit_circle 2):]
x is non empty Relation-like the carrier of I[01] -defined the carrier of (Tunit_circle 2) -valued Function-like V26( the carrier of I[01]) quasi_total Element of bool [: the carrier of I[01], the carrier of (Tunit_circle 2):]
y is non empty Relation-like the carrier of I[01] -defined the carrier of (Tunit_circle 2) -valued Function-like V26( the carrier of I[01]) quasi_total Element of bool [: the carrier of I[01], the carrier of (Tunit_circle 2):]
S is V11() ext-real real Element of the carrier of I[01]
x . S is Element of the carrier of (Tunit_circle 2)
y . S is Element of the carrier of (Tunit_circle 2)
((2 * PI) * S) * S is V11() ext-real real Element of REAL
cos (((2 * PI) * S) * S) is V11() ext-real real Element of REAL
sin (((2 * PI) * S) * S) is V11() ext-real real Element of REAL
|[(cos (((2 * PI) * S) * S)),(sin (((2 * PI) * S) * S))]| is non empty Relation-like NAT -defined Function-like finite V44(2) FinSequence-like FinSubsequence-like V203() V204() V205() Element of the carrier of (TOP-REAL 2)
S is V11() ext-real real set
(S) is non empty Relation-like the carrier of I[01] -defined the carrier of (Tunit_circle 2) -valued Function-like V26( the carrier of I[01]) quasi_total Element of bool [: the carrier of I[01], the carrier of (Tunit_circle 2):]
(S) is non empty Relation-like the carrier of I[01] -defined the carrier of R^1 -valued Function-like V26( the carrier of I[01]) quasi_total continuous V203() V204() V205() Path of R^1 0, R^1 S
R^1 S is V11() ext-real real Element of the carrier of R^1
CircleMap * (S) is non empty Relation-like the carrier of I[01] -defined the carrier of I[01] -defined the carrier of (Tunit_circle 2) -valued the carrier of (Tunit_circle 2) -valued Function-like V26( the carrier of I[01]) V26( the carrier of I[01]) quasi_total quasi_total continuous Element of bool [: the carrier of I[01], the carrier of (Tunit_circle 2):]
x is V11() ext-real real Element of the carrier of I[01]
(S) . x is Element of the carrier of (Tunit_circle 2)
(CircleMap * (S)) . x is Element of the carrier of (Tunit_circle 2)
(S) . x is V11() ext-real real Element of the carrier of R^1
S * x is V11() ext-real real set
(2 * PI) * S is V11() ext-real real Element of REAL
((2 * PI) * S) * x is V11() ext-real real Element of REAL
cos (((2 * PI) * S) * x) is V11() ext-real real Element of REAL
sin (((2 * PI) * S) * x) is V11() ext-real real Element of REAL
|[(cos (((2 * PI) * S) * x)),(sin (((2 * PI) * S) * x))]| is non empty Relation-like NAT -defined Function-like finite V44(2) FinSequence-like FinSubsequence-like V203() V204() V205() Element of the carrier of (TOP-REAL 2)
(2 * PI) * ((S) . x) is V11() ext-real real Element of REAL
cos ((2 * PI) * ((S) . x)) is V11() ext-real real Element of REAL
sin ((2 * PI) * ((S) . x)) is V11() ext-real real Element of REAL
|[(cos ((2 * PI) * ((S) . x))),(sin ((2 * PI) * ((S) . x)))]| is non empty Relation-like NAT -defined Function-like finite V44(2) FinSequence-like FinSubsequence-like V203() V204() V205() Element of the carrier of (TOP-REAL 2)
CircleMap . ((S) . x) is Element of the carrier of (Tunit_circle 2)
S is V11() ext-real real integer set
(S) is non empty Relation-like the carrier of I[01] -defined the carrier of (Tunit_circle 2) -valued Function-like V26( the carrier of I[01]) quasi_total Element of bool [: the carrier of I[01], the carrier of (Tunit_circle 2):]
(S) is non empty Relation-like the carrier of I[01] -defined the carrier of R^1 -valued Function-like V26( the carrier of I[01]) quasi_total continuous V203() V204() V205() Path of R^1 0, R^1 S
R^1 S is V11() ext-real real Element of the carrier of R^1
CircleMap * (S) is non empty Relation-like the carrier of I[01] -defined the carrier of I[01] -defined the carrier of (Tunit_circle 2) -valued the carrier of (Tunit_circle 2) -valued Function-like V26( the carrier of I[01]) V26( the carrier of I[01]) quasi_total quasi_total continuous Element of bool [: the carrier of I[01], the carrier of (Tunit_circle 2):]
(S) . 0 is set
(S) . 1 is set
(2 * PI) * S is V11() ext-real real Element of REAL
j0 is V11() ext-real real Element of the carrier of I[01]
((2 * PI) * S) * j0 is V11() ext-real real Element of REAL
cos (((2 * PI) * S) * j0) is V11() ext-real real Element of REAL
sin (((2 * PI) * S) * j0) is V11() ext-real real Element of REAL
|[(cos (((2 * PI) * S) * j0)),(sin (((2 * PI) * S) * j0))]| is non empty Relation-like NAT -defined Function-like finite V44(2) FinSequence-like FinSubsequence-like V203() V204() V205() Element of the carrier of (TOP-REAL 2)
j1 is V11() ext-real real Element of the carrier of I[01]
((2 * PI) * S) * j1 is V11() ext-real real Element of REAL
cos (((2 * PI) * S) * j1) is V11() ext-real real Element of REAL
sin (((2 * PI) * S) * j1) is V11() ext-real real Element of REAL
|[(cos (((2 * PI) * S) * j1)),(sin (((2 * PI) * S) * j1))]| is non empty Relation-like NAT -defined Function-like finite V44(2) FinSequence-like FinSubsequence-like V203() V204() V205() Element of the carrier of (TOP-REAL 2)
((2 * PI) * S) + 0 is V11() ext-real real Element of REAL
sin (((2 * PI) * S) + 0) is V11() ext-real real Element of REAL
|[(cos 0),(sin (((2 * PI) * S) + 0))]| is non empty Relation-like NAT -defined Function-like finite V44(2) FinSequence-like FinSubsequence-like V203() V204() V205() Element of the carrier of (TOP-REAL 2)
S is Element of bool (bool the carrier of (Tunit_circle 2))
S is Element of bool (bool the carrier of (Tunit_circle 2))
x is Element of bool the carrier of (Tunit_circle 2)
CircleMap " x is V213() V214() V215() Element of bool the carrier of R^1
(Tunit_circle 2) | x is strict TopSpace-like SubSpace of Tunit_circle 2
the carrier of ((Tunit_circle 2) | x) is set
y is mutually-disjoint open Element of bool (bool the carrier of R^1)
union y is V213() V214() V215() Element of bool the carrier of R^1
S is V213() V214() V215() Element of bool the carrier of R^1
R^1 | S is strict TopSpace-like V302() SubSpace of R^1
the carrier of (R^1 | S) is V213() V214() V215() set
[: the carrier of (R^1 | S), the carrier of ((Tunit_circle 2) | x):] is set
bool [: the carrier of (R^1 | S), the carrier of ((Tunit_circle 2) | x):] is non empty set
x is Relation-like the carrier of (R^1 | S) -defined the carrier of ((Tunit_circle 2) | x) -valued Function-like quasi_total Element of bool [: the carrier of (R^1 | S), the carrier of ((Tunit_circle 2) | x):]
CircleMap | S is Relation-like the carrier of R^1 -defined the carrier of (Tunit_circle 2) -valued Function-like Element of bool [: the carrier of R^1, the carrier of (Tunit_circle 2):]
y is mutually-disjoint open Element of bool (bool the carrier of R^1)
union y is V213() V214() V215() Element of bool the carrier of R^1
S is V213() V214() V215() Element of bool the carrier of R^1
R^1 | S is strict TopSpace-like V302() SubSpace of R^1
the carrier of (R^1 | S) is V213() V214() V215() set
[: the carrier of (R^1 | S), the carrier of ((Tunit_circle 2) | x):] is set
bool [: the carrier of (R^1 | S), the carrier of ((Tunit_circle 2) | x):] is non empty set
x is Relation-like the carrier of (R^1 | S) -defined the carrier of ((Tunit_circle 2) | x) -valued Function-like quasi_total Element of bool [: the carrier of (R^1 | S), the carrier of ((Tunit_circle 2) | x):]
CircleMap | S is Relation-like the carrier of R^1 -defined the carrier of (Tunit_circle 2) -valued Function-like Element of bool [: the carrier of R^1, the carrier of (Tunit_circle 2):]
Sspace 0[01] is non empty strict TopSpace-like T_0 T_1 T_2 V302() SubSpace of I[01]
[#] (Sspace 0[01]) is non empty non proper open closed dense non boundary V213() V214() V215() Element of bool the carrier of (Sspace 0[01])
the carrier of (Sspace 0[01]) is non empty V213() V214() V215() set
bool the carrier of (Sspace 0[01]) is non empty set
S is V11() ext-real real set
x is V11() ext-real real set
Closed-Interval-TSpace (S,x) is non empty strict TopSpace-like V302() SubSpace of R^1
the carrier of (Closed-Interval-TSpace (S,x)) is non empty V213() V214() V215() set
bool the carrier of (Closed-Interval-TSpace (S,x)) is non empty set
bool (bool the carrier of (Closed-Interval-TSpace (S,x))) is non empty set
y is Element of bool (bool the carrier of (Closed-Interval-TSpace (S,x)))
S is Relation-like NAT -defined bool REAL -valued Function-like finite FinSequence-like FinSubsequence-like IntervalCover of y
x is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V203() V204() V205() IntervalCoverPts of S
len x is ordinal natural V11() ext-real non negative real integer V34() V213() V214() V215() V216() V217() V218() V317() Element of NAT
len S is ordinal natural V11() ext-real non negative real integer V34() V213() V214() V215() V216() V217() V218() V317() Element of NAT
(len S) + 1 is non empty ordinal natural V11() ext-real positive non negative real integer V34() V213() V214() V215() V216() V217() V218() V315() V317() Element of NAT
x is Element of bool (bool the carrier of (Tunit_circle 2))
y is non empty TopSpace-like TopStruct
[:y,I[01]:] is non empty strict TopSpace-like TopStruct
the carrier of [:y,I[01]:] is non empty set
[: the carrier of [:y,I[01]:], the carrier of (Tunit_circle 2):] is non empty set
bool [: the carrier of [:y,I[01]:], the carrier of (Tunit_circle 2):] is non empty set
the carrier of y is non empty set
bool the carrier of y is non empty set
S is non empty Relation-like the carrier of [:y,I[01]:] -defined the carrier of (Tunit_circle 2) -valued Function-like V26( the carrier of [:y,I[01]:]) quasi_total continuous Element of bool [: the carrier of [:y,I[01]:], the carrier of (Tunit_circle 2):]
x is Element of the carrier of y
[#] (Tunit_circle 2) is non empty non proper open closed dense non boundary compact Element of bool the carrier of (Tunit_circle 2)
union x is Element of bool the carrier of (Tunit_circle 2)
F is V11() ext-real real Element of the carrier of I[01]
[x,F] is Element of the carrier of [:y,I[01]:]
{x,F} is non empty set
{x} is non empty set
{{x,F},{x}} is non empty set
S . [x,F] is Element of the carrier of (Tunit_circle 2)
ftm is set
yt is non empty open Element of bool the carrier of (Tunit_circle 2)
[:y,I[01]:] is non empty strict TopSpace-like TopStruct
the carrier of [:y,I[01]:] is non empty set
[x,0[01]] is Element of the carrier of [:y,I[01]:]
{x,0[01]} is non empty set
{x} is non empty set
{{x,0[01]},{x}} is non empty set
S . [x,0[01]] is Element of the carrier of (Tunit_circle 2)
ftm is non empty open Element of bool the carrier of (Tunit_circle 2)
F is non empty set
yt is V11() ext-real real Element of the carrier of I[01]
[x,yt] is set
{x,yt} is non empty set
{{x,yt},{x}} is non empty set
S . [x,yt] is set
[x,yt] is Element of the carrier of [:y,I[01]:]
S . [x,yt] is Element of the carrier of (Tunit_circle 2)
Pt is non empty open Element of bool the carrier of (Tunit_circle 2)
[: the carrier of I[01],F:] is non empty set
bool [: the carrier of I[01],F:] is non empty set
yt is non empty Relation-like the carrier of I[01] -defined F -valued Function-like V26( the carrier of I[01]) quasi_total Element of bool [: the carrier of I[01],F:]
[: the carrier of y, the carrier of I[01]:] is non empty V203() V204() V205() set
bool [: the carrier of y, the carrier of I[01]:] is non empty set
Pt is V11() ext-real real Element of the carrier of I[01]
yt . Pt is set
[x,Pt] is Element of the carrier of [:y,I[01]:]
{x,Pt} is non empty set
{{x,Pt},{x}} is non empty set
S . [x,Pt] is Element of the carrier of (Tunit_circle 2)
yt . Pt is Element of F