:: TOPALG_5 semantic presentation

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 / b

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 / b

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 / b

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 / b

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 / b

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 / b

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