:: 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₁))) where b₁ is ordinal natural V11() ext-real non negative real integer V34() V213() V214() V215() V216() V217() V218() V317() Element of NAT : not b₁ = 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 / b₁))) where b₁ is ordinal natural V11() ext-real non negative real integer V34() V213() V214() V215() V216() V217() V218() V317() Element of NAT : not b₁ = 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 / b₁))) where b₁ is ordinal natural V11() ext-real non negative real integer V34() V213() V214() V215() V216() V217() V218() V317() Element of NAT : not b₁ = 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 / b₁))) where b₁ is ordinal natural V11() ext-real non negative real integer V34() V213() V214() V215() V216() V217() V218() V317() Element of NAT : not b₁ = 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 / b₁))) where b₁ is ordinal natural V11() ext-real non negative real integer V34() V213() V214() V215() V216() V217() V218() V317() Element of NAT : not b₁ = 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 / b₁))) where b₁ is ordinal natural V11() ext-real non negative real integer V34() V213() V214() V215() V216() V217() V218() V317() Element of NAT : not b₁ = 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
Qt is open Element of bool the carrier of (Tunit_circle 2)
bool the carrier of [:y,I[01]:] is non empty set
Ft is Element of bool the carrier of [:y,I[01]:]
S .: Ft is Element of bool the carrier of (Tunit_circle 2)
bool (bool the carrier of [:y,I[01]:]) is non empty set
ft0 is Element of bool (bool the carrier of [:y,I[01]:])
union ft0 is Element of bool the carrier of [:y,I[01]:]
ft1 is set
ftn is Element of bool the carrier of y
ft is V213() V214() V215() Element of bool the carrier of I[01]
[:ftn,ft:] is V203() V204() V205() Element of bool the carrier of [:y,I[01]:]
sM0 is non empty open V213() V214() V215() Element of bool the carrier of I[01]
I[01] | sM0 is non empty strict TopSpace-like T_0 T_1 T_2 open locally_connected V302() SubSpace of I[01]
the carrier of (I[01] | sM0) is non empty V213() V214() V215() set
g2 is V11() ext-real real Element of the carrier of (I[01] | sM0)
Component_of g2 is non empty connected V213() V214() V215() Element of bool the carrier of (I[01] | sM0)
bool the carrier of (I[01] | sM0) is non empty set
Component_of (Pt,sM0) is V213() V214() V215() Element of bool the carrier of I[01]
G is open Element of bool the carrier of y
ft2 is open connected V213() V214() V215() Element of bool the carrier of I[01]
[:G,ft2:] is V203() V204() V205() Element of bool the carrier of [:y,I[01]:]
sM1 is Relation-like the carrier of y -defined the carrier of I[01] -valued V203() V204() V205() Element of bool [: the carrier of y, the carrier of I[01]:]
S .: [:G,ft2:] is Element of bool the carrier of (Tunit_circle 2)
[:G,sM0:] is V203() V204() V205() Element of bool the carrier of [:y,I[01]:]
S .: sM1 is Element of bool the carrier of (Tunit_circle 2)
bool [: the carrier of y, the carrier of I[01]:] is non empty Element of bool (bool [: the carrier of y, the carrier of I[01]:])
bool (bool [: the carrier of y, the carrier of I[01]:]) is non empty set
[: the carrier of I[01],(bool [: the carrier of y, the carrier of I[01]:]):] is non empty set
bool [: the carrier of I[01],(bool [: the carrier of y, the carrier of I[01]:]):] is non empty set
Pt is non empty Relation-like the carrier of I[01] -defined bool [: the carrier of y, the carrier of I[01]:] -valued Function-like V26( the carrier of I[01]) quasi_total Element of bool [: the carrier of I[01],(bool [: the carrier of y, the carrier of I[01]:]):]
bool the carrier of [:y,I[01]:] is non empty set
bool (bool the carrier of [:y,I[01]:]) is non empty set
rng Pt is Element of bool (bool [: the carrier of y, the carrier of I[01]:])
bool (bool [: the carrier of y, the carrier of I[01]:]) is non empty set
Qt is Element of bool (bool the carrier of [:y,I[01]:])
Ft is Element of bool the carrier of [:y,I[01]:]
dom Pt is V213() V214() V215() Element of bool the carrier of I[01]
ft0 is set
Pt . ft0 is set
yt . ft0 is set
ft1 is open Element of bool the carrier of y
ftn is open connected V213() V214() V215() Element of bool the carrier of I[01]
[:ft1,ftn:] is V203() V204() V205() Element of bool the carrier of [:y,I[01]:]
S .: [:ft1,ftn:] is Element of bool the carrier of (Tunit_circle 2)
dom Pt is V213() V214() V215() Element of bool the carrier of I[01]
{x} is non empty connected compact Element of bool the carrier of y
[:{x},([#] I[01]):] is non empty V203() V204() V205() Element of bool the carrier of [:y,I[01]:]
union Qt is Element of bool the carrier of [:y,I[01]:]
Ft is set
ft0 is set
ft1 is set
[ft0,ft1] is set
{ft0,ft1} is non empty set
{ft0} is non empty set
{{ft0,ft1},{ft0}} is non empty set
ftn is V11() ext-real real Element of the carrier of I[01]
yt . ftn is Element of F
Pt . ftn is Relation-like the carrier of y -defined the carrier of I[01] -valued V203() V204() V205() Element of bool [: the carrier of y, the carrier of I[01]:]
ft is open Element of bool the carrier of y
G is open connected V213() V214() V215() Element of bool the carrier of I[01]
[:ft,G:] is V203() V204() V205() Element of bool the carrier of [:y,I[01]:]
S .: [:ft,G:] is Element of bool the carrier of (Tunit_circle 2)
[x,ftn] is Element of the carrier of [:y,I[01]:]
{x,ftn} is non empty set
{{x,ftn},{x}} is non empty set
Ft is Element of bool (bool the carrier of [:y,I[01]:])
{ b₁ where b₁ is open Element of bool the carrier of y : ( x in b₁ & ex b₂ being open V213() V214() V215() Element of bool the carrier of I[01] st [:b₁,b₂:] in Ft ) } is set
bool the carrier of y is non empty Element of bool (bool the carrier of y)
bool (bool the carrier of y) is non empty set
ft1 is set
ftn is open Element of bool the carrier of y
ft is open V213() V214() V215() Element of bool the carrier of I[01]
[:ftn,ft:] is V203() V204() V205() Element of bool the carrier of [:y,I[01]:]
ftn is Relation-like Function-like set
rng ftn is set
dom ftn is set
ft1 is Element of bool (bool the carrier of y)
ft is set
ftn . ft is set
G is set
Pt . G is set
yt . G is set
sM0 is open Element of bool the carrier of y
g2 is open connected V213() V214() V215() Element of bool the carrier of I[01]
[:sM0,g2:] is V203() V204() V205() Element of bool the carrier of [:y,I[01]:]
S .: [:sM0,g2:] is Element of bool the carrier of (Tunit_circle 2)
[:(dom ftn),ft1:] is set
bool [:(dom ftn),ft1:] is non empty set
ft is Relation-like dom ftn -defined ft1 -valued Function-like quasi_total Element of bool [:(dom ftn),ft1:]
{ b₁ where b₁ is open connected V213() V214() V215() Element of bool the carrier of I[01] : ex b₂ being open Element of bool the carrier of y st [:b₂,b₁:] in Ft } is set
union Ft is Element of bool the carrier of [:y,I[01]:]
sM0 is set
g2 is set
Pt . g2 is set
yt . g2 is set
ft2 is open Element of bool the carrier of y
sM1 is open connected V213() V214() V215() Element of bool the carrier of I[01]
[:ft2,sM1:] is V203() V204() V205() Element of bool the carrier of [:y,I[01]:]
S .: [:ft2,sM1:] is Element of bool the carrier of (Tunit_circle 2)
dom ft is Element of bool (dom ftn)
bool (dom ftn) is non empty set
rng ft is Element of bool ft1
bool ft1 is non empty set
Qt is set
Qt is open Element of bool the carrier of y
G is open V213() V214() V215() Element of bool the carrier of I[01]
[:Qt,G:] is V203() V204() V205() Element of bool the carrier of [:y,I[01]:]
G is open V213() V214() V215() Element of bool the carrier of I[01]
[:Qt,G:] is V203() V204() V205() Element of bool the carrier of [:y,I[01]:]
F1 is set
ftn . F1 is set
ft . F1 is set
x is open Element of bool the carrier of y
x1 is non empty open V213() V214() V215() Element of bool the carrier of I[01]
[:x,x1:] is V203() V204() V205() Element of bool the carrier of [:y,I[01]:]
Qt is Element of bool the carrier of y
Qt is open Element of bool the carrier of y
G is open V213() V214() V215() Element of bool the carrier of I[01]
[:Qt,G:] is V203() V204() V205() Element of bool the carrier of [:y,I[01]:]
meet ft1 is Element of bool the carrier of y
bool the carrier of I[01] is non empty Element of bool (bool the carrier of I[01])
bool (bool the carrier of I[01]) is non empty set
Qt is set
G is open connected V213() V214() V215() Element of bool the carrier of I[01]
F1 is open Element of bool the carrier of y
[:F1,G:] is V203() V204() V205() Element of bool the carrier of [:y,I[01]:]
the carrier of (Closed-Interval-TSpace (0,1)) is non empty V213() V214() V215() set
bool the carrier of (Closed-Interval-TSpace (0,1)) is non empty set
bool (bool the carrier of (Closed-Interval-TSpace (0,1))) is non empty set
[#] (Closed-Interval-TSpace (0,1)) is non empty non proper open closed dense non boundary V213() V214() V215() Element of bool the carrier of (Closed-Interval-TSpace (0,1))
Qt is Element of bool (bool the carrier of (Closed-Interval-TSpace (0,1)))
union Qt is V213() V214() V215() Element of bool the carrier of (Closed-Interval-TSpace (0,1))
G is set
F1 is V11() ext-real real Element of the carrier of I[01]
[x,F1] is Element of the carrier of [:y,I[01]:]
{x,F1} is non empty set
{{x,F1},{x}} is non empty set
x is set
x1 is set
Pt . x1 is set
yt . x1 is set
x2 is open Element of bool the carrier of y
XZZ is open connected V213() V214() V215() Element of bool the carrier of I[01]
[:x2,XZZ:] is V203() V204() V205() Element of bool the carrier of [:y,I[01]:]
S .: [:x2,XZZ:] is Element of bool the carrier of (Tunit_circle 2)
the Relation-like NAT -defined bool REAL -valued Function-like finite FinSequence-like FinSubsequence-like IntervalCover of Qt is Relation-like NAT -defined bool REAL -valued Function-like finite FinSequence-like FinSubsequence-like IntervalCover of Qt
the Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V203() V204() V205() IntervalCoverPts of the Relation-like NAT -defined bool REAL -valued Function-like finite FinSequence-like FinSubsequence-like IntervalCover of Qt is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V203() V204() V205() IntervalCoverPts of the Relation-like NAT -defined bool REAL -valued Function-like finite FinSequence-like FinSubsequence-like IntervalCover of Qt
x is V213() V214() V215() Element of bool the carrier of (Closed-Interval-TSpace (0,1))
x1 is open connected V213() V214() V215() Element of bool the carrier of I[01]
x2 is open Element of bool the carrier of y
[:x2,x1:] is V203() V204() V205() Element of bool the carrier of [:y,I[01]:]
x is V213() V214() V215() Element of bool the carrier of (Closed-Interval-TSpace (0,1))
x1 is open connected V213() V214() V215() Element of bool the carrier of I[01]
x2 is open Element of bool the carrier of y
[:x2,x1:] is V203() V204() V205() Element of bool the carrier of [:y,I[01]:]
x is non empty Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V203() V204() V205() FinSequence of REAL
x . 1 is V11() ext-real real Element of REAL
len x is ordinal natural V11() ext-real non negative real integer V34() V213() V214() V215() V216() V217() V218() V317() Element of NAT
x . (len x) is V11() ext-real real Element of REAL
dom x is V213() V214() V215() V216() V217() V218() V317() Element of bool NAT
Qt is open Element of bool the carrier of y
x1 is set
x2 is open Element of bool the carrier of y
XZZ is open V213() V214() V215() Element of bool the carrier of I[01]
[:x2,XZZ:] is V203() V204() V205() Element of bool the carrier of [:y,I[01]:]
x1 is ordinal natural V11() ext-real non negative real integer set
x1 + 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 . x1 is V11() ext-real real Element of REAL
x . (x1 + 1) is V11() ext-real real Element of REAL
[.(x . x1),(x . (x1 + 1)).] is V213() V214() V215() V320() Element of bool REAL
[:Qt,[.(x . x1),(x . (x1 + 1)).]:] is V203() V204() V205() set
S .: [:Qt,[.(x . x1),(x . (x1 + 1)).]:] is Element of bool the carrier of (Tunit_circle 2)
len the Relation-like NAT -defined bool REAL -valued Function-like finite FinSequence-like FinSubsequence-like IntervalCover of Qt is ordinal natural V11() ext-real non negative real integer V34() V213() V214() V215() V216() V217() V218() V317() Element of NAT
(len the Relation-like NAT -defined bool REAL -valued Function-like finite FinSequence-like FinSubsequence-like IntervalCover of Qt) + 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
dom the Relation-like NAT -defined bool REAL -valued Function-like finite FinSequence-like FinSubsequence-like IntervalCover of Qt is V213() V214() V215() V216() V217() V218() V317() Element of bool NAT
the Relation-like NAT -defined bool REAL -valued Function-like finite FinSequence-like FinSubsequence-like IntervalCover of Qt . x1 is set
rng the Relation-like NAT -defined bool REAL -valued Function-like finite FinSequence-like FinSubsequence-like IntervalCover of Qt is Element of bool (bool REAL)
bool (bool REAL) is non empty set
x2 is open connected V213() V214() V215() Element of bool the carrier of I[01]
XZZ is open Element of bool the carrier of y
[:XZZ,x2:] is V203() V204() V205() Element of bool the carrier of [:y,I[01]:]
XZZ is open Element of bool the carrier of y
[:XZZ,x2:] is V203() V204() V205() Element of bool the carrier of [:y,I[01]:]
Uit is set
Pt . Uit is set
[x,Uit] is set
{x,Uit} is non empty set
{{x,Uit},{x}} is non empty set
S . [x,Uit] is set
yt . Uit is set
Uit is open Element of bool the carrier of (Tunit_circle 2)
f is non empty open Element of bool the carrier of (Tunit_circle 2)
f is open Element of bool the carrier of y
Uith is open connected V213() V214() V215() Element of bool the carrier of I[01]
[:f,Uith:] is V203() V204() V205() Element of bool the carrier of [:y,I[01]:]
S .: [:f,Uith:] is Element of bool the carrier of (Tunit_circle 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 non empty TopSpace-like TopStruct
[:x,I[01]:] is non empty strict TopSpace-like TopStruct
the carrier of [:x,I[01]:] is non empty set
[: the carrier of [:x,I[01]:], the carrier of (Tunit_circle 2):] is non empty set
bool [: the carrier of [:x,I[01]:], the carrier of (Tunit_circle 2):] is non empty set
[:x,(Sspace 0[01]):] is non empty strict TopSpace-like TopStruct
the carrier of [:x,(Sspace 0[01]):] is non empty set
[: the carrier of [:x,(Sspace 0[01]):], the carrier of R^1:] is non empty V203() V204() V205() set
bool [: the carrier of [:x,(Sspace 0[01]):], the carrier of R^1:] is non empty set
the carrier of x is non empty set
[: the carrier of x,{0}:] is non empty RAT -valued INT -valued V203() V204() V205() V206() set
[: the carrier of [:x,I[01]:], the carrier of R^1:] is non empty V203() V204() V205() set
bool [: the carrier of [:x,I[01]:], the carrier of R^1:] is non empty set
y is non empty Relation-like the carrier of [:x,I[01]:] -defined the carrier of (Tunit_circle 2) -valued Function-like V26( the carrier of [:x,I[01]:]) quasi_total Element of bool [: the carrier of [:x,I[01]:], the carrier of (Tunit_circle 2):]
y | [: the carrier of x,{0}:] is Relation-like the carrier of [:x,I[01]:] -defined the carrier of (Tunit_circle 2) -valued Function-like Element of bool [: the carrier of [:x,I[01]:], the carrier of (Tunit_circle 2):]
S is non empty Relation-like the carrier of [:x,(Sspace 0[01]):] -defined the carrier of R^1 -valued Function-like V26( the carrier of [:x,(Sspace 0[01]):]) quasi_total V203() V204() V205() Element of bool [: the carrier of [:x,(Sspace 0[01]):], the carrier of R^1:]
CircleMap * S is non empty Relation-like the carrier of [:x,(Sspace 0[01]):] -defined the carrier of (Tunit_circle 2) -valued Function-like V26( the carrier of [:x,(Sspace 0[01]):]) quasi_total Element of bool [: the carrier of [:x,(Sspace 0[01]):], the carrier of (Tunit_circle 2):]
[: the carrier of [:x,(Sspace 0[01]):], the carrier of (Tunit_circle 2):] is non empty set
bool [: the carrier of [:x,(Sspace 0[01]):], the carrier of (Tunit_circle 2):] is non empty set
bool the carrier of x is non empty set
dom y is Element of bool the carrier of [:x,I[01]:]
bool the carrier of [:x,I[01]:] is non empty set
[: the carrier of x, the carrier of I[01]:] is non empty V203() V204() V205() set
[: the carrier of x, the carrier of (Sspace 0[01]):] is non empty V203() V204() V205() set
dom S is Element of bool the carrier of [:x,(Sspace 0[01]):]
bool the carrier of [:x,(Sspace 0[01]):] is non empty set
x is Element of the carrier of [:x,I[01]:]
F is Element of the carrier of x
ftm is V11() ext-real real Element of the carrier of I[01]
[F,ftm] is Element of the carrier of [:x,I[01]:]
{F,ftm} is non empty set
{F} is non empty set
{{F,ftm},{F}} is non empty set
yt is non empty Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V203() V204() V205() FinSequence of REAL
yt . 1 is V11() ext-real real Element of REAL
len yt is ordinal natural V11() ext-real non negative real integer V34() V213() V214() V215() V216() V217() V218() V317() Element of NAT
yt . (len yt) is V11() ext-real real Element of REAL
dom yt is V213() V214() V215() V216() V217() V218() V317() Element of bool NAT
Pt is open Element of bool the carrier of x
Pt is open Element of bool the carrier of x
Qt is non empty open Element of bool the carrier of x
Ft is ordinal natural V11() ext-real non negative real integer V34() V213() V214() V215() V216() V217() V218() V317() Element of NAT
yt . Ft is V11() ext-real real Element of REAL
Ft + 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
Ft + 0 is ordinal natural V11() ext-real non negative real integer V34() V213() V214() V215() V216() V217() V218() V317() Element of NAT
yt . (Ft + 1) is V11() ext-real real Element of REAL
Ft is ordinal natural V11() ext-real non negative real integer V34() V213() V214() V215() V216() V217() V218() V317() Element of NAT
yt . Ft is V11() ext-real real Element of REAL
Ft + 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
yt . (Ft + 1) is V11() ext-real real Element of REAL
[.(yt . Ft),(yt . (Ft + 1)).] is V213() V214() V215() V320() Element of bool REAL
ft0 is set
ft1 is V11() ext-real real Element of REAL
Ft is ordinal natural V11() ext-real non negative real integer V34() V213() V214() V215() V216() V217() V218() V317() Element of NAT
yt . Ft is V11() ext-real real Element of REAL
[.0,(yt . Ft).] is V213() V214() V215() V320() Element of bool REAL
Ft + 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
yt . (Ft + 1) is V11() ext-real real Element of REAL
[.0,(yt . (Ft + 1)).] is V213() V214() V215() V320() Element of bool REAL
ft0 is non empty open Element of bool the carrier of x
x | ft0 is non empty strict TopSpace-like open SubSpace of x
[:ft0, the carrier of I[01]:] is non empty V203() V204() V205() set
S | [:ft0, the carrier of I[01]:] is Relation-like the carrier of [:x,(Sspace 0[01]):] -defined the carrier of R^1 -valued Function-like V203() V204() V205() Element of bool [: the carrier of [:x,(Sspace 0[01]):], the carrier of R^1:]
[:ft0,{0}:] is non empty RAT -valued INT -valued V203() V204() V205() V206() set
S | [:ft0,{0}:] is Relation-like the carrier of [:x,(Sspace 0[01]):] -defined the carrier of R^1 -valued Function-like V203() V204() V205() Element of bool [: the carrier of [:x,(Sspace 0[01]):], the carrier of R^1:]
dom (S | [:ft0,{0}:]) is Element of bool the carrier of [:x,(Sspace 0[01]):]
ft is non empty V213() V214() V215() Element of bool the carrier of I[01]
[:ft0,ft:] is non empty V203() V204() V205() Element of bool the carrier of [:x,I[01]:]
I[01] | ft is non empty strict TopSpace-like T_0 T_1 T_2 V302() SubSpace of I[01]
[:(x | ft0),(I[01] | ft):] is non empty strict TopSpace-like TopStruct
the carrier of [:(x | ft0),(I[01] | ft):] is non empty set
the carrier of (x | ft0) is non empty set
the carrier of (I[01] | ft) is non empty V213() V214() V215() set
[: the carrier of (x | ft0), the carrier of (I[01] | ft):] is non empty V203() V204() V205() set
rng (S | [:ft0,{0}:]) is V213() V214() V215() Element of bool the carrier of R^1
[: the carrier of [:(x | ft0),(I[01] | ft):], the carrier of R^1:] is non empty V203() V204() V205() set
bool [: the carrier of [:(x | ft0),(I[01] | ft):], the carrier of R^1:] is non empty set
y | [:ft0,ft:] is Relation-like the carrier of [:x,I[01]:] -defined the carrier of (Tunit_circle 2) -valued Function-like Element of bool [: the carrier of [:x,I[01]:], the carrier of (Tunit_circle 2):]
dom (y | [:ft0,ft:]) is Element of bool the carrier of [:x,I[01]:]
sM0 is non empty Relation-like the carrier of [:(x | ft0),(I[01] | ft):] -defined the carrier of R^1 -valued Function-like V26( the carrier of [:(x | ft0),(I[01] | ft):]) quasi_total V203() V204() V205() Element of bool [: the carrier of [:(x | ft0),(I[01] | ft):], the carrier of R^1:]
CircleMap * sM0 is non empty Relation-like the carrier of [:(x | ft0),(I[01] | ft):] -defined the carrier of (Tunit_circle 2) -valued Function-like V26( the carrier of [:(x | ft0),(I[01] | ft):]) quasi_total Element of bool [: the carrier of [:(x | ft0),(I[01] | ft):], the carrier of (Tunit_circle 2):]
[: the carrier of [:(x | ft0),(I[01] | ft):], the carrier of (Tunit_circle 2):] is non empty set
bool [: the carrier of [:(x | ft0),(I[01] | ft):], the carrier of (Tunit_circle 2):] is non empty set
sM0 | [: the carrier of x,{0}:] is Relation-like the carrier of [:(x | ft0),(I[01] | ft):] -defined the carrier of R^1 -valued Function-like V203() V204() V205() Element of bool [: the carrier of [:(x | ft0),(I[01] | ft):], the carrier of R^1:]
g2 is non empty V213() V214() V215() Element of bool the carrier of (Sspace 0[01])
(Sspace 0[01]) | g2 is non empty strict TopSpace-like T_0 T_1 T_2 V302() SubSpace of Sspace 0[01]
G is non empty Element of bool the carrier of [:x,(Sspace 0[01]):]
[:x,(Sspace 0[01]):] | G is non empty strict TopSpace-like SubSpace of [:x,(Sspace 0[01]):]
rng sM0 is V213() V214() V215() Element of bool the carrier of R^1
dom (CircleMap * sM0) is Element of bool the carrier of [:(x | ft0),(I[01] | ft):]
bool the carrier of [:(x | ft0),(I[01] | ft):] is non empty set
dom sM0 is Element of bool the carrier of [:(x | ft0),(I[01] | ft):]
ft2 is set
(y | [:ft0,ft:]) . ft2 is set
(CircleMap * sM0) . ft2 is set
y . ft2 is set
(CircleMap * S) . ft2 is set
S . ft2 is V11() ext-real real Element of REAL
CircleMap . (S . ft2) is set
sM0 . ft2 is V11() ext-real real Element of REAL
CircleMap . (sM0 . ft2) is set
dom (sM0 | [: the carrier of x,{0}:]) is Element of bool the carrier of [:(x | ft0),(I[01] | ft):]
[:ft0,ft:] /\ [: the carrier of x,{0}:] is Element of bool the carrier of [:x,I[01]:]
ft2 is set
(sM0 | [: the carrier of x,{0}:]) . ft2 is V11() ext-real real Element of REAL
(S | [:ft0, the carrier of I[01]:]) . ft2 is V11() ext-real real Element of REAL
sM0 . ft2 is V11() ext-real real Element of REAL
S . ft2 is V11() ext-real real Element of REAL
dom (S | [:ft0, the carrier of I[01]:]) is Element of bool the carrier of [:x,(Sspace 0[01]):]
[: the carrier of x,{0}:] /\ [:ft0, the carrier of I[01]:] is set
[.(yt . Ft),(yt . (Ft + 1)).] is V213() V214() V215() V320() Element of bool REAL
[:Qt,[.(yt . Ft),(yt . (Ft + 1)).]:] is V203() V204() V205() set
y .: [:Qt,[.(yt . Ft),(yt . (Ft + 1)).]:] is Element of bool the carrier of (Tunit_circle 2)
ft1 is non empty Element of bool the carrier of (Tunit_circle 2)
CircleMap " ft1 is V213() V214() V215() Element of bool the carrier of R^1
(Tunit_circle 2) | ft1 is non empty strict TopSpace-like SubSpace of Tunit_circle 2
the carrier of ((Tunit_circle 2) | ft1) is non empty set
ftn is mutually-disjoint open Element of bool (bool the carrier of R^1)
union ftn is V213() V214() V215() Element of bool the carrier of R^1
[F,(yt . Ft)] is Element of [: the carrier of x,REAL:]
[: the carrier of x,REAL:] is non empty V203() V204() V205() set
{F,(yt . Ft)} is non empty set
{{F,(yt . Ft)},{F}} is non empty set
ft is non empty open Element of bool the carrier of x
x | ft is non empty strict TopSpace-like open SubSpace of x
G is non empty V213() V214() V215() Element of bool the carrier of I[01]
I[01] | G is non empty strict TopSpace-like T_0 T_1 T_2 V302() SubSpace of I[01]
[:(x | ft),(I[01] | G):] is non empty strict TopSpace-like TopStruct
the carrier of [:(x | ft),(I[01] | G):] is non empty set
[: the carrier of [:(x | ft),(I[01] | G):], the carrier of R^1:] is non empty V203() V204() V205() set
bool [: the carrier of [:(x | ft),(I[01] | G):], the carrier of R^1:] is non empty set
sM0 is non empty Relation-like the carrier of [:(x | ft),(I[01] | G):] -defined the carrier of R^1 -valued Function-like V26( the carrier of [:(x | ft),(I[01] | G):]) quasi_total V203() V204() V205() Element of bool [: the carrier of [:(x | ft),(I[01] | G):], the carrier of R^1:]
[:ft,G:] is non empty V203() V204() V205() Element of bool the carrier of [:x,I[01]:]
y | [:ft,G:] is Relation-like the carrier of [:x,I[01]:] -defined the carrier of (Tunit_circle 2) -valued Function-like Element of bool [: the carrier of [:x,I[01]:], the carrier of (Tunit_circle 2):]
CircleMap * sM0 is non empty Relation-like the carrier of [:(x | ft),(I[01] | G):] -defined the carrier of (Tunit_circle 2) -valued Function-like V26( the carrier of [:(x | ft),(I[01] | G):]) quasi_total Element of bool [: the carrier of [:(x | ft),(I[01] | G):], the carrier of (Tunit_circle 2):]
[: the carrier of [:(x | ft),(I[01] | G):], the carrier of (Tunit_circle 2):] is non empty set
bool [: the carrier of [:(x | ft),(I[01] | G):], the carrier of (Tunit_circle 2):] is non empty set
sM0 | [: the carrier of x,{0}:] is Relation-like the carrier of [:(x | ft),(I[01] | G):] -defined the carrier of R^1 -valued Function-like V203() V204() V205() Element of bool [: the carrier of [:(x | ft),(I[01] | G):], the carrier of R^1:]
[:ft, the carrier of I[01]:] is non empty V203() V204() V205() set
S | [:ft, the carrier of I[01]:] is Relation-like the carrier of [:x,(Sspace 0[01]):] -defined the carrier of R^1 -valued Function-like V203() V204() V205() Element of bool [: the carrier of [:x,(Sspace 0[01]):], the carrier of R^1:]
ft is open Element of bool the carrier of x
x | ft is strict TopSpace-like open SubSpace of x
G is non empty V213() V214() V215() Element of bool the carrier of I[01]
I[01] | G is non empty strict TopSpace-like T_0 T_1 T_2 V302() SubSpace of I[01]
[:(x | ft),(I[01] | G):] is strict TopSpace-like TopStruct
the carrier of [:(x | ft),(I[01] | G):] is set
[: the carrier of [:(x | ft),(I[01] | G):], the carrier of R^1:] is V203() V204() V205() set
bool [: the carrier of [:(x | ft),(I[01] | G):], the carrier of R^1:] is non empty set
sM0 is Relation-like the carrier of [:(x | ft),(I[01] | G):] -defined the carrier of R^1 -valued Function-like V26( the carrier of [:(x | ft),(I[01] | G):]) quasi_total V203() V204() V205() Element of bool [: the carrier of [:(x | ft),(I[01] | G):], the carrier of R^1:]
[:ft,G:] is V203() V204() V205() Element of bool the carrier of [:x,I[01]:]
y | [:ft,G:] is Relation-like the carrier of [:x,I[01]:] -defined the carrier of (Tunit_circle 2) -valued Function-like Element of bool [: the carrier of [:x,I[01]:], the carrier of (Tunit_circle 2):]
CircleMap * sM0 is Relation-like the carrier of [:(x | ft),(I[01] | G):] -defined the carrier of (Tunit_circle 2) -valued Function-like V26( the carrier of [:(x | ft),(I[01] | G):]) quasi_total Element of bool [: the carrier of [:(x | ft),(I[01] | G):], the carrier of (Tunit_circle 2):]
[: the carrier of [:(x | ft),(I[01] | G):], the carrier of (Tunit_circle 2):] is set
bool [: the carrier of [:(x | ft),(I[01] | G):], the carrier of (Tunit_circle 2):] is non empty set
sM0 | [: the carrier of x,{0}:] is Relation-like the carrier of [:(x | ft),(I[01] | G):] -defined the carrier of R^1 -valued Function-like V203() V204() V205() Element of bool [: the carrier of [:(x | ft),(I[01] | G):], the carrier of R^1:]
[:ft, the carrier of I[01]:] is V203() V204() V205() set
S | [:ft, the carrier of I[01]:] is Relation-like the carrier of [:x,(Sspace 0[01]):] -defined the carrier of R^1 -valued Function-like V203() V204() V205() Element of bool [: the carrier of [:x,(Sspace 0[01]):], the carrier of R^1:]
g2 is non empty open Element of bool the carrier of x
x | g2 is non empty strict TopSpace-like open SubSpace of x
[:(x | g2),(I[01] | G):] is non empty strict TopSpace-like TopStruct
the carrier of [:(x | g2),(I[01] | G):] is non empty set
the carrier of (x | g2) is non empty set
the carrier of (I[01] | G) is non empty V213() V214() V215() set
[: the carrier of (x | g2), the carrier of (I[01] | G):] is non empty V203() V204() V205() set
bool the carrier of (x | g2) is non empty set
dom sM0 is Element of bool the carrier of [:(x | ft),(I[01] | G):]
bool the carrier of [:(x | ft),(I[01] | G):] is non empty set
{(yt . Ft)} is non empty V213() V214() V215() Element of bool REAL
bool the carrier of (I[01] | G) is non empty set
sM1 is non empty V213() V214() V215() Element of bool the carrier of I[01]
[:g2,sM1:] is non empty V203() V204() V205() Element of bool the carrier of [:x,I[01]:]
sM0 | [:g2,sM1:] is Relation-like the carrier of [:(x | ft),(I[01] | G):] -defined the carrier of R^1 -valued Function-like V203() V204() V205() Element of bool [: the carrier of [:(x | ft),(I[01] | G):], the carrier of R^1:]
I[01] | sM1 is non empty strict TopSpace-like T_0 T_1 T_2 V302() SubSpace of I[01]
[:(x | g2),(I[01] | sM1):] is non empty strict TopSpace-like TopStruct
the carrier of [:(x | g2),(I[01] | sM1):] is non empty set
the carrier of (I[01] | sM1) is non empty V213() V214() V215() set
[: the carrier of (x | g2), the carrier of (I[01] | sM1):] is non empty V203() V204() V205() set
rng (sM0 | [:g2,sM1:]) is V213() V214() V215() Element of bool the carrier of R^1
[:g2,[.(yt . Ft),(yt . (Ft + 1)).]:] is V203() V204() V205() set
dom (sM0 | [:g2,sM1:]) is Element of bool the carrier of [:(x | ft),(I[01] | G):]
[:g2,{(yt . Ft)}:] is non empty V203() V204() V205() set
ft2 is non empty Element of bool the carrier of (x | g2)
(x | g2) | ft2 is non empty strict TopSpace-like SubSpace of x | g2
Qt is non empty V213() V214() V215() Element of bool the carrier of (I[01] | G)
(I[01] | G) | Qt is non empty strict TopSpace-like T_0 T_1 T_2 V302() SubSpace of I[01] | G
[:((x | g2) | ft2),((I[01] | G) | Qt):] is non empty strict TopSpace-like TopStruct
[:ft2,Qt:] is non empty V203() V204() V205() Element of bool the carrier of [:(x | g2),(I[01] | G):]
bool the carrier of [:(x | g2),(I[01] | G):] is non empty set
[:(x | g2),(I[01] | G):] | [:ft2,Qt:] is non empty strict TopSpace-like SubSpace of [:(x | g2),(I[01] | G):]
[: the carrier of [:(x | g2),(I[01] | sM1):], the carrier of R^1:] is non empty V203() V204() V205() set
bool [: the carrier of [:(x | g2),(I[01] | sM1):], the carrier of R^1:] is non empty set
G is non empty Relation-like the carrier of [:(x | g2),(I[01] | sM1):] -defined the carrier of R^1 -valued Function-like V26( the carrier of [:(x | g2),(I[01] | sM1):]) quasi_total V203() V204() V205() Element of bool [: the carrier of [:(x | g2),(I[01] | sM1):], the carrier of R^1:]
y . [F,(yt . Ft)] is set
[:g2,G:] is non empty V203() V204() V205() Element of bool the carrier of [:x,I[01]:]
(CircleMap * sM0) . [F,(yt . Ft)] is set
sM0 . [F,(yt . Ft)] is V11() ext-real real Element of REAL
CircleMap . (sM0 . [F,(yt . Ft)]) is set
F1 is set
[#] R^1 is non empty non proper open closed dense non boundary V213() V214() V215() Element of bool the carrier of R^1
x is non empty V213() V214() V215() Element of bool the carrier of R^1
G " x is Element of bool the carrier of [:(x | g2),(I[01] | sM1):]
bool the carrier of [:(x | g2),(I[01] | sM1):] is non empty set
bool (bool the carrier of [:(x | g2),(I[01] | sM1):]) is non empty set
bool the carrier of (I[01] | sM1) is non empty set
x1 is Element of bool (bool the carrier of [:(x | g2),(I[01] | sM1):])
union x1 is Element of bool the carrier of [:(x | g2),(I[01] | sM1):]
G . [F,(yt . Ft)] is V11() ext-real real Element of REAL
x2 is set
CircleMap | x 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):]
dom (CircleMap | x) is V213() V214() V215() Element of bool the carrier of R^1
rng (CircleMap | x) is Element of bool the carrier of (Tunit_circle 2)
Uit is set
Uit is set
(CircleMap | x) . Uit is set
CircleMap . Uit is set
Uit is Element of bool the carrier of (x | g2)
Uit is V213() V214() V215() Element of bool the carrier of (I[01] | sM1)
[:Uit,Uit:] is V203() V204() V205() Element of bool the carrier of [:(x | g2),(I[01] | sM1):]
R^1 | x is non empty strict TopSpace-like V302() SubSpace of R^1
the carrier of (R^1 | x) is non empty V213() V214() V215() set
[: the carrier of (R^1 | x), the carrier of ((Tunit_circle 2) | ft1):] is non empty set
bool [: the carrier of (R^1 | x), the carrier of ((Tunit_circle 2) | ft1):] is non empty set
[#] (x | g2) is non empty non proper open closed dense non boundary Element of bool the carrier of (x | g2)
f is Element of bool the carrier of x
f /\ ([#] (x | g2)) is Element of bool the carrier of (x | g2)
Uith is set
Uith is set
[Uith,Uith] is set
{Uith,Uith} is non empty set
{Uith} is non empty set
{{Uith,Uith},{Uith}} is non empty set
f /\ g2 is Element of bool the carrier of x
a is non empty open Element of bool the carrier of x
[:a,[.(yt . Ft),(yt . (Ft + 1)).]:] is V203() V204() V205() set
y .: [:a,[.(yt . Ft),(yt . (Ft + 1)).]:] is Element of bool the carrier of (Tunit_circle 2)
SS is non empty V213() V214() V215() Element of bool the carrier of I[01]
[:a,SS:] is non empty V203() V204() V205() Element of bool the carrier of [:x,I[01]:]
y | [:a,SS:] is Relation-like the carrier of [:x,I[01]:] -defined the carrier of (Tunit_circle 2) -valued Function-like Element of bool [: the carrier of [:x,I[01]:], the carrier of (Tunit_circle 2):]
dom (y | [:a,SS:]) is Element of bool the carrier of [:x,I[01]:]
f is non empty Relation-like the carrier of (R^1 | x) -defined the carrier of ((Tunit_circle 2) | ft1) -valued Function-like V26( the carrier of (R^1 | x)) quasi_total Element of bool [: the carrier of (R^1 | x), the carrier of ((Tunit_circle 2) | ft1):]
f " is non empty Relation-like the carrier of ((Tunit_circle 2) | ft1) -defined the carrier of (R^1 | x) -valued Function-like V26( the carrier of ((Tunit_circle 2) | ft1)) quasi_total V203() V204() V205() Element of bool [: the carrier of ((Tunit_circle 2) | ft1), the carrier of (R^1 | x):]
[: the carrier of ((Tunit_circle 2) | ft1), the carrier of (R^1 | x):] is non empty V203() V204() V205() set
bool [: the carrier of ((Tunit_circle 2) | ft1), the carrier of (R^1 | x):] is non empty set
(f ") * (y | [:a,SS:]) is Relation-like the carrier of [:x,I[01]:] -defined the carrier of (R^1 | x) -valued Function-like V203() V204() V205() Element of bool [: the carrier of [:x,I[01]:], the carrier of (R^1 | x):]
[: the carrier of [:x,I[01]:], the carrier of (R^1 | x):] is non empty V203() V204() V205() set
bool [: the carrier of [:x,I[01]:], the carrier of (R^1 | x):] is non empty set
dom (f ") is Element of bool the carrier of ((Tunit_circle 2) | ft1)
bool the carrier of ((Tunit_circle 2) | ft1) is non empty set
[#] ((Tunit_circle 2) | ft1) is non empty non proper open closed dense non boundary Element of bool the carrier of ((Tunit_circle 2) | ft1)
rng (y | [:a,SS:]) is Element of bool the carrier of (Tunit_circle 2)
Fn2 is set
ff is set
(y | [:a,SS:]) . ff is set
y . ff is set
y .: [:a,SS:] is Element of bool the carrier of (Tunit_circle 2)
[:Qt,SS:] is non empty V203() V204() V205() Element of bool the carrier of [:x,I[01]:]
y .: [:Qt,SS:] is Element of bool the carrier of (Tunit_circle 2)
dom ((f ") * (y | [:a,SS:])) is Element of bool the carrier of [:x,I[01]:]
[:a,G:] is non empty V203() V204() V205() Element of bool the carrier of [:x,I[01]:]
sM0 | [:a,G:] is Relation-like the carrier of [:(x | ft),(I[01] | G):] -defined the carrier of R^1 -valued Function-like V203() V204() V205() Element of bool [: the carrier of [:(x | ft),(I[01] | G):], the carrier of R^1:]
x | a is non empty strict TopSpace-like open SubSpace of x
the carrier of (x | a) is non empty set
[:(x | a),(I[01] | G):] is non empty strict TopSpace-like TopStruct
the carrier of [:(x | a),(I[01] | G):] is non empty set
dom (sM0 | [:a,G:]) is Element of bool the carrier of [:(x | ft),(I[01] | G):]
rng (sM0 | [:a,G:]) is V213() V214() V215() Element of bool the carrier of R^1
rng ((f ") * (y | [:a,SS:])) is V213() V214() V215() Element of bool the carrier of (R^1 | x)
bool the carrier of (R^1 | x) is non empty set
I[01] | SS is non empty strict TopSpace-like T_0 T_1 T_2 V302() SubSpace of I[01]
the carrier of (I[01] | SS) is non empty V213() V214() V215() set
[:(x | a),(I[01] | SS):] is non empty strict TopSpace-like TopStruct
the carrier of [:(x | a),(I[01] | SS):] is non empty set
[: the carrier of [:(x | a),(I[01] | SS):], the carrier of R^1:] is non empty V203() V204() V205() set
bool [: the carrier of [:(x | a),(I[01] | SS):], the carrier of R^1:] is non empty set
Fni1 is non empty Relation-like the carrier of [:(x | a),(I[01] | SS):] -defined the carrier of R^1 -valued Function-like V26( the carrier of [:(x | a),(I[01] | SS):]) quasi_total V203() V204() V205() Element of bool [: the carrier of [:(x | a),(I[01] | SS):], the carrier of R^1:]
(sM0 | [:a,G:]) +* Fni1 is Relation-like Function-like V203() V204() V205() set
[: the carrier of [:(x | a),(I[01] | G):], the carrier of R^1:] is non empty V203() V204() V205() set
bool [: the carrier of [:(x | a),(I[01] | G):], the carrier of R^1:] is non empty set
rng ((sM0 | [:a,G:]) +* Fni1) is V213() V214() V215() set
rng Fni1 is V213() V214() V215() Element of bool the carrier of R^1
(rng (sM0 | [:a,G:])) \/ (rng Fni1) is V213() V214() V215() Element of bool the carrier of R^1
dom ((sM0 | [:a,G:]) +* Fni1) is set
[:a,G:] \/ [:a,SS:] is non empty Element of bool the carrier of [:x,I[01]:]
rng f is Element of bool the carrier of ((Tunit_circle 2) | ft1)
ff is Relation-like Function-like set
ff " is Relation-like Function-like set
K0 is set
[:a,{(yt . Ft)}:] is non empty V203() V204() V205() set
sM0 .: [:a,{(yt . Ft)}:] is V213() V214() V215() Element of bool the carrier of R^1
K0 is set
gF is Element of the carrier of [:(x | g2),(I[01] | G):]
sM0 . gF is V11() ext-real real Element of REAL
dom G is Element of bool the carrier of [:(x | g2),(I[01] | sM1):]
G . gF is V11() ext-real real Element of REAL
[#] [:(x | a),(I[01] | G):] is non empty non proper open closed dense non boundary Element of bool the carrier of [:(x | a),(I[01] | G):]
bool the carrier of [:(x | a),(I[01] | G):] is non empty set
[#] [:(x | a),(I[01] | SS):] is non empty non proper open closed dense non boundary Element of bool the carrier of [:(x | a),(I[01] | SS):]
bool the carrier of [:(x | a),(I[01] | SS):] is non empty set
([#] [:(x | a),(I[01] | G):]) /\ ([#] [:(x | a),(I[01] | SS):]) is Element of bool the carrier of [:(x | a),(I[01] | SS):]
Fn2 is non empty Relation-like the carrier of [:(x | a),(I[01] | G):] -defined the carrier of R^1 -valued Function-like V26( the carrier of [:(x | a),(I[01] | G):]) quasi_total V203() V204() V205() Element of bool [: the carrier of [:(x | a),(I[01] | G):], the carrier of R^1:]
K0 is set
Fn2 . K0 is V11() ext-real real Element of REAL
Fni1 . K0 is V11() ext-real real Element of REAL
([#] [:(x | a),(I[01] | SS):]) /\ ([#] [:(x | a),(I[01] | G):]) is Element of bool the carrier of [:(x | a),(I[01] | G):]
sM0 . K0 is V11() ext-real real Element of REAL
[:a,G:] /\ [:a,SS:] is Element of bool the carrier of [:x,I[01]:]
G /\ SS is V213() V214() V215() Element of bool the carrier of I[01]
[:a,(G /\ SS):] is V203() V204() V205() Element of bool the carrier of [:x,I[01]:]
gF is Element of a
fF is V11() ext-real real Element of {(yt . Ft)}
[gF,fF] is Element of [:a,{(yt . Ft)}:]
{gF,fF} is non empty set
{gF} is non empty set
{{gF,fF},{gF}} is non empty set
(y | [:a,SS:]) . K0 is set
y . K0 is set
y | [:g2,G:] is Relation-like the carrier of [:x,I[01]:] -defined the carrier of (Tunit_circle 2) -valued Function-like Element of bool [: the carrier of [:x,I[01]:], the carrier of (Tunit_circle 2):]
(y | [:g2,G:]) . K0 is set
CircleMap . (sM0 . K0) is set
(CircleMap | x) . (sM0 . K0) is set
ff . (Fn2 . K0) is set
(ff ") . ((y | [:a,SS:]) . K0) is set
[: the carrier of [:(x | a),(I[01] | SS):], the carrier of (Tunit_circle 2):] is non empty set
bool [: the carrier of [:(x | a),(I[01] | SS):], the carrier of (Tunit_circle 2):] is non empty set
[: the carrier of [:(x | a),(I[01] | SS):], the carrier of ((Tunit_circle 2) | ft1):] is non empty set
bool [: the carrier of [:(x | a),(I[01] | SS):], the carrier of ((Tunit_circle 2) | ft1):] is non empty set
[:x,I[01]:] | [:a,SS:] is non empty strict TopSpace-like SubSpace of [:x,I[01]:]
gF is non empty Relation-like the carrier of [:(x | a),(I[01] | SS):] -defined the carrier of (Tunit_circle 2) -valued Function-like V26( the carrier of [:(x | a),(I[01] | SS):]) quasi_total Element of bool [: the carrier of [:(x | a),(I[01] | SS):], the carrier of (Tunit_circle 2):]
fF is non empty Relation-like the carrier of [:(x | a),(I[01] | SS):] -defined the carrier of ((Tunit_circle 2) | ft1) -valued Function-like V26( the carrier of [:(x | a),(I[01] | SS):]) quasi_total Element of bool [: the carrier of [:(x | a),(I[01] | SS):], the carrier of ((Tunit_circle 2) | ft1):]
(f ") * fF is non empty Relation-like the carrier of [:(x | a),(I[01] | SS):] -defined the carrier of (R^1 | x) -valued Function-like V26( the carrier of [:(x | a),(I[01] | SS):]) quasi_total V203() V204() V205() Element of bool [: the carrier of [:(x | a),(I[01] | SS):], the carrier of (R^1 | x):]
[: the carrier of [:(x | a),(I[01] | SS):], the carrier of (R^1 | x):] is non empty V203() V204() V205() set
bool [: the carrier of [:(x | a),(I[01] | SS):], the carrier of (R^1 | x):] is non empty set
K0 is Element of bool the carrier of [:(x | g2),(I[01] | G):]
[:(x | g2),(I[01] | G):] | K0 is strict TopSpace-like SubSpace of [:(x | g2),(I[01] | G):]
aN1 is non empty Element of bool the carrier of (x | g2)
(x | g2) | aN1 is non empty strict TopSpace-like SubSpace of x | g2
aS is non empty V213() V214() V215() Element of bool the carrier of (I[01] | G)
(I[01] | G) | aS is non empty strict TopSpace-like T_0 T_1 T_2 V302() SubSpace of I[01] | G
[:((x | g2) | aN1),((I[01] | G) | aS):] is non empty strict TopSpace-like TopStruct
[:(x | a),((I[01] | G) | aS):] is non empty strict TopSpace-like TopStruct
[:a, the carrier of I[01]:] is non empty V203() V204() V205() set
S | [:a, the carrier of I[01]:] is Relation-like the carrier of [:x,(Sspace 0[01]):] -defined the carrier of R^1 -valued Function-like V203() V204() V205() Element of bool [: the carrier of [:x,(Sspace 0[01]):], the carrier of R^1:]
G \/ SS is non empty V213() V214() V215() Element of bool the carrier of I[01]
S1 is non empty V213() V214() V215() Element of bool the carrier of I[01]
I[01] | S1 is non empty strict TopSpace-like T_0 T_1 T_2 V302() SubSpace of I[01]
[:(x | a),(I[01] | S1):] is non empty strict TopSpace-like TopStruct
the carrier of [:(x | a),(I[01] | S1):] is non empty set
[: the carrier of [:(x | a),(I[01] | S1):], the carrier of R^1:] is non empty V203() V204() V205() set
bool [: the carrier of [:(x | a),(I[01] | S1):], the carrier of R^1:] is non empty set
[:a,S1:] is non empty V203() V204() V205() Element of bool the carrier of [:x,I[01]:]
y | [:a,S1:] is Relation-like the carrier of [:x,I[01]:] -defined the carrier of (Tunit_circle 2) -valued Function-like Element of bool [: the carrier of [:x,I[01]:], the carrier of (Tunit_circle 2):]
the carrier of (I[01] | S1) is non empty V213() V214() V215() set
Fn1 is non empty Relation-like the carrier of [:(x | a),(I[01] | S1):] -defined the carrier of R^1 -valued Function-like V26( the carrier of [:(x | a),(I[01] | S1):]) quasi_total V203() V204() V205() Element of bool [: the carrier of [:(x | a),(I[01] | S1):], the carrier of R^1:]
CircleMap * Fn1 is non empty Relation-like the carrier of [:(x | a),(I[01] | S1):] -defined the carrier of (Tunit_circle 2) -valued Function-like V26( the carrier of [:(x | a),(I[01] | S1):]) quasi_total Element of bool [: the carrier of [:(x | a),(I[01] | S1):], the carrier of (Tunit_circle 2):]
[: the carrier of [:(x | a),(I[01] | S1):], the carrier of (Tunit_circle 2):] is non empty set
bool [: the carrier of [:(x | a),(I[01] | S1):], the carrier of (Tunit_circle 2):] is non empty set
Fn1 | [: the carrier of x,{0}:] is Relation-like the carrier of [:(x | a),(I[01] | S1):] -defined the carrier of R^1 -valued Function-like V203() V204() V205() Element of bool [: the carrier of [:(x | a),(I[01] | S1):], the carrier of R^1:]
dom (Fn1 | [: the carrier of x,{0}:]) is Element of bool the carrier of [:(x | a),(I[01] | S1):]
bool the carrier of [:(x | a),(I[01] | S1):] is non empty set
dom Fn1 is Element of bool the carrier of [:(x | a),(I[01] | S1):]
(dom Fn1) /\ [: the carrier of x,{0}:] is Element of bool the carrier of [:(x | a),(I[01] | S1):]
a /\ the carrier of x is Element of bool the carrier of x
S1 /\ {0} is V213() V214() V215() V216() V217() V218() V317() Element of bool REAL
[:(a /\ the carrier of x),(S1 /\ {0}):] is RAT -valued INT -valued V203() V204() V205() V206() set
[:a,(S1 /\ {0}):] is RAT -valued INT -valued V203() V204() V205() V206() set
[:a,{0}:] is non empty RAT -valued INT -valued V203() V204() V205() V206() set
F1 is set
(Fn1 | [: the carrier of x,{0}:]) . F1 is V11() ext-real real Element of REAL
(S | [:a, the carrier of I[01]:]) . F1 is V11() ext-real real Element of REAL
[:g2, the carrier of I[01]:] is non empty V203() V204() V205() set
F2 is set
hS is set
[F2,hS] is set
{F2,hS} is non empty set
{F2} is non empty set
{{F2,hS},{F2}} is non empty set
dom Fni1 is Element of bool the carrier of [:(x | a),(I[01] | SS):]
Fn1 . F1 is V11() ext-real real Element of REAL
(sM0 | [:a,G:]) . F1 is V11() ext-real real Element of REAL
sM0 . F1 is V11() ext-real real Element of REAL
S | [:g2, the carrier of I[01]:] is Relation-like the carrier of [:x,(Sspace 0[01]):] -defined the carrier of R^1 -valued Function-like V203() V204() V205() Element of bool [: the carrier of [:x,(Sspace 0[01]):], the carrier of R^1:]
(S | [:g2, the carrier of I[01]:]) . F1 is V11() ext-real real Element of REAL
S . F1 is V11() ext-real real Element of REAL
dom Fni1 is Element of bool the carrier of [:(x | a),(I[01] | SS):]
b1 is set
b2 is set
[b1,b2] is set
{b1,b2} is non empty set
{b1} is non empty set
{{b1,b2},{b1}} is non empty set
[F2,(yt . Ft)] is set
{F2,(yt . Ft)} is non empty set
{{F2,(yt . Ft)},{F2}} is non empty set
S . F1 is V11() ext-real real Element of REAL
S | [:g2, the carrier of I[01]:] is Relation-like the carrier of [:x,(Sspace 0[01]):] -defined the carrier of R^1 -valued Function-like V203() V204() V205() Element of bool [: the carrier of [:x,(Sspace 0[01]):], the carrier of R^1:]
(S | [:g2, the carrier of I[01]:]) . F1 is V11() ext-real real Element of REAL
sM0 . F1 is V11() ext-real real Element of REAL
ff . ((S | [:a, the carrier of I[01]:]) . F1) is set
CircleMap . ((S | [:a, the carrier of I[01]:]) . F1) is set
CircleMap . (S . F1) is set
(CircleMap * S) . F1 is set
y . F1 is set
Fn1 . F1 is V11() ext-real real Element of REAL
Fni1 . F1 is V11() ext-real real Element of REAL
(y | [:a,SS:]) . F1 is set
(ff ") . ((y | [:a,SS:]) . F1) is set
(ff ") . (y . F1) is set
dom Fni1 is Element of bool the carrier of [:(x | a),(I[01] | SS):]
rng Fn1 is V213() V214() V215() Element of bool the carrier of R^1
dom (CircleMap * Fn1) is Element of bool the carrier of [:(x | a),(I[01] | S1):]
F1 is set
(CircleMap * Fn1) . F1 is set
y . F1 is set
dom Fni1 is Element of bool the carrier of [:(x | a),(I[01] | SS):]
y .: [:a,SS:] is Element of bool the carrier of (Tunit_circle 2)
[:Qt,SS:] is non empty V203() V204() V205() Element of bool the carrier of [:x,I[01]:]
y .: [:Qt,SS:] is Element of bool the carrier of (Tunit_circle 2)
dom (ff ") is set
y " (dom (ff ")) is Element of bool the carrier of [:x,I[01]:]
y * (ff ") is Relation-like Function-like set
dom (y * (ff ")) is set
Fn1 . F1 is V11() ext-real real Element of REAL
CircleMap . (Fn1 . F1) is set
Fni1 . F1 is V11() ext-real real Element of REAL
CircleMap . (Fni1 . F1) is set
(y | [:a,SS:]) . F1 is set
(f ") . ((y | [:a,SS:]) . F1) is V11() ext-real real Element of REAL
CircleMap . ((f ") . ((y | [:a,SS:]) . F1)) is set
(f ") . (y . F1) is V11() ext-real real Element of REAL
CircleMap . ((f ") . (y . F1)) is set
(y * (ff ")) . F1 is set
CircleMap . ((y * (ff ")) . F1) is set
(y * (ff ")) * CircleMap is Relation-like Function-like set
((y * (ff ")) * CircleMap) . F1 is set
(ff ") * CircleMap is Relation-like Function-like set
y * ((ff ") * CircleMap) is Relation-like Function-like set
(y * ((ff ") * CircleMap)) . F1 is set
((ff ") * CircleMap) . (y . F1) is set
dom Fni1 is Element of bool the carrier of [:(x | a),(I[01] | SS):]
Fn1 . F1 is V11() ext-real real Element of REAL
CircleMap . (Fn1 . F1) is set
(sM0 | [:a,G:]) . F1 is V11() ext-real real Element of REAL
CircleMap . ((sM0 | [:a,G:]) . F1) is set
sM0 . F1 is V11() ext-real real Element of REAL
CircleMap . (sM0 . F1) is set
(CircleMap * sM0) . F1 is set
dom Fni1 is Element of bool the carrier of [:(x | a),(I[01] | SS):]
[#] (I[01] | S1) is non empty non proper open closed dense non boundary V213() V214() V215() Element of bool the carrier of (I[01] | S1)
bool the carrier of (I[01] | S1) is non empty set
[#] (I[01] | G) is non empty non proper open closed dense non boundary V213() V214() V215() Element of bool the carrier of (I[01] | G)
[#] (I[01] | SS) is non empty non proper open closed dense non boundary V213() V214() V215() Element of bool the carrier of (I[01] | SS)
bool the carrier of (I[01] | SS) is non empty set
F1 is V213() V214() V215() Element of bool the carrier of (I[01] | S1)
F2 is V213() V214() V215() Element of bool the carrier of (I[01] | S1)
hS is V213() V214() V215() Element of bool the carrier of I[01]
hSS is V213() V214() V215() Element of bool the carrier of I[01]
Fn2 +* Fni1 is Relation-like Function-like V203() V204() V205() set
b1 is non empty Relation-like the carrier of [:(x | a),(I[01] | S1):] -defined the carrier of R^1 -valued Function-like V26( the carrier of [:(x | a),(I[01] | S1):]) quasi_total V203() V204() V205() Element of bool [: the carrier of [:(x | a),(I[01] | S1):], the carrier of R^1:]
(dom y) /\ [:a,S1:] is Element of bool the carrier of [:x,I[01]:]
dom (S | [:a, the carrier of I[01]:]) is Element of bool the carrier of [:x,(Sspace 0[01]):]
(dom S) /\ [:a, the carrier of I[01]:] is Element of bool the carrier of [:x,(Sspace 0[01]):]
the carrier of x /\ a is Element of bool the carrier of x
{0} /\ the carrier of I[01] is V213() V214() V215() V216() V217() V218() V317() Element of bool REAL
[:( the carrier of x /\ a),({0} /\ the carrier of I[01]):] is RAT -valued INT -valued V203() V204() V205() V206() set
[:a,({0} /\ the carrier of I[01]):] is RAT -valued INT -valued V203() V204() V205() V206() set
yt . 0 is V11() ext-real real Element of REAL
[.0,(yt . 0).] is V213() V214() V215() V320() Element of bool REAL
[.0,(yt . (len yt)).] is V213() V214() V215() V320() Element of bool REAL
Ft is non empty open Element of bool the carrier of x
x | Ft is non empty strict TopSpace-like open SubSpace of x
ft0 is non empty V213() V214() V215() Element of bool the carrier of I[01]
I[01] | ft0 is non empty strict TopSpace-like T_0 T_1 T_2 V302() SubSpace of I[01]
[:(x | Ft),(I[01] | ft0):] is non empty strict TopSpace-like TopStruct
the carrier of [:(x | Ft),(I[01] | ft0):] is non empty set
[: the carrier of [:(x | Ft),(I[01] | ft0):], the carrier of R^1:] is non empty V203() V204() V205() set
bool [: the carrier of [:(x | Ft),(I[01] | ft0):], the carrier of R^1:] is non empty set
ft1 is non empty Relation-like the carrier of [:(x | Ft),(I[01] | ft0):] -defined the carrier of R^1 -valued Function-like V26( the carrier of [:(x | Ft),(I[01] | ft0):]) quasi_total V203() V204() V205() Element of bool [: the carrier of [:(x | Ft),(I[01] | ft0):], the carrier of R^1:]
[:Ft,ft0:] is non empty V203() V204() V205() Element of bool the carrier of [:x,I[01]:]
y | [:Ft,ft0:] is Relation-like the carrier of [:x,I[01]:] -defined the carrier of (Tunit_circle 2) -valued Function-like Element of bool [: the carrier of [:x,I[01]:], the carrier of (Tunit_circle 2):]
CircleMap * ft1 is non empty Relation-like the carrier of [:(x | Ft),(I[01] | ft0):] -defined the carrier of (Tunit_circle 2) -valued Function-like V26( the carrier of [:(x | Ft),(I[01] | ft0):]) quasi_total Element of bool [: the carrier of [:(x | Ft),(I[01] | ft0):], the carrier of (Tunit_circle 2):]
[: the carrier of [:(x | Ft),(I[01] | ft0):], the carrier of (Tunit_circle 2):] is non empty set
bool [: the carrier of [:(x | Ft),(I[01] | ft0):], the carrier of (Tunit_circle 2):] is non empty set
ft1 | [: the carrier of x,{0}:] is Relation-like the carrier of [:(x | Ft),(I[01] | ft0):] -defined the carrier of R^1 -valued Function-like V203() V204() V205() Element of bool [: the carrier of [:(x | Ft),(I[01] | ft0):], the carrier of R^1:]
[:Ft, the carrier of I[01]:] is non empty V203() V204() V205() set
S | [:Ft, the carrier of I[01]:] is Relation-like the carrier of [:x,(Sspace 0[01]):] -defined the carrier of R^1 -valued Function-like V203() V204() V205() Element of bool [: the carrier of [:x,(Sspace 0[01]):], the carrier of R^1:]
ft1 . x is V11() ext-real real Element of REAL
[:(x | Ft),I[01]:] is non empty strict TopSpace-like TopStruct
the carrier of [:(x | Ft),I[01]:] is non empty set
[: the carrier of [:(x | Ft),I[01]:], the carrier of R^1:] is non empty V203() V204() V205() set
bool [: the carrier of [:(x | Ft),I[01]:], the carrier of R^1:] is non empty set
ftn is V11() ext-real real Element of the carrier of R^1
y | [:Ft, the carrier of I[01]:] is Relation-like the carrier of [:x,I[01]:] -defined the carrier of (Tunit_circle 2) -valued Function-like Element of bool [: the carrier of [:x,I[01]:], the carrier of (Tunit_circle 2):]
ft is non empty Relation-like the carrier of [:(x | Ft),I[01]:] -defined the carrier of R^1 -valued Function-like V26( the carrier of [:(x | Ft),I[01]:]) quasi_total V203() V204() V205() Element of bool [: the carrier of [:(x | Ft),I[01]:], the carrier of R^1:]
ft . x is V11() ext-real real Element of REAL
CircleMap * ft is non empty Relation-like the carrier of [:(x | Ft),I[01]:] -defined the carrier of (Tunit_circle 2) -valued Function-like V26( the carrier of [:(x | Ft),I[01]:]) quasi_total Element of bool [: the carrier of [:(x | Ft),I[01]:], the carrier of (Tunit_circle 2):]
[: the carrier of [:(x | Ft),I[01]:], the carrier of (Tunit_circle 2):] is non empty set
bool [: the carrier of [:(x | Ft),I[01]:], the carrier of (Tunit_circle 2):] is non empty set
ft | [: the carrier of x,{0}:] is Relation-like the carrier of [:(x | Ft),I[01]:] -defined the carrier of R^1 -valued Function-like V203() V204() V205() Element of bool [: the carrier of [:(x | Ft),I[01]:], the carrier of R^1:]
G is non empty Relation-like the carrier of [:(x | Ft),I[01]:] -defined the carrier of R^1 -valued Function-like V26( the carrier of [:(x | Ft),I[01]:]) quasi_total V203() V204() V205() Element of bool [: the carrier of [:(x | Ft),I[01]:], the carrier of R^1:]
CircleMap * G is non empty Relation-like the carrier of [:(x | Ft),I[01]:] -defined the carrier of (Tunit_circle 2) -valued Function-like V26( the carrier of [:(x | Ft),I[01]:]) quasi_total Element of bool [: the carrier of [:(x | Ft),I[01]:], the carrier of (Tunit_circle 2):]
G | [: the carrier of x,{0}:] is Relation-like the carrier of [:(x | Ft),I[01]:] -defined the carrier of R^1 -valued Function-like V203() V204() V205() Element of bool [: the carrier of [:(x | Ft),I[01]:], the carrier of R^1:]
dom ft is Element of bool the carrier of [:(x | Ft),I[01]:]
bool the carrier of [:(x | Ft),I[01]:] is non empty set
the carrier of (x | Ft) is non empty set
[: the carrier of (x | Ft), the carrier of I[01]:] is non empty V203() V204() V205() set
dom G is Element of bool the carrier of [:(x | Ft),I[01]:]
sM0 is ordinal natural V11() ext-real non negative real integer V34() V213() V214() V215() V216() V217() V218() V317() Element of NAT
yt . sM0 is V11() ext-real real Element of REAL
[.0,(yt . sM0).] is V213() V214() V215() V320() Element of bool REAL
sM0 + 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
yt . (sM0 + 1) is V11() ext-real real Element of REAL
[.0,(yt . (sM0 + 1)).] is V213() V214() V215() V320() Element of bool REAL
ft2 is non empty V213() V214() V215() Element of bool the carrier of I[01]
[:Ft,ft2:] is non empty V203() V204() V205() Element of bool the carrier of [:x,I[01]:]
ft | [:Ft,ft2:] is Relation-like the carrier of [:(x | Ft),I[01]:] -defined the carrier of R^1 -valued Function-like V203() V204() V205() Element of bool [: the carrier of [:(x | Ft),I[01]:], the carrier of R^1:]
dom (ft | [:Ft,ft2:]) is Element of bool the carrier of [:(x | Ft),I[01]:]
G | [:Ft,ft2:] is Relation-like the carrier of [:(x | Ft),I[01]:] -defined the carrier of R^1 -valued Function-like V203() V204() V205() Element of bool [: the carrier of [:(x | Ft),I[01]:], the carrier of R^1:]
sM1 is set
(ft | [:Ft,ft2:]) . sM1 is V11() ext-real real Element of REAL
(G | [:Ft,ft2:]) . sM1 is V11() ext-real real Element of REAL
[: the carrier of x,ft2:] is non empty V203() V204() V205() set
ft . sM1 is V11() ext-real real Element of REAL
(ft | [: the carrier of x,{0}:]) . sM1 is V11() ext-real real Element of REAL
G . sM1 is V11() ext-real real Element of REAL
dom (G | [:Ft,ft2:]) is Element of bool the carrier of [:(x | Ft),I[01]:]
[.(yt . sM0),(yt . (sM0 + 1)).] is V213() V214() V215() V320() Element of bool REAL
sM1 is non empty V213() V214() V215() Element of bool the carrier of I[01]
[:Ft,sM1:] is non empty V203() V204() V205() Element of bool the carrier of [:x,I[01]:]
ft | [:Ft,sM1:] is Relation-like the carrier of [:(x | Ft),I[01]:] -defined the carrier of R^1 -valued Function-like V203() V204() V205() Element of bool [: the carrier of [:(x | Ft),I[01]:], the carrier of R^1:]
G | [:Ft,sM1:] is Relation-like the carrier of [:(x | Ft),I[01]:] -defined the carrier of R^1 -valued Function-like V203() V204() V205() Element of bool [: the carrier of [:(x | Ft),I[01]:], the carrier of R^1:]
sM1 is non empty V213() V214() V215() Element of bool the carrier of I[01]
[:Ft,sM1:] is non empty V203() V204() V205() Element of bool the carrier of [:x,I[01]:]
ft | [:Ft,sM1:] is Relation-like the carrier of [:(x | Ft),I[01]:] -defined the carrier of R^1 -valued Function-like V203() V204() V205() Element of bool [: the carrier of [:(x | Ft),I[01]:], the carrier of R^1:]
G | [:Ft,sM1:] is Relation-like the carrier of [:(x | Ft),I[01]:] -defined the carrier of R^1 -valued Function-like V203() V204() V205() Element of bool [: the carrier of [:(x | Ft),I[01]:], the carrier of R^1:]
ft2 is V213() V214() V215() Element of bool the carrier of I[01]
sM1 \/ ft2 is non empty V213() V214() V215() Element of bool the carrier of I[01]
Qt is non empty V213() V214() V215() Element of bool the carrier of I[01]
[:Ft,Qt:] is non empty V203() V204() V205() Element of bool the carrier of [:x,I[01]:]
ft | [:Ft,Qt:] is Relation-like the carrier of [:(x | Ft),I[01]:] -defined the carrier of R^1 -valued Function-like V203() V204() V205() Element of bool [: the carrier of [:(x | Ft),I[01]:], the carrier of R^1:]
G | [:Ft,Qt:] is Relation-like the carrier of [:(x | Ft),I[01]:] -defined the carrier of R^1 -valued Function-like V203() V204() V205() Element of bool [: the carrier of [:(x | Ft),I[01]:], the carrier of R^1:]
dom (ft | [:Ft,Qt:]) is Element of bool the carrier of [:(x | Ft),I[01]:]
[:Qt,ft2:] is V203() V204() V205() Element of bool the carrier of [:x,I[01]:]
y .: [:Qt,ft2:] is Element of bool the carrier of (Tunit_circle 2)
Qt is non empty Element of bool the carrier of (Tunit_circle 2)
CircleMap " Qt is V213() V214() V215() Element of bool the carrier of R^1
(Tunit_circle 2) | Qt is non empty strict TopSpace-like SubSpace of Tunit_circle 2
the carrier of ((Tunit_circle 2) | Qt) is non empty set
G is mutually-disjoint open Element of bool (bool the carrier of R^1)
union G is V213() V214() V215() Element of bool the carrier of R^1
F1 is set
(ft | [:Ft,Qt:]) . F1 is V11() ext-real real Element of REAL
(G | [:Ft,Qt:]) . F1 is V11() ext-real real Element of REAL
x is set
x1 is set
[x,x1] is set
{x,x1} is non empty set
{x} is non empty set
{{x,x1},{x}} is non empty set
[x,(yt . sM0)] is set
{x,(yt . sM0)} is non empty set
{{x,(yt . sM0)},{x}} is non empty set
y . [x,(yt . sM0)] is set
x2 is non empty Element of bool the carrier of x
[:x2,ft2:] is V203() V204() V205() Element of bool the carrier of [:x,I[01]:]
G | [:x2,ft2:] is Relation-like the carrier of [:(x | Ft),I[01]:] -defined the carrier of R^1 -valued Function-like V203() V204() V205() Element of bool [: the carrier of [:(x | Ft),I[01]:], the carrier of R^1:]
dom (G | [:x2,ft2:]) is Element of bool the carrier of [:(x | Ft),I[01]:]
XZZ is Element of bool the carrier of [:(x | Ft),I[01]:]
ft .: XZZ is V213() V214() V215() Element of bool the carrier of R^1
Uit is set
union G is set
Uit is Element of the carrier of [:(x | Ft),I[01]:]
ft . Uit is V11() ext-real real Element of the carrier of R^1
y . Uit is set
CircleMap . (ft . Uit) is Element of the carrier of (Tunit_circle 2)
(CircleMap * ft) . Uit is Element of the carrier of (Tunit_circle 2)
G .: XZZ is V213() V214() V215() Element of bool the carrier of R^1
Uit is set
union G is set
Uit is Element of the carrier of [:(x | Ft),I[01]:]
G . Uit is V11() ext-real real Element of the carrier of R^1
CircleMap . (G . Uit) is Element of the carrier of (Tunit_circle 2)
(CircleMap * G) . Uit is Element of the carrier of (Tunit_circle 2)
y . Uit is set
ft . [x,(yt . sM0)] is V11() ext-real real Element of REAL
(ft | [:Ft,sM1:]) . [x,(yt . sM0)] is V11() ext-real real Element of REAL
G . [x,(yt . sM0)] is V11() ext-real real Element of REAL
(CircleMap * G) . [x,(yt . sM0)] is set
CircleMap . (G . [x,(yt . sM0)]) is set
Uit is set
(CircleMap * ft) . [x,(yt . sM0)] is set
CircleMap . (ft . [x,(yt . sM0)]) is set
Uit is set
f is non empty V213() V214() V215() Element of bool the carrier of R^1
f is non empty V213() V214() V215() Element of bool the carrier of R^1
CircleMap | f 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):]
dom (CircleMap | f) is V213() V214() V215() Element of bool the carrier of R^1
rng (CircleMap | f) is Element of bool the carrier of (Tunit_circle 2)
Uith is set
b is set
(CircleMap | f) . b is set
CircleMap . b is set
R^1 | f is non empty strict TopSpace-like V302() SubSpace of R^1
the carrier of (R^1 | f) is non empty V213() V214() V215() set
[: the carrier of (R^1 | f), the carrier of ((Tunit_circle 2) | Qt):] is non empty set
bool [: the carrier of (R^1 | f), the carrier of ((Tunit_circle 2) | Qt):] is non empty set
ft | [:x2,ft2:] is Relation-like the carrier of [:(x | Ft),I[01]:] -defined the carrier of R^1 -valued Function-like V203() V204() V205() Element of bool [: the carrier of [:(x | Ft),I[01]:], the carrier of R^1:]
dom (ft | [:x2,ft2:]) is Element of bool the carrier of [:(x | Ft),I[01]:]
rng (G | [:x2,ft2:]) is V213() V214() V215() Element of bool the carrier of R^1
Uith is non empty Relation-like the carrier of (R^1 | f) -defined the carrier of ((Tunit_circle 2) | Qt) -valued Function-like V26( the carrier of (R^1 | f)) quasi_total Element of bool [: the carrier of (R^1 | f), the carrier of ((Tunit_circle 2) | Qt):]
dom Uith is V213() V214() V215() Element of bool the carrier of (R^1 | f)
bool the carrier of (R^1 | f) is non empty set
b is set
a is set
(G | [:x2,ft2:]) . a is V11() ext-real real Element of REAL
G . a is V11() ext-real real Element of REAL
rng (ft | [:x2,ft2:]) is V213() V214() V215() Element of bool the carrier of R^1
b is set
a is set
(ft | [:x2,ft2:]) . a is V11() ext-real real Element of REAL
ft . a is V11() ext-real real Element of REAL
Uith * (ft | [:x2,ft2:]) is Relation-like the carrier of [:(x | Ft),I[01]:] -defined the carrier of ((Tunit_circle 2) | Qt) -valued Function-like Element of bool [: the carrier of [:(x | Ft),I[01]:], the carrier of ((Tunit_circle 2) | Qt):]
[: the carrier of [:(x | Ft),I[01]:], the carrier of ((Tunit_circle 2) | Qt):] is non empty set
bool [: the carrier of [:(x | Ft),I[01]:], the carrier of ((Tunit_circle 2) | Qt):] is non empty set
dom (Uith * (ft | [:x2,ft2:])) is Element of bool the carrier of [:(x | Ft),I[01]:]
Uith * (G | [:x2,ft2:]) is Relation-like the carrier of [:(x | Ft),I[01]:] -defined the carrier of ((Tunit_circle 2) | Qt) -valued Function-like Element of bool [: the carrier of [:(x | Ft),I[01]:], the carrier of ((Tunit_circle 2) | Qt):]
b is set
(Uith * (ft | [:x2,ft2:])) . b is set
(Uith * (G | [:x2,ft2:])) . b is set
ft . b is V11() ext-real real Element of REAL
ft .: [:x2,ft2:] is V213() V214() V215() Element of bool the carrier of R^1
G . b is V11() ext-real real Element of REAL
G .: [:x2,ft2:] is V213() V214() V215() Element of bool the carrier of R^1
Uith * ft is Relation-like the carrier of [:(x | Ft),I[01]:] -defined the carrier of ((Tunit_circle 2) | Qt) -valued Function-like Element of bool [: the carrier of [:(x | Ft),I[01]:], the carrier of ((Tunit_circle 2) | Qt):]
(Uith * ft) | [:x2,ft2:] is Relation-like the carrier of [:(x | Ft),I[01]:] -defined the carrier of ((Tunit_circle 2) | Qt) -valued Function-like Element of bool [: the carrier of [:(x | Ft),I[01]:], the carrier of ((Tunit_circle 2) | Qt):]
((Uith * ft) | [:x2,ft2:]) . b is set
(Uith * ft) . b is set
Uith . (ft . b) is set
CircleMap . (ft . b) is set
(CircleMap * ft) . b is set
CircleMap . (G . b) is set
Uith . (G . b) is set
Uith * G is Relation-like the carrier of [:(x | Ft),I[01]:] -defined the carrier of ((Tunit_circle 2) | Qt) -valued Function-like Element of bool [: the carrier of [:(x | Ft),I[01]:], the carrier of ((Tunit_circle 2) | Qt):]
(Uith * G) . b is set
(Uith * G) | [:x2,ft2:] is Relation-like the carrier of [:(x | Ft),I[01]:] -defined the carrier of ((Tunit_circle 2) | Qt) -valued Function-like Element of bool [: the carrier of [:(x | Ft),I[01]:], the carrier of ((Tunit_circle 2) | Qt):]
((Uith * G) | [:x2,ft2:]) . b is set
dom (Uith * (G | [:x2,ft2:])) is Element of bool the carrier of [:(x | Ft),I[01]:]
ft . F1 is V11() ext-real real Element of REAL
(ft | [:x2,ft2:]) . F1 is V11() ext-real real Element of REAL
(G | [:x2,ft2:]) . F1 is V11() ext-real real Element of REAL
G . F1 is V11() ext-real real Element of REAL
ft . F1 is V11() ext-real real Element of REAL
(ft | [:Ft,sM1:]) . F1 is V11() ext-real real Element of REAL
G . F1 is V11() ext-real real Element of REAL
dom (G | [:Ft,Qt:]) is Element of bool the carrier of [:(x | Ft),I[01]:]
sM0 is non empty V213() V214() V215() Element of bool the carrier of I[01]
[:Ft,sM0:] is non empty V203() V204() V205() Element of bool the carrier of [:x,I[01]:]
ft | [:Ft,sM0:] is Relation-like the carrier of [:(x | Ft),I[01]:] -defined the carrier of R^1 -valued Function-like V203() V204() V205() Element of bool [: the carrier of [:(x | Ft),I[01]:], the carrier of R^1:]
G | [:Ft,sM0:] is Relation-like the carrier of [:(x | Ft),I[01]:] -defined the carrier of R^1 -valued Function-like V203() V204() V205() Element of bool [: the carrier of [:(x | Ft),I[01]:], the carrier of R^1:]
x is non empty Relation-like the carrier of [:x,I[01]:] -defined the carrier of R^1 -valued Function-like V26( the carrier of [:x,I[01]:]) quasi_total V203() V204() V205() Element of bool [: the carrier of [:x,I[01]:], the carrier of R^1:]
CircleMap * x is non empty Relation-like the carrier of [:x,I[01]:] -defined the carrier of (Tunit_circle 2) -valued Function-like V26( the carrier of [:x,I[01]:]) quasi_total Element of bool [: the carrier of [:x,I[01]:], the carrier of (Tunit_circle 2):]
x | [: the carrier of x,{0}:] is Relation-like the carrier of [:x,I[01]:] -defined the carrier of R^1 -valued Function-like V203() V204() V205() Element of bool [: the carrier of [:x,I[01]:], the carrier of R^1:]
F is Element of bool the carrier of x
x | F is strict TopSpace-like SubSpace of x
[:(x | F),I[01]:] is strict TopSpace-like TopStruct
the carrier of [:(x | F),I[01]:] is set
[: the carrier of [:(x | F),I[01]:], the carrier of R^1:] is V203() V204() V205() set
bool [: the carrier of [:(x | F),I[01]:], the carrier of R^1:] is non empty set
ftm is Relation-like the carrier of [:(x | F),I[01]:] -defined the carrier of R^1 -valued Function-like V26( the carrier of [:(x | F),I[01]:]) quasi_total V203() V204() V205() Element of bool [: the carrier of [:(x | F),I[01]:], the carrier of R^1:]
dom ftm is Element of bool the carrier of [:(x | F),I[01]:]
bool the carrier of [:(x | F),I[01]:] is non empty set
the carrier of (x | F) is set
[: the carrier of (x | F), the carrier of I[01]:] is V203() V204() V205() set
[:F, the carrier of I[01]:] is V203() V204() V205() set
F is Element of the carrier of [:x,I[01]:]
ftm is Element of the carrier of x
{ftm} is non empty connected compact Element of bool the carrier of x
[:{ftm}, the carrier of I[01]:] is non empty V203() V204() V205() set
yt is V11() ext-real real Element of the carrier of I[01]
[ftm,yt] is Element of the carrier of [:x,I[01]:]
{ftm,yt} is non empty set
{ftm} is non empty set
{{ftm,yt},{ftm}} is non empty set
Pt is non empty open Element of bool the carrier of x
x | Pt is non empty strict TopSpace-like open SubSpace of x
[:(x | Pt),I[01]:] is non empty strict TopSpace-like TopStruct
the carrier of [:(x | Pt),I[01]:] is non empty set
[: the carrier of [:(x | Pt),I[01]:], the carrier of R^1:] is non empty V203() V204() V205() set
bool [: the carrier of [:(x | Pt),I[01]:], the carrier of R^1:] is non empty set
Qt is non empty open Element of bool the carrier of x
x | Qt is non empty strict TopSpace-like open SubSpace of x
[:(x | Qt),I[01]:] is non empty strict TopSpace-like TopStruct
the carrier of [:(x | Qt),I[01]:] is non empty set
[: the carrier of [:(x | Qt),I[01]:], the carrier of R^1:] is non empty V203() V204() V205() set
bool [: the carrier of [:(x | Qt),I[01]:], the carrier of R^1:] is non empty set
[:Qt, the carrier of I[01]:] is non empty V203() V204() V205() set
y | [:Qt, the carrier of I[01]:] is Relation-like the carrier of [:x,I[01]:] -defined the carrier of (Tunit_circle 2) -valued Function-like Element of bool [: the carrier of [:x,I[01]:], the carrier of (Tunit_circle 2):]
S | [:Qt, the carrier of I[01]:] is Relation-like the carrier of [:x,(Sspace 0[01]):] -defined the carrier of R^1 -valued Function-like V203() V204() V205() Element of bool [: the carrier of [:x,(Sspace 0[01]):], the carrier of R^1:]
[:Pt, the carrier of I[01]:] is non empty V203() V204() V205() set
y | [:Pt, the carrier of I[01]:] is Relation-like the carrier of [:x,I[01]:] -defined the carrier of (Tunit_circle 2) -valued Function-like Element of bool [: the carrier of [:x,I[01]:], the carrier of (Tunit_circle 2):]
S | [:Pt, the carrier of I[01]:] is Relation-like the carrier of [:x,(Sspace 0[01]):] -defined the carrier of R^1 -valued Function-like V203() V204() V205() Element of bool [: the carrier of [:x,(Sspace 0[01]):], the carrier of R^1:]
Ft is non empty Relation-like the carrier of [:(x | Pt),I[01]:] -defined the carrier of R^1 -valued Function-like V26( the carrier of [:(x | Pt),I[01]:]) quasi_total V203() V204() V205() Element of bool [: the carrier of [:(x | Pt),I[01]:], the carrier of R^1:]
CircleMap * Ft is non empty Relation-like the carrier of [:(x | Pt),I[01]:] -defined the carrier of (Tunit_circle 2) -valued Function-like V26( the carrier of [:(x | Pt),I[01]:]) quasi_total Element of bool [: the carrier of [:(x | Pt),I[01]:], the carrier of (Tunit_circle 2):]
[: the carrier of [:(x | Pt),I[01]:], the carrier of (Tunit_circle 2):] is non empty set
bool [: the carrier of [:(x | Pt),I[01]:], the carrier of (Tunit_circle 2):] is non empty set
Ft | [: the carrier of x,{0}:] is Relation-like the carrier of [:(x | Pt),I[01]:] -defined the carrier of R^1 -valued Function-like V203() V204() V205() Element of bool [: the carrier of [:(x | Pt),I[01]:], the carrier of R^1:]
Ft | [:{ftm}, the carrier of I[01]:] is Relation-like the carrier of [:(x | Pt),I[01]:] -defined the carrier of R^1 -valued Function-like V203() V204() V205() Element of bool [: the carrier of [:(x | Pt),I[01]:], the carrier of R^1:]
ft0 is non empty Relation-like the carrier of [:(x | Qt),I[01]:] -defined the carrier of R^1 -valued Function-like V26( the carrier of [:(x | Qt),I[01]:]) quasi_total V203() V204() V205() Element of bool [: the carrier of [:(x | Qt),I[01]:], the carrier of R^1:]
CircleMap * ft0 is non empty Relation-like the carrier of [:(x | Qt),I[01]:] -defined the carrier of (Tunit_circle 2) -valued Function-like V26( the carrier of [:(x | Qt),I[01]:]) quasi_total Element of bool [: the carrier of [:(x | Qt),I[01]:], the carrier of (Tunit_circle 2):]
[: the carrier of [:(x | Qt),I[01]:], the carrier of (Tunit_circle 2):] is non empty set
bool [: the carrier of [:(x | Qt),I[01]:], the carrier of (Tunit_circle 2):] is non empty set
ft0 | [: the carrier of x,{0}:] is Relation-like the carrier of [:(x | Qt),I[01]:] -defined the carrier of R^1 -valued Function-like V203() V204() V205() Element of bool [: the carrier of [:(x | Qt),I[01]:], the carrier of R^1:]
ft0 | [:{ftm}, the carrier of I[01]:] is Relation-like the carrier of [:(x | Qt),I[01]:] -defined the carrier of R^1 -valued Function-like V203() V204() V205() Element of bool [: the carrier of [:(x | Qt),I[01]:], the carrier of R^1:]
ft1 is non empty Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V203() V204() V205() FinSequence of REAL
ft1 . 1 is V11() ext-real real Element of REAL
len ft1 is ordinal natural V11() ext-real non negative real integer V34() V213() V214() V215() V216() V217() V218() V317() Element of NAT
ft1 . (len ft1) is V11() ext-real real Element of REAL
dom ft1 is V213() V214() V215() V216() V217() V218() V317() Element of bool NAT
ftn is open Element of bool the carrier of x
ftn is open Element of bool the carrier of x
dom ft0 is Element of bool the carrier of [:(x | Qt),I[01]:]
bool the carrier of [:(x | Qt),I[01]:] is non empty set
the carrier of (x | Pt) is non empty set
[: the carrier of (x | Pt), the carrier of I[01]:] is non empty V203() V204() V205() set
the carrier of (x | Qt) is non empty set
[: the carrier of (x | Qt), the carrier of I[01]:] is non empty V203() V204() V205() set
dom Ft is Element of bool the carrier of [:(x | Pt),I[01]:]
bool the carrier of [:(x | Pt),I[01]:] is non empty set
G is ordinal natural V11() ext-real non negative real integer V34() V213() V214() V215() V216() V217() V218() V317() Element of NAT
ft1 . G is V11() ext-real real Element of REAL
[.0,(ft1 . G).] is V213() V214() V215() V320() Element of bool REAL
G + 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
ft1 . (G + 1) is V11() ext-real real Element of REAL
[.0,(ft1 . (G + 1)).] is V213() V214() V215() V320() Element of bool REAL
g2 is non empty V213() V214() V215() Element of bool the carrier of I[01]
[:{ftm},g2:] is non empty V203() V204() V205() Element of bool the carrier of [:x,I[01]:]
Ft | [:{ftm},g2:] is Relation-like the carrier of [:(x | Pt),I[01]:] -defined the carrier of R^1 -valued Function-like V203() V204() V205() Element of bool [: the carrier of [:(x | Pt),I[01]:], the carrier of R^1:]
dom (Ft | [:{ftm},g2:]) is Element of bool the carrier of [:(x | Pt),I[01]:]
ft0 | [:{ftm},g2:] is Relation-like the carrier of [:(x | Qt),I[01]:] -defined the carrier of R^1 -valued Function-like V203() V204() V205() Element of bool [: the carrier of [:(x | Qt),I[01]:], the carrier of R^1:]
ft2 is set
(Ft | [:{ftm},g2:]) . ft2 is V11() ext-real real Element of REAL
(ft0 | [:{ftm},g2:]) . ft2 is V11() ext-real real Element of REAL
[: the carrier of x,g2:] is non empty V203() V204() V205() set
Ft . ft2 is V11() ext-real real Element of REAL
(Ft | [: the carrier of x,{0}:]) . ft2 is V11() ext-real real Element of REAL
S . ft2 is V11() ext-real real Element of REAL
(S | [:Qt, the carrier of I[01]:]) . ft2 is V11() ext-real real Element of REAL
ft0 . ft2 is V11() ext-real real Element of REAL
dom (ft0 | [:{ftm},g2:]) is Element of bool the carrier of [:(x | Qt),I[01]:]
sM0 is ordinal natural V11() ext-real non negative real integer V34() V213() V214() V215() V216() V217() V218() V317() Element of NAT
ft1 . sM0 is V11() ext-real real Element of REAL
sM0 + 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
sM0 + 0 is ordinal natural V11() ext-real non negative real integer V34() V213() V214() V215() V216() V217() V218() V317() Element of NAT
ft1 . (sM0 + 1) is V11() ext-real real Element of REAL
[.(ft1 . G),(ft1 . (G + 1)).] is V213() V214() V215() V320() Element of bool REAL
g2 is non empty V213() V214() V215() Element of bool the carrier of I[01]
[:{ftm},g2:] is non empty V203() V204() V205() Element of bool the carrier of [:x,I[01]:]
Ft | [:{ftm},g2:] is Relation-like the carrier of [:(x | Pt),I[01]:] -defined the carrier of R^1 -valued Function-like V203() V204() V205() Element of bool [: the carrier of [:(x | Pt),I[01]:], the carrier of R^1:]
ft0 | [:{ftm},g2:] is Relation-like the carrier of [:(x | Qt),I[01]:] -defined the carrier of R^1 -valued Function-like V203() V204() V205() Element of bool [: the carrier of [:(x | Qt),I[01]:], the carrier of R^1:]
g2 is non empty V213() V214() V215() Element of bool the carrier of I[01]
[:{ftm},g2:] is non empty V203() V204() V205() Element of bool the carrier of [:x,I[01]:]
Ft | [:{ftm},g2:] is Relation-like the carrier of [:(x | Pt),I[01]:] -defined the carrier of R^1 -valued Function-like V203() V204() V205() Element of bool [: the carrier of [:(x | Pt),I[01]:], the carrier of R^1:]
ft0 | [:{ftm},g2:] is Relation-like the carrier of [:(x | Qt),I[01]:] -defined the carrier of R^1 -valued Function-like V203() V204() V205() Element of bool [: the carrier of [:(x | Qt),I[01]:], the carrier of R^1:]
ft2 is ordinal natural V11() ext-real non negative real integer V34() V213() V214() V215() V216() V217() V218() V317() Element of NAT
ft1 . ft2 is V11() ext-real real Element of REAL
ft2 + 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
ft1 . (ft2 + 1) is V11() ext-real real Element of REAL
[.(ft1 . ft2),(ft1 . (ft2 + 1)).] is V213() V214() V215() V320() Element of bool REAL
sM1 is set
Qt is V11() ext-real real Element of REAL
ft2 is V213() V214() V215() Element of bool the carrier of I[01]
g2 \/ ft2 is non empty V213() V214() V215() Element of bool the carrier of I[01]
sM1 is non empty V213() V214() V215() Element of bool the carrier of I[01]
[:{ftm},sM1:] is non empty V203() V204() V205() Element of bool the carrier of [:x,I[01]:]
Ft | [:{ftm},sM1:] is Relation-like the carrier of [:(x | Pt),I[01]:] -defined the carrier of R^1 -valued Function-like V203() V204() V205() Element of bool [: the carrier of [:(x | Pt),I[01]:], the carrier of R^1:]
ft0 | [:{ftm},sM1:] is Relation-like the carrier of [:(x | Qt),I[01]:] -defined the carrier of R^1 -valued Function-like V203() V204() V205() Element of bool [: the carrier of [:(x | Qt),I[01]:], the carrier of R^1:]
dom (Ft | [:{ftm},sM1:]) is Element of bool the carrier of [:(x | Pt),I[01]:]
ft is non empty open Element of bool the carrier of x
[:ft,ft2:] is V203() V204() V205() Element of bool the carrier of [:x,I[01]:]
y .: [:ft,ft2:] is Element of bool the carrier of (Tunit_circle 2)
Qt is non empty Element of bool the carrier of (Tunit_circle 2)
CircleMap " Qt is V213() V214() V215() Element of bool the carrier of R^1
(Tunit_circle 2) | Qt is non empty strict TopSpace-like SubSpace of Tunit_circle 2
the carrier of ((Tunit_circle 2) | Qt) is non empty set
Qt is mutually-disjoint open Element of bool (bool the carrier of R^1)
union Qt is V213() V214() V215() Element of bool the carrier of R^1
G is set
(Ft | [:{ftm},sM1:]) . G is V11() ext-real real Element of REAL
(ft0 | [:{ftm},sM1:]) . G is V11() ext-real real Element of REAL
F1 is set
x is set
[F1,x] is set
{F1,x} is non empty set
{F1} is non empty set
{{F1,x},{F1}} is non empty set
x1 is non empty Element of bool the carrier of x
[:x1,ft2:] is V203() V204() V205() Element of bool the carrier of [:x,I[01]:]
[F1,(ft1 . G)] is set
{F1,(ft1 . G)} is non empty set
{{F1,(ft1 . G)},{F1}} is non empty set
y . [F1,(ft1 . G)] is set
x2 is Element of bool the carrier of [:(x | Pt),I[01]:]
Ft .: x2 is V213() V214() V215() Element of bool the carrier of R^1
XZZ is set
union Qt is set
Uit is Element of the carrier of [:(x | Pt),I[01]:]
Ft . Uit is V11() ext-real real Element of the carrier of R^1
CircleMap . (Ft . Uit) is Element of the carrier of (Tunit_circle 2)
(CircleMap * Ft) . Uit is Element of the carrier of (Tunit_circle 2)
y . Uit is set
XZZ is Element of bool the carrier of [:(x | Qt),I[01]:]
ft0 .: x2 is V213() V214() V215() Element of bool the carrier of R^1
Uit is set
union Qt is set
Uit is Element of the carrier of [:(x | Qt),I[01]:]
ft0 . Uit is V11() ext-real real Element of the carrier of R^1
CircleMap . (ft0 . Uit) is Element of the carrier of (Tunit_circle 2)
(CircleMap * ft0) . Uit is Element of the carrier of (Tunit_circle 2)
y . Uit is set
(CircleMap * Ft) . [F1,(ft1 . G)] is set
Ft . [F1,(ft1 . G)] is V11() ext-real real Element of REAL
CircleMap . (Ft . [F1,(ft1 . G)]) is set
Uit is set
Uit is non empty V213() V214() V215() Element of bool the carrier of R^1
CircleMap | Uit 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):]
dom (CircleMap | Uit) is V213() V214() V215() Element of bool the carrier of R^1
rng (CircleMap | Uit) is Element of bool the carrier of (Tunit_circle 2)
f is set
Uith is set
(CircleMap | Uit) . Uith is set
CircleMap . Uith is set
R^1 | Uit is non empty strict TopSpace-like V302() SubSpace of R^1
the carrier of (R^1 | Uit) is non empty V213() V214() V215() set
[: the carrier of (R^1 | Uit), the carrier of ((Tunit_circle 2) | Qt):] is non empty set
bool [: the carrier of (R^1 | Uit), the carrier of ((Tunit_circle 2) | Qt):] is non empty set
[:Qt,g2:] is non empty V203() V204() V205() Element of bool the carrier of [:x,I[01]:]
(CircleMap * ft0) . [F1,(ft1 . G)] is set
ft0 . [F1,(ft1 . G)] is V11() ext-real real Element of REAL
CircleMap . (ft0 . [F1,(ft1 . G)]) is set
Uith is set
Ft | [:x1,ft2:] is Relation-like the carrier of [:(x | Pt),I[01]:] -defined the carrier of R^1 -valued Function-like V203() V204() V205() Element of bool [: the carrier of [:(x | Pt),I[01]:], the carrier of R^1:]
dom (Ft | [:x1,ft2:]) is Element of bool the carrier of [:(x | Pt),I[01]:]
rng (Ft | [:x1,ft2:]) is V213() V214() V215() Element of bool the carrier of R^1
f is non empty Relation-like the carrier of (R^1 | Uit) -defined the carrier of ((Tunit_circle 2) | Qt) -valued Function-like V26( the carrier of (R^1 | Uit)) quasi_total Element of bool [: the carrier of (R^1 | Uit), the carrier of ((Tunit_circle 2) | Qt):]
dom f is V213() V214() V215() Element of bool the carrier of (R^1 | Uit)
bool the carrier of (R^1 | Uit) is non empty set
b is set
a is set
(Ft | [:x1,ft2:]) . a is V11() ext-real real Element of REAL
Ft . a is V11() ext-real real Element of REAL
f * (Ft | [:x1,ft2:]) is Relation-like the carrier of [:(x | Pt),I[01]:] -defined the carrier of ((Tunit_circle 2) | Qt) -valued Function-like Element of bool [: the carrier of [:(x | Pt),I[01]:], the carrier of ((Tunit_circle 2) | Qt):]
[: the carrier of [:(x | Pt),I[01]:], the carrier of ((Tunit_circle 2) | Qt):] is non empty set
bool [: the carrier of [:(x | Pt),I[01]:], the carrier of ((Tunit_circle 2) | Qt):] is non empty set
dom (f * (Ft | [:x1,ft2:])) is Element of bool the carrier of [:(x | Pt),I[01]:]
Uith is non empty V213() V214() V215() Element of bool the carrier of R^1
(Ft | [:{ftm},g2:]) . [F1,(ft1 . G)] is V11() ext-real real Element of REAL
ft0 | [:x1,ft2:] is Relation-like the carrier of [:(x | Qt),I[01]:] -defined the carrier of R^1 -valued Function-like V203() V204() V205() Element of bool [: the carrier of [:(x | Qt),I[01]:], the carrier of R^1:]
f * (ft0 | [:x1,ft2:]) is Relation-like the carrier of [:(x | Qt),I[01]:] -defined the carrier of ((Tunit_circle 2) | Qt) -valued Function-like Element of bool [: the carrier of [:(x | Qt),I[01]:], the carrier of ((Tunit_circle 2) | Qt):]
[: the carrier of [:(x | Qt),I[01]:], the carrier of ((Tunit_circle 2) | Qt):] is non empty set
bool [: the carrier of [:(x | Qt),I[01]:], the carrier of ((Tunit_circle 2) | Qt):] is non empty set
b is set
(f * (Ft | [:x1,ft2:])) . b is set
(f * (ft0 | [:x1,ft2:])) . b is set
Ft . b is V11() ext-real real Element of REAL
Ft .: [:x1,ft2:] is V213() V214() V215() Element of bool the carrier of R^1
ft0 . b is V11() ext-real real Element of REAL
ft0 .: [:x1,ft2:] is V213() V214() V215() Element of bool the carrier of R^1
(dom Ft) /\ [:x1,ft2:] is Element of bool the carrier of [:x,I[01]:]
f * Ft is Relation-like the carrier of [:(x | Pt),I[01]:] -defined the carrier of ((Tunit_circle 2) | Qt) -valued Function-like Element of bool [: the carrier of [:(x | Pt),I[01]:], the carrier of ((Tunit_circle 2) | Qt):]
(f * Ft) | [:x1,ft2:] is Relation-like the carrier of [:(x | Pt),I[01]:] -defined the carrier of ((Tunit_circle 2) | Qt) -valued Function-like Element of bool [: the carrier of [:(x | Pt),I[01]:], the carrier of ((Tunit_circle 2) | Qt):]
((f * Ft) | [:x1,ft2:]) . b is set
(f * Ft) . b is set
f . (Ft . b) is set
CircleMap . (Ft . b) is set
(CircleMap * Ft) . b is set
y . b is set
(CircleMap * ft0) . b is set
CircleMap . (ft0 . b) is set
f . (ft0 . b) is set
f * ft0 is Relation-like the carrier of [:(x | Qt),I[01]:] -defined the carrier of ((Tunit_circle 2) | Qt) -valued Function-like Element of bool [: the carrier of [:(x | Qt),I[01]:], the carrier of ((Tunit_circle 2) | Qt):]
(f * ft0) . b is set
(f * ft0) | [:x1,ft2:] is Relation-like the carrier of [:(x | Qt),I[01]:] -defined the carrier of ((Tunit_circle 2) | Qt) -valued Function-like Element of bool [: the carrier of [:(x | Qt),I[01]:], the carrier of ((Tunit_circle 2) | Qt):]
((f * ft0) | [:x1,ft2:]) . b is set
dom (ft0 | [:x1,ft2:]) is Element of bool the carrier of [:(x | Qt),I[01]:]
rng (ft0 | [:x1,ft2:]) is V213() V214() V215() Element of bool the carrier of R^1
b is set
a is set
(ft0 | [:x1,ft2:]) . a is V11() ext-real real Element of REAL
ft0 . a is V11() ext-real real Element of REAL
dom (f * (ft0 | [:x1,ft2:])) is Element of bool the carrier of [:(x | Qt),I[01]:]
Ft . G is V11() ext-real real Element of REAL
(Ft | [:x1,ft2:]) . G is V11() ext-real real Element of REAL
(ft0 | [:x1,ft2:]) . G is V11() ext-real real Element of REAL
ft0 . G is V11() ext-real real Element of REAL
Ft . G is V11() ext-real real Element of REAL
(Ft | [:{ftm},g2:]) . G is V11() ext-real real Element of REAL
ft0 . G is V11() ext-real real Element of REAL
dom (ft0 | [:{ftm},sM1:]) is Element of bool the carrier of [:(x | Qt),I[01]:]
ft1 . 0 is V11() ext-real real Element of REAL
[.0,(ft1 . 0).] is V213() V214() V215() V320() Element of bool REAL
[.0,(ft1 . (len ft1)).] is V213() V214() V215() V320() Element of bool REAL
G is non empty V213() V214() V215() Element of bool the carrier of I[01]
[:{ftm},G:] is non empty V203() V204() V205() Element of bool the carrier of [:x,I[01]:]
Ft | [:{ftm},G:] is Relation-like the carrier of [:(x | Pt),I[01]:] -defined the carrier of R^1 -valued Function-like V203() V204() V205() Element of bool [: the carrier of [:(x | Pt),I[01]:], the carrier of R^1:]
ft0 | [:{ftm},G:] is Relation-like the carrier of [:(x | Qt),I[01]:] -defined the carrier of R^1 -valued Function-like V203() V204() V205() Element of bool [: the carrier of [:(x | Qt),I[01]:], the carrier of R^1:]
F is Element of the carrier of [:x,I[01]:]
x . F is V11() ext-real real Element of the carrier of R^1
ftm is V213() V214() V215() Element of bool the carrier of R^1
Qt is non empty open Element of bool the carrier of x
x | Qt is non empty strict TopSpace-like open SubSpace of x
[:(x | Qt),I[01]:] is non empty strict TopSpace-like TopStruct
the carrier of [:(x | Qt),I[01]:] is non empty set
[: the carrier of [:(x | Qt),I[01]:], the carrier of R^1:] is non empty V203() V204() V205() set
bool [: the carrier of [:(x | Qt),I[01]:], the carrier of R^1:] is non empty set
yt is Element of the carrier of x
Pt is V11() ext-real real Element of the carrier of I[01]
[yt,Pt] is Element of the carrier of [:x,I[01]:]
{yt,Pt} is non empty set
{yt} is non empty set
{{yt,Pt},{yt}} is non empty set
Ft is non empty Relation-like the carrier of [:(x | Qt),I[01]:] -defined the carrier of R^1 -valued Function-like V26( the carrier of [:(x | Qt),I[01]:]) quasi_total V203() V204() V205() Element of bool [: the carrier of [:(x | Qt),I[01]:], the carrier of R^1:]
Ft . F is V11() ext-real real Element of REAL
[:Qt, the carrier of I[01]:] is non empty V203() V204() V205() set
y | [:Qt, the carrier of I[01]:] is Relation-like the carrier of [:x,I[01]:] -defined the carrier of (Tunit_circle 2) -valued Function-like Element of bool [: the carrier of [:x,I[01]:], the carrier of (Tunit_circle 2):]
CircleMap * Ft is non empty Relation-like the carrier of [:(x | Qt),I[01]:] -defined the carrier of (Tunit_circle 2) -valued Function-like V26( the carrier of [:(x | Qt),I[01]:]) quasi_total Element of bool [: the carrier of [:(x | Qt),I[01]:], the carrier of (Tunit_circle 2):]
[: the carrier of [:(x | Qt),I[01]:], the carrier of (Tunit_circle 2):] is non empty set
bool [: the carrier of [:(x | Qt),I[01]:], the carrier of (Tunit_circle 2):] is non empty set
Ft | [: the carrier of x,{0}:] is Relation-like the carrier of [:(x | Qt),I[01]:] -defined the carrier of R^1 -valued Function-like V203() V204() V205() Element of bool [: the carrier of [:(x | Qt),I[01]:], the carrier of R^1:]
S | [:Qt, the carrier of I[01]:] is Relation-like the carrier of [:x,(Sspace 0[01]):] -defined the carrier of R^1 -valued Function-like V203() V204() V205() Element of bool [: the carrier of [:x,(Sspace 0[01]):], the carrier of R^1:]
the carrier of (x | Qt) is non empty set
[: the carrier of (x | Qt), the carrier of I[01]:] is non empty V203() V204() V205() set
bool the carrier of [:(x | Qt),I[01]:] is non empty set
ft0 is Element of bool the carrier of [:(x | Qt),I[01]:]
Ft .: ft0 is V213() V214() V215() Element of bool the carrier of R^1
dom Ft is Element of bool the carrier of [:(x | Qt),I[01]:]
[#] (x | Qt) is non empty non proper open closed dense non boundary Element of bool the carrier of (x | Qt)
bool the carrier of (x | Qt) is non empty set
[#] [:(x | Qt),I[01]:] is non empty non proper open closed dense non boundary Element of bool the carrier of [:(x | Qt),I[01]:]
[:Qt,([#] I[01]):] is non empty V203() V204() V205() Element of bool the carrier of [:x,I[01]:]
[:x,I[01]:] | [:Qt,([#] I[01]):] is non empty strict TopSpace-like SubSpace of [:x,I[01]:]
ft1 is Element of bool the carrier of [:x,I[01]:]
ft1 /\ ([#] [:(x | Qt),I[01]:]) is Element of bool the carrier of [:(x | Qt),I[01]:]
ft1 /\ [:Qt,([#] I[01]):] is Element of bool the carrier of [:x,I[01]:]
ftn is Element of bool the carrier of [:x,I[01]:]
x .: ftn is V213() V214() V215() Element of bool the carrier of R^1
ft is set
G is Element of the carrier of [:x,I[01]:]
x . G is V11() ext-real real Element of the carrier of R^1
ft2 is non empty open Element of bool the carrier of x
x | ft2 is non empty strict TopSpace-like open SubSpace of x
[:(x | ft2),I[01]:] is non empty strict TopSpace-like TopStruct
the carrier of [:(x | ft2),I[01]:] is non empty set
[: the carrier of [:(x | ft2),I[01]:], the carrier of R^1:] is non empty V203() V204() V205() set
bool [: the carrier of [:(x | ft2),I[01]:], the carrier of R^1:] is non empty set
sM0 is Element of the carrier of x
g2 is V11() ext-real real Element of the carrier of I[01]
[sM0,g2] is Element of the carrier of [:x,I[01]:]
{sM0,g2} is non empty set
{sM0} is non empty set
{{sM0,g2},{sM0}} is non empty set
sM1 is non empty Relation-like the carrier of [:(x | ft2),I[01]:] -defined the carrier of R^1 -valued Function-like V26( the carrier of [:(x | ft2),I[01]:]) quasi_total V203() V204() V205() Element of bool [: the carrier of [:(x | ft2),I[01]:], the carrier of R^1:]
sM1 . G is V11() ext-real real Element of REAL
[:ft2, the carrier of I[01]:] is non empty V203() V204() V205() set
y | [:ft2, the carrier of I[01]:] is Relation-like the carrier of [:x,I[01]:] -defined the carrier of (Tunit_circle 2) -valued Function-like Element of bool [: the carrier of [:x,I[01]:], the carrier of (Tunit_circle 2):]
CircleMap * sM1 is non empty Relation-like the carrier of [:(x | ft2),I[01]:] -defined the carrier of (Tunit_circle 2) -valued Function-like V26( the carrier of [:(x | ft2),I[01]:]) quasi_total Element of bool [: the carrier of [:(x | ft2),I[01]:], the carrier of (Tunit_circle 2):]
[: the carrier of [:(x | ft2),I[01]:], the carrier of (Tunit_circle 2):] is non empty set
bool [: the carrier of [:(x | ft2),I[01]:], the carrier of (Tunit_circle 2):] is non empty set
sM1 | [: the carrier of x,{0}:] is Relation-like the carrier of [:(x | ft2),I[01]:] -defined the carrier of R^1 -valued Function-like V203() V204() V205() Element of bool [: the carrier of [:(x | ft2),I[01]:], the carrier of R^1:]
S | [:ft2, the carrier of I[01]:] is Relation-like the carrier of [:x,(Sspace 0[01]):] -defined the carrier of R^1 -valued Function-like V203() V204() V205() Element of bool [: the carrier of [:x,(Sspace 0[01]):], the carrier of R^1:]
{sM0} is non empty connected compact Element of bool the carrier of x
[:{sM0}, the carrier of I[01]:] is non empty V203() V204() V205() set
Ft . G is V11() ext-real real Element of REAL
Ft | [:{sM0}, the carrier of I[01]:] is Relation-like the carrier of [:(x | Qt),I[01]:] -defined the carrier of R^1 -valued Function-like V203() V204() V205() Element of bool [: the carrier of [:(x | Qt),I[01]:], the carrier of R^1:]
(Ft | [:{sM0}, the carrier of I[01]:]) . G is V11() ext-real real Element of REAL
sM1 | [:{sM0}, the carrier of I[01]:] is Relation-like the carrier of [:(x | ft2),I[01]:] -defined the carrier of R^1 -valued Function-like V203() V204() V205() Element of bool [: the carrier of [:(x | ft2),I[01]:], the carrier of R^1:]
(sM1 | [:{sM0}, the carrier of I[01]:]) . G is V11() ext-real real Element of REAL
F is Element of the carrier of [:x,I[01]:]
y . F is Element of the carrier of (Tunit_circle 2)
(CircleMap * x) . F is Element of the carrier of (Tunit_circle 2)
x . F is V11() ext-real real Element of the carrier of R^1
Pt is non empty open Element of bool the carrier of x
x | Pt is non empty strict TopSpace-like open SubSpace of x
[:(x | Pt),I[01]:] is non empty strict TopSpace-like TopStruct
the carrier of [:(x | Pt),I[01]:] is non empty set
[: the carrier of [:(x | Pt),I[01]:], the carrier of R^1:] is non empty V203() V204() V205() set
bool [: the carrier of [:(x | Pt),I[01]:], the carrier of R^1:] is non empty set
ftm is Element of the carrier of x
yt is V11() ext-real real Element of the carrier of I[01]
[ftm,yt] is Element of the carrier of [:x,I[01]:]
{ftm,yt} is non empty set
{ftm} is non empty set
{{ftm,yt},{ftm}} is non empty set
Qt is non empty Relation-like the carrier of [:(x | Pt),I[01]:] -defined the carrier of R^1 -valued Function-like V26( the carrier of [:(x | Pt),I[01]:]) quasi_total V203() V204() V205() Element of bool [: the carrier of [:(x | Pt),I[01]:], the carrier of R^1:]
Qt . F is V11() ext-real real Element of REAL
[:Pt, the carrier of I[01]:] is non empty V203() V204() V205() set
y | [:Pt, the carrier of I[01]:] is Relation-like the carrier of [:x,I[01]:] -defined the carrier of (Tunit_circle 2) -valued Function-like Element of bool [: the carrier of [:x,I[01]:], the carrier of (Tunit_circle 2):]
CircleMap * Qt is non empty Relation-like the carrier of [:(x | Pt),I[01]:] -defined the carrier of (Tunit_circle 2) -valued Function-like V26( the carrier of [:(x | Pt),I[01]:]) quasi_total Element of bool [: the carrier of [:(x | Pt),I[01]:], the carrier of (Tunit_circle 2):]
[: the carrier of [:(x | Pt),I[01]:], the carrier of (Tunit_circle 2):] is non empty set
bool [: the carrier of [:(x | Pt),I[01]:], the carrier of (Tunit_circle 2):] is non empty set
Qt | [: the carrier of x,{0}:] is Relation-like the carrier of [:(x | Pt),I[01]:] -defined the carrier of R^1 -valued Function-like V203() V204() V205() Element of bool [: the carrier of [:(x | Pt),I[01]:], the carrier of R^1:]
S | [:Pt, the carrier of I[01]:] is Relation-like the carrier of [:x,(Sspace 0[01]):] -defined the carrier of R^1 -valued Function-like V203() V204() V205() Element of bool [: the carrier of [:x,(Sspace 0[01]):], the carrier of R^1:]
the carrier of (x | Pt) is non empty set
[: the carrier of (x | Pt), the carrier of I[01]:] is non empty V203() V204() V205() set
CircleMap . (x . F) is Element of the carrier of (Tunit_circle 2)
(CircleMap * Qt) . F is set
dom x is Element of bool the carrier of [:x,I[01]:]
F is set
S . F is V11() ext-real real Element of REAL
x . F is V11() ext-real real Element of REAL
Pt is non empty open Element of bool the carrier of x
x | Pt is non empty strict TopSpace-like open SubSpace of x
[:(x | Pt),I[01]:] is non empty strict TopSpace-like TopStruct
the carrier of [:(x | Pt),I[01]:] is non empty set
[: the carrier of [:(x | Pt),I[01]:], the carrier of R^1:] is non empty V203() V204() V205() set
bool [: the carrier of [:(x | Pt),I[01]:], the carrier of R^1:] is non empty set
ftm is Element of the carrier of x
yt is V11() ext-real real Element of the carrier of I[01]
[ftm,yt] is Element of the carrier of [:x,I[01]:]
{ftm,yt} is non empty set
{ftm} is non empty set
{{ftm,yt},{ftm}} is non empty set
Qt is non empty Relation-like the carrier of [:(x | Pt),I[01]:] -defined the carrier of R^1 -valued Function-like V26( the carrier of [:(x | Pt),I[01]:]) quasi_total V203() V204() V205() Element of bool [: the carrier of [:(x | Pt),I[01]:], the carrier of R^1:]
Qt . F is V11() ext-real real Element of REAL
[:Pt, the carrier of I[01]:] is non empty V203() V204() V205() set
y | [:Pt, the carrier of I[01]:] is Relation-like the carrier of [:x,I[01]:] -defined the carrier of (Tunit_circle 2) -valued Function-like Element of bool [: the carrier of [:x,I[01]:], the carrier of (Tunit_circle 2):]
CircleMap * Qt is non empty Relation-like the carrier of [:(x | Pt),I[01]:] -defined the carrier of (Tunit_circle 2) -valued Function-like V26( the carrier of [:(x | Pt),I[01]:]) quasi_total Element of bool [: the carrier of [:(x | Pt),I[01]:], the carrier of (Tunit_circle 2):]
[: the carrier of [:(x | Pt),I[01]:], the carrier of (Tunit_circle 2):] is non empty set
bool [: the carrier of [:(x | Pt),I[01]:], the carrier of (Tunit_circle 2):] is non empty set
Qt | [: the carrier of x,{0}:] is Relation-like the carrier of [:(x | Pt),I[01]:] -defined the carrier of R^1 -valued Function-like V203() V204() V205() Element of bool [: the carrier of [:(x | Pt),I[01]:], the carrier of R^1:]
S | [:Pt, the carrier of I[01]:] is Relation-like the carrier of [:x,(Sspace 0[01]):] -defined the carrier of R^1 -valued Function-like V203() V204() V205() Element of bool [: the carrier of [:x,(Sspace 0[01]):], the carrier of R^1:]
(S | [:Pt, the carrier of I[01]:]) . F is V11() ext-real real Element of REAL
(dom x) /\ [: the carrier of x,{0}:] is Element of bool the carrier of [:x,I[01]:]
F is non empty Relation-like the carrier of [:x,I[01]:] -defined the carrier of R^1 -valued Function-like V26( the carrier of [:x,I[01]:]) quasi_total V203() V204() V205() Element of bool [: the carrier of [:x,I[01]:], the carrier of R^1:]
CircleMap * F is non empty Relation-like the carrier of [:x,I[01]:] -defined the carrier of (Tunit_circle 2) -valued Function-like V26( the carrier of [:x,I[01]:]) quasi_total Element of bool [: the carrier of [:x,I[01]:], the carrier of (Tunit_circle 2):]
F | [: the carrier of x,{0}:] is Relation-like the carrier of [:x,I[01]:] -defined the carrier of R^1 -valued Function-like V203() V204() V205() Element of bool [: the carrier of [:x,I[01]:], the carrier of R^1:]
ftm is Element of the carrier of [:x,I[01]:]
x . ftm is V11() ext-real real Element of the carrier of R^1
F . ftm is V11() ext-real real Element of the carrier of R^1
Qt is non empty open Element of bool the carrier of x
x | Qt is non empty strict TopSpace-like open SubSpace of x
[:(x | Qt),I[01]:] is non empty strict TopSpace-like TopStruct
the carrier of [:(x | Qt),I[01]:] is non empty set
[: the carrier of [:(x | Qt),I[01]:], the carrier of R^1:] is non empty V203() V204() V205() set
bool [: the carrier of [:(x | Qt),I[01]:], the carrier of R^1:] is non empty set
yt is Element of the carrier of x
Pt is V11() ext-real real Element of the carrier of I[01]
[yt,Pt] is Element of the carrier of [:x,I[01]:]
{yt,Pt} is non empty set
{yt} is non empty set
{{yt,Pt},{yt}} is non empty set
Ft is non empty Relation-like the carrier of [:(x | Qt),I[01]:] -defined the carrier of R^1 -valued Function-like V26( the carrier of [:(x | Qt),I[01]:]) quasi_total V203() V204() V205() Element of bool [: the carrier of [:(x | Qt),I[01]:], the carrier of R^1:]
Ft . ftm is V11() ext-real real Element of REAL
[:Qt, the carrier of I[01]:] is non empty V203() V204() V205() set
y | [:Qt, the carrier of I[01]:] is Relation-like the carrier of [:x,I[01]:] -defined the carrier of (Tunit_circle 2) -valued Function-like Element of bool [: the carrier of [:x,I[01]:], the carrier of (Tunit_circle 2):]
CircleMap * Ft is non empty Relation-like the carrier of [:(x | Qt),I[01]:] -defined the carrier of (Tunit_circle 2) -valued Function-like V26( the carrier of [:(x | Qt),I[01]:]) quasi_total Element of bool [: the carrier of [:(x | Qt),I[01]:], the carrier of (Tunit_circle 2):]
[: the carrier of [:(x | Qt),I[01]:], the carrier of (Tunit_circle 2):] is non empty set
bool [: the carrier of [:(x | Qt),I[01]:], the carrier of (Tunit_circle 2):] is non empty set
Ft | [: the carrier of x,{0}:] is Relation-like the carrier of [:(x | Qt),I[01]:] -defined the carrier of R^1 -valued Function-like V203() V204() V205() Element of bool [: the carrier of [:(x | Qt),I[01]:], the carrier of R^1:]
S | [:Qt, the carrier of I[01]:] is Relation-like the carrier of [:x,(Sspace 0[01]):] -defined the carrier of R^1 -valued Function-like V203() V204() V205() Element of bool [: the carrier of [:x,(Sspace 0[01]):], the carrier of R^1:]
the carrier of (x | Qt) is non empty set
[: the carrier of (x | Qt), the carrier of I[01]:] is non empty V203() V204() V205() set
dom F is Element of bool the carrier of [:x,I[01]:]
F | [:Qt, the carrier of I[01]:] is Relation-like the carrier of [:x,I[01]:] -defined the carrier of R^1 -valued Function-like V203() V204() V205() Element of bool [: the carrier of [:x,I[01]:], the carrier of R^1:]
dom (F | [:Qt, the carrier of I[01]:]) is Element of bool the carrier of [:x,I[01]:]
rng (F | [:Qt, the carrier of I[01]:]) is V213() V214() V215() Element of bool the carrier of R^1
(F | [:Qt, the carrier of I[01]:]) | [: the carrier of x,{0}:] is Relation-like the carrier of [:x,I[01]:] -defined the carrier of R^1 -valued Function-like V203() V204() V205() Element of bool [: the carrier of [:x,I[01]:], the carrier of R^1:]
[: the carrier of x,{0}:] /\ [:Qt, the carrier of I[01]:] is set
F | ([: the carrier of x,{0}:] /\ [:Qt, the carrier of I[01]:]) is Relation-like the carrier of [:x,I[01]:] -defined the carrier of R^1 -valued Function-like V203() V204() V205() Element of bool [: the carrier of [:x,I[01]:], the carrier of R^1:]
ft0 is non empty Relation-like the carrier of [:(x | Qt),I[01]:] -defined the carrier of R^1 -valued Function-like V26( the carrier of [:(x | Qt),I[01]:]) quasi_total V203() V204() V205() Element of bool [: the carrier of [:(x | Qt),I[01]:], the carrier of R^1:]
CircleMap * (F | [:Qt, the carrier of I[01]:]) is Relation-like the carrier of [:x,I[01]:] -defined the carrier of (Tunit_circle 2) -valued Function-like Element of bool [: the carrier of [:x,I[01]:], the carrier of (Tunit_circle 2):]
(F | [:Qt, the carrier of I[01]:]) . ftm is V11() ext-real real Element of REAL
{1} is non empty V213() V214() V215() V216() V217() V218() V315() V317() Element of bool REAL
1TopSp {1} is non empty strict TopSpace-like T_0 T_1 T_2 TopStruct
bool {1} is non empty Element of bool (bool {1})
bool {1} is non empty set
bool (bool {1}) is non empty set
[#] (bool {1}) is non empty non proper Element of bool (bool {1})
bool (bool {1}) is non empty set
TopStruct(# {1},([#] (bool {1})) #) is non empty strict TopStruct
x is Element of the carrier of (Tunit_circle 2)
y is Element of the carrier of (Tunit_circle 2)
{x} is non empty connected compact Element of bool the carrier of (Tunit_circle 2)
CircleMap " {x} is V213() V214() V215() Element of bool the carrier of R^1
S is V11() ext-real real Element of the carrier of R^1
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 continuous Path of x,y
the carrier of (1TopSp {1}) is non empty set
[: the carrier of (1TopSp {1}), the carrier of I[01]:] is non empty V203() V204() V205() set
[:[: the carrier of (1TopSp {1}), the carrier of I[01]:], the carrier of (Tunit_circle 2):] is non empty set
bool [:[: the carrier of (1TopSp {1}), the carrier of I[01]:], the carrier of (Tunit_circle 2):] is non empty set
F is non empty Relation-like [: the carrier of (1TopSp {1}), the carrier of I[01]:] -defined the carrier of (Tunit_circle 2) -valued Function-like V26([: the carrier of (1TopSp {1}), the carrier of I[01]:]) quasi_total Element of bool [:[: the carrier of (1TopSp {1}), the carrier of I[01]:], the carrier of (Tunit_circle 2):]
ftm is Element of the carrier of (1TopSp {1})
j0 is V11() ext-real real Element of the carrier of I[01]
[ftm,j0] is Element of the carrier of [:(1TopSp {1}),I[01]:]
[:(1TopSp {1}),I[01]:] is non empty strict TopSpace-like T_0 T_1 T_2 TopStruct
the carrier of [:(1TopSp {1}),I[01]:] is non empty set
{ftm,j0} is non empty set
{ftm} is non empty set
{{ftm,j0},{ftm}} is non empty set
[: the carrier of (1TopSp {1}),{0}:] is non empty RAT -valued INT -valued V203() V204() V205() V206() set
[: the carrier of [:(1TopSp {1}),I[01]:], the carrier of (Tunit_circle 2):] is non empty set
bool [: the carrier of [:(1TopSp {1}),I[01]:], the carrier of (Tunit_circle 2):] is non empty set
[:(1TopSp {1}),(Sspace 0[01]):] is non empty strict TopSpace-like T_0 T_1 T_2 TopStruct
[:(1TopSp {1}),(Sspace 0[01]):] --> S is non empty Relation-like the carrier of [:(1TopSp {1}),(Sspace 0[01]):] -defined the carrier of R^1 -valued Function-like V26( the carrier of [:(1TopSp {1}),(Sspace 0[01]):]) quasi_total continuous V203() V204() V205() Element of bool [: the carrier of [:(1TopSp {1}),(Sspace 0[01]):], the carrier of R^1:]
the carrier of [:(1TopSp {1}),(Sspace 0[01]):] is non empty set
[: the carrier of [:(1TopSp {1}),(Sspace 0[01]):], the carrier of R^1:] is non empty V203() V204() V205() set
bool [: the carrier of [:(1TopSp {1}),(Sspace 0[01]):], the carrier of R^1:] is non empty set
K178( the carrier of R^1, the carrier of [:(1TopSp {1}),(Sspace 0[01]):],S) is non empty Relation-like the carrier of [:(1TopSp {1}),(Sspace 0[01]):] -defined the carrier of R^1 -valued Function-like V26( the carrier of [:(1TopSp {1}),(Sspace 0[01]):]) quasi_total V203() V204() V205() Element of bool [: the carrier of [:(1TopSp {1}),(Sspace 0[01]):], the carrier of R^1:]
[: the carrier of (1TopSp {1}), the carrier of (Sspace 0[01]):] is non empty V203() V204() V205() set
Qt is Element of the carrier of (1TopSp {1})
Ft is ordinal natural V11() ext-real non negative real integer V34() Element of {0}
[Qt,Ft] is Element of [: the carrier of (1TopSp {1}),{0}:]
{Qt,Ft} is non empty set
{Qt} is non empty set
{{Qt,Ft},{Qt}} is non empty set
([:(1TopSp {1}),(Sspace 0[01]):] --> S) . [Qt,Ft] is V11() ext-real real Element of REAL
[#] (1TopSp {1}) is non empty non proper open closed dense non boundary Element of bool the carrier of (1TopSp {1})
bool the carrier of (1TopSp {1}) is non empty set
yt is non empty Relation-like the carrier of [:(1TopSp {1}),I[01]:] -defined the carrier of (Tunit_circle 2) -valued Function-like V26( the carrier of [:(1TopSp {1}),I[01]:]) quasi_total Element of bool [: the carrier of [:(1TopSp {1}),I[01]:], the carrier of (Tunit_circle 2):]
bool the carrier of [:(1TopSp {1}),I[01]:] is non empty set
Qt is Element of the carrier of [:(1TopSp {1}),I[01]:]
yt . Qt is Element of the carrier of (Tunit_circle 2)
Ft is Element of bool the carrier of (Tunit_circle 2)
ft0 is Element of the carrier of (1TopSp {1})
ft1 is V11() ext-real real Element of the carrier of I[01]
[ft0,ft1] is Element of the carrier of [:(1TopSp {1}),I[01]:]
{ft0,ft1} is non empty set
{ft0} is non empty set
{{ft0,ft1},{ft0}} is non empty set
yt . (ft0,ft1) is set
[ft0,ft1] is set
yt . [ft0,ft1] is set
x . ft1 is Element of the carrier of (Tunit_circle 2)
ftn is V213() V214() V215() Element of bool the carrier of I[01]
x .: ftn is Element of bool the carrier of (Tunit_circle 2)
[:{1},ftn:] is V203() V204() V205() set
G is Element of bool the carrier of [:(1TopSp {1}),I[01]:]
yt .: G is Element of bool the carrier of (Tunit_circle 2)
sM0 is set
g2 is set
yt . g2 is set
ft2 is Element of the carrier of (1TopSp {1})
sM1 is V11() ext-real real Element of the carrier of I[01]
[ft2,sM1] is Element of the carrier of [:(1TopSp {1}),I[01]:]
{ft2,sM1} is non empty set
{ft2} is non empty set
{{ft2,sM1},{ft2}} is non empty set
x . sM1 is Element of the carrier of (Tunit_circle 2)
yt . (ft2,sM1) is set
[ft2,sM1] is set
yt . [ft2,sM1] is set
CircleMap . S is Element of the carrier of (Tunit_circle 2)
CircleMap * ([:(1TopSp {1}),(Sspace 0[01]):] --> S) is non empty Relation-like the carrier of [:(1TopSp {1}),(Sspace 0[01]):] -defined the carrier of [:(1TopSp {1}),(Sspace 0[01]):] -defined the carrier of (Tunit_circle 2) -valued the carrier of (Tunit_circle 2) -valued Function-like V26( the carrier of [:(1TopSp {1}),(Sspace 0[01]):]) V26( the carrier of [:(1TopSp {1}),(Sspace 0[01]):]) quasi_total quasi_total continuous Element of bool [: the carrier of [:(1TopSp {1}),(Sspace 0[01]):], the carrier of (Tunit_circle 2):]
[: the carrier of [:(1TopSp {1}),(Sspace 0[01]):], the carrier of (Tunit_circle 2):] is non empty set
bool [: the carrier of [:(1TopSp {1}),(Sspace 0[01]):], the carrier of (Tunit_circle 2):] is non empty set
dom (CircleMap * ([:(1TopSp {1}),(Sspace 0[01]):] --> S)) is Element of bool the carrier of [:(1TopSp {1}),(Sspace 0[01]):]
bool the carrier of [:(1TopSp {1}),(Sspace 0[01]):] is non empty set
yt | [: the carrier of (1TopSp {1}),{0}:] is Relation-like the carrier of [:(1TopSp {1}),I[01]:] -defined the carrier of (Tunit_circle 2) -valued Function-like Element of bool [: the carrier of [:(1TopSp {1}),I[01]:], the carrier of (Tunit_circle 2):]
Qt is set
(yt | [: the carrier of (1TopSp {1}),{0}:]) . Qt is set
(CircleMap * ([:(1TopSp {1}),(Sspace 0[01]):] --> S)) . Qt is set
Ft is set
ft0 is set
[Ft,ft0] is set
{Ft,ft0} is non empty set
{Ft} is non empty set
{{Ft,ft0},{Ft}} is non empty set
yt . (Ft,ft0) is set
yt . [Ft,ft0] is set
x . ft0 is set
([:(1TopSp {1}),(Sspace 0[01]):] --> S) . Qt is V11() ext-real real Element of REAL
CircleMap . (([:(1TopSp {1}),(Sspace 0[01]):] --> S) . Qt) is set
dom yt is Element of bool the carrier of [:(1TopSp {1}),I[01]:]
dom (yt | [: the carrier of (1TopSp {1}),{0}:]) is Element of bool the carrier of [:(1TopSp {1}),I[01]:]
[: the carrier of [:(1TopSp {1}),I[01]:], the carrier of R^1:] is non empty V203() V204() V205() set
bool [: the carrier of [:(1TopSp {1}),I[01]:], the carrier of R^1:] is non empty set
Qt is non empty Relation-like the carrier of [:(1TopSp {1}),I[01]:] -defined the carrier of R^1 -valued Function-like V26( the carrier of [:(1TopSp {1}),I[01]:]) quasi_total V203() V204() V205() Element of bool [: the carrier of [:(1TopSp {1}),I[01]:], the carrier of R^1:]
CircleMap * Qt is non empty Relation-like the carrier of [:(1TopSp {1}),I[01]:] -defined the carrier of (Tunit_circle 2) -valued Function-like V26( the carrier of [:(1TopSp {1}),I[01]:]) quasi_total Element of bool [: the carrier of [:(1TopSp {1}),I[01]:], the carrier of (Tunit_circle 2):]
Qt | [: the carrier of (1TopSp {1}),{0}:] is Relation-like the carrier of [:(1TopSp {1}),I[01]:] -defined the carrier of R^1 -valued Function-like V203() V204() V205() Element of bool [: the carrier of [:(1TopSp {1}),I[01]:], the carrier of R^1:]
((1TopSp {1}),I[01],R^1,Qt,ftm) 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:]
Ft 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:]
Ft . 0 is V11() ext-real real Element of REAL
CircleMap * Ft 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):]
Qt . (ftm,j0) is set
[ftm,j0] is set
Qt . [ftm,j0] is V11() ext-real real set
([:(1TopSp {1}),(Sspace 0[01]):] --> S) . [ftm,j0] is V11() ext-real real Element of REAL
ft0 is V11() ext-real real Element of the carrier of I[01]
x . ft0 is Element of the carrier of (Tunit_circle 2)
(CircleMap * Ft) . ft0 is Element of the carrier of (Tunit_circle 2)
Ft . ft0 is V11() ext-real real Element of the carrier of R^1
CircleMap . (Ft . ft0) is Element of the carrier of (Tunit_circle 2)
Qt . (ftm,ft0) is set
[ftm,ft0] is set
{ftm,ft0} is non empty set
{{ftm,ft0},{ftm}} is non empty set
Qt . [ftm,ft0] is V11() ext-real real set
CircleMap . (Qt . (ftm,ft0)) is set
(CircleMap * Qt) . (ftm,ft0) is set
(CircleMap * Qt) . [ftm,ft0] is set
ft0 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:]
CircleMap * ft0 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):]
ft0 . 0 is V11() ext-real real Element of REAL
[:[: the carrier of (1TopSp {1}), the carrier of I[01]:], the carrier of R^1:] is non empty V203() V204() V205() set
bool [:[: the carrier of (1TopSp {1}), the carrier of I[01]:], the carrier of R^1:] is non empty set
ft1 is non empty Relation-like [: the carrier of (1TopSp {1}), the carrier of I[01]:] -defined the carrier of R^1 -valued Function-like V26([: the carrier of (1TopSp {1}), the carrier of I[01]:]) quasi_total V203() V204() V205() Element of bool [:[: the carrier of (1TopSp {1}), the carrier of I[01]:], the carrier of R^1:]
ftn is non empty Relation-like the carrier of [:(1TopSp {1}),I[01]:] -defined the carrier of R^1 -valued Function-like V26( the carrier of [:(1TopSp {1}),I[01]:]) quasi_total V203() V204() V205() Element of bool [: the carrier of [:(1TopSp {1}),I[01]:], the carrier of R^1:]
ft is Element of the carrier of [:(1TopSp {1}),I[01]:]
ftn . ft is V11() ext-real real Element of the carrier of R^1
G is V213() V214() V215() Element of bool the carrier of R^1
sM0 is Element of the carrier of (1TopSp {1})
g2 is V11() ext-real real Element of the carrier of I[01]
[sM0,g2] is Element of the carrier of [:(1TopSp {1}),I[01]:]
{sM0,g2} is non empty set
{sM0} is non empty set
{{sM0,g2},{sM0}} is non empty set
ftn . (sM0,g2) is set
[sM0,g2] is set
ftn . [sM0,g2] is V11() ext-real real set
ft0 . g2 is V11() ext-real real Element of the carrier of R^1
ft2 is V213() V214() V215() Element of bool the carrier of I[01]
ft0 .: ft2 is V213() V214() V215() Element of bool the carrier of R^1
[:([#] (1TopSp {1})),ft2:] is V203() V204() V205() Element of bool the carrier of [:(1TopSp {1}),I[01]:]
sM1 is V203() V204() V205() Element of bool the carrier of [:(1TopSp {1}),I[01]:]
ftn .: sM1 is V213() V214() V215() Element of bool the carrier of R^1
Qt is set
Qt is Element of the carrier of [:(1TopSp {1}),I[01]:]
ftn . Qt is V11() ext-real real Element of the carrier of R^1
G is set
F1 is set
[G,F1] is set
{G,F1} is non empty set
{G} is non empty set
{{G,F1},{G}} is non empty set
ft0 . F1 is V11() ext-real real Element of REAL
ftn . (G,F1) is set
ftn . [G,F1] is V11() ext-real real set
CircleMap * ftn is non empty Relation-like the carrier of [:(1TopSp {1}),I[01]:] -defined the carrier of (Tunit_circle 2) -valued Function-like V26( the carrier of [:(1TopSp {1}),I[01]:]) quasi_total Element of bool [: the carrier of [:(1TopSp {1}),I[01]:], the carrier of (Tunit_circle 2):]
ft is Element of the carrier of [:(1TopSp {1}),I[01]:]
yt . ft is Element of the carrier of (Tunit_circle 2)
(CircleMap * ftn) . ft is Element of the carrier of (Tunit_circle 2)
G is Element of the carrier of (1TopSp {1})
sM0 is V11() ext-real real Element of the carrier of I[01]
[G,sM0] is Element of the carrier of [:(1TopSp {1}),I[01]:]
{G,sM0} is non empty set
{G} is non empty set
{{G,sM0},{G}} is non empty set
ftn . (G,sM0) is set
[G,sM0] is set
ftn . [G,sM0] is V11() ext-real real set
CircleMap . (ftn . (G,sM0)) is set
ft0 . sM0 is V11() ext-real real Element of the carrier of R^1
CircleMap . (ft0 . sM0) is Element of the carrier of (Tunit_circle 2)
(CircleMap * ft0) . sM0 is Element of the carrier of (Tunit_circle 2)
yt . (G,sM0) is set
yt . [G,sM0] is set
ft is V11() ext-real real Element of the carrier of I[01]
Ft . ft is V11() ext-real real Element of the carrier of R^1
ft0 . ft is V11() ext-real real Element of the carrier of R^1
dom ftn is Element of bool the carrier of [:(1TopSp {1}),I[01]:]
ftn | [: the carrier of (1TopSp {1}),{0}:] is Relation-like the carrier of [:(1TopSp {1}),I[01]:] -defined the carrier of R^1 -valued Function-like V203() V204() V205() Element of bool [: the carrier of [:(1TopSp {1}),I[01]:], the carrier of R^1:]
dom (ftn | [: the carrier of (1TopSp {1}),{0}:]) is Element of bool the carrier of [:(1TopSp {1}),I[01]:]
G is set
(ftn | [: the carrier of (1TopSp {1}),{0}:]) . G is V11() ext-real real Element of REAL
([:(1TopSp {1}),(Sspace 0[01]):] --> S) . G is V11() ext-real real Element of REAL
sM0 is set
g2 is set
[sM0,g2] is set
{sM0,g2} is non empty set
{sM0} is non empty set
{{sM0,g2},{sM0}} is non empty set
ftn . (sM0,g2) is set
ftn . [sM0,g2] is V11() ext-real real set
ft0 . g2 is V11() ext-real real Element of REAL
dom ([:(1TopSp {1}),(Sspace 0[01]):] --> S) is Element of bool the carrier of [:(1TopSp {1}),(Sspace 0[01]):]
Qt . (ftm,ft) is set
[ftm,ft] is set
{ftm,ft} is non empty set
{{ftm,ft},{ftm}} is non empty set
Qt . [ftm,ft] is V11() ext-real real set
ftn . (ftm,ft) is set
ftn . [ftm,ft] is V11() ext-real real set
S is Element of the carrier of (Tunit_circle 2)
x is Element of the carrier of (Tunit_circle 2)
{S} is non empty connected compact Element of bool the carrier of (Tunit_circle 2)
CircleMap " {S} is V213() V214() V215() Element of bool the carrier of R^1
{x} is non empty connected compact Element of bool the carrier of (Tunit_circle 2)
CircleMap " {x} is V213() V214() V215() Element of bool the carrier of R^1
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 continuous Path of S,x
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 continuous Path of S,x
x is non empty Relation-like the carrier of [:I[01],I[01]:] -defined the carrier of (Tunit_circle 2) -valued Function-like V26( the carrier of [:I[01],I[01]:]) quasi_total Homotopy of y,S
F is V11() ext-real real Element of the carrier of R^1
the non empty Relation-like the carrier of I[01] -defined the carrier of (Tunit_circle 2) -valued Function-like constant V26( the carrier of I[01]) quasi_total continuous Path of S,S is non empty Relation-like the carrier of I[01] -defined the carrier of (Tunit_circle 2) -valued Function-like constant V26( the carrier of I[01]) quasi_total continuous Path of S,S
I[01] --> F 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:]
K178( the carrier of R^1, the carrier of I[01],F) 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:]
the non empty Relation-like the carrier of I[01] -defined the carrier of (Tunit_circle 2) -valued Function-like constant V26( the carrier of I[01]) quasi_total continuous Path of x,x is non empty Relation-like the carrier of I[01] -defined the carrier of (Tunit_circle 2) -valued Function-like constant V26( the carrier of I[01]) quasi_total continuous Path of x,x
Qt 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:]
Qt . 0 is V11() ext-real real Element of REAL
CircleMap * Qt 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):]
Ft is V11() ext-real real Element of the carrier of I[01]
Qt . Ft is V11() ext-real real Element of REAL
[: the carrier of I[01],{0}:] is non empty RAT -valued INT -valued V203() V204() V205() V206() set
[:[: the carrier of I[01],{0}:],REAL:] is non empty V203() V204() V205() set
bool [:[: the carrier of I[01],{0}:],REAL:] is non empty set
Ft is non empty Relation-like [: the carrier of I[01],{0}:] -defined REAL -valued Function-like V26([: the carrier of I[01],{0}:]) quasi_total V203() V204() V205() Element of bool [:[: the carrier of I[01],{0}:],REAL:]
CircleMap . F is Element of the carrier of (Tunit_circle 2)
CircleMap * (I[01] --> F) 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):]
ft0 is V11() ext-real real Element of the carrier of I[01]
the non empty Relation-like the carrier of I[01] -defined the carrier of (Tunit_circle 2) -valued Function-like constant V26( the carrier of I[01]) quasi_total continuous Path of S,S . ft0 is Element of the carrier of (Tunit_circle 2)
(CircleMap * (I[01] --> F)) . ft0 is Element of the carrier of (Tunit_circle 2)
(I[01] --> F) . ft0 is V11() ext-real real Element of the carrier of R^1
CircleMap . ((I[01] --> F) . ft0) is Element of the carrier of (Tunit_circle 2)
ft0 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:]
ft0 . 0 is V11() ext-real real Element of REAL
CircleMap * ft0 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):]
j0 is V11() ext-real real Element of the carrier of I[01]
(I[01] --> F) . j0 is V11() ext-real real Element of the carrier of R^1
rng Ft is V213() V214() V215() Element of bool REAL
dom Ft is Relation-like the carrier of I[01] -defined INT -valued {0} -valued V203() V204() V205() V206() Element of bool [: the carrier of I[01],{0}:]
bool [: the carrier of I[01],{0}:] is non empty set
[:I[01],(Sspace 0[01]):] is non empty strict TopSpace-like T_0 T_1 T_2 TopStruct
the carrier of [:I[01],(Sspace 0[01]):] is non empty set
[: the carrier of I[01], the carrier of (Sspace 0[01]):] is non empty V203() V204() V205() set
[: the carrier of [:I[01],(Sspace 0[01]):], the carrier of R^1:] is non empty V203() V204() V205() set
bool [: the carrier of [:I[01],(Sspace 0[01]):], the carrier of R^1:] is non empty set
ft1 is non empty Relation-like the carrier of [:I[01],(Sspace 0[01]):] -defined the carrier of R^1 -valued Function-like V26( the carrier of [:I[01],(Sspace 0[01]):]) quasi_total V203() V204() V205() Element of bool [: the carrier of [:I[01],(Sspace 0[01]):], the carrier of R^1:]
CircleMap * ft1 is non empty Relation-like the carrier of [:I[01],(Sspace 0[01]):] -defined the carrier of (Tunit_circle 2) -valued Function-like V26( the carrier of [:I[01],(Sspace 0[01]):]) quasi_total Element of bool [: the carrier of [:I[01],(Sspace 0[01]):], the carrier of (Tunit_circle 2):]
[: the carrier of [:I[01],(Sspace 0[01]):], the carrier of (Tunit_circle 2):] is non empty set
bool [: the carrier of [:I[01],(Sspace 0[01]):], the carrier of (Tunit_circle 2):] is non empty set
dom (CircleMap * ft1) is Element of bool the carrier of [:I[01],(Sspace 0[01]):]
bool the carrier of [:I[01],(Sspace 0[01]):] is non empty set
x | [: the carrier of I[01],{0}:] is Relation-like the carrier of [:I[01],I[01]:] -defined the carrier of (Tunit_circle 2) -valued Function-like Element of bool [: the carrier of [:I[01],I[01]:], the carrier of (Tunit_circle 2):]
[: the carrier of [:I[01],I[01]:], the carrier of (Tunit_circle 2):] is non empty set
bool [: the carrier of [:I[01],I[01]:], the carrier of (Tunit_circle 2):] is non empty set
ftn is set
(x | [: the carrier of I[01],{0}:]) . ftn is set
(CircleMap * ft1) . ftn is set
ft is set
G is set
[ft,G] is set
{ft,G} is non empty set
{ft} is non empty set
{{ft,G},{ft}} is non empty set
x . (ft,0) is set
[ft,0] is set
{ft,0} is non empty set
{{ft,0},{ft}} is non empty set
x . [ft,0] is set
(CircleMap * Qt) . ft is set
Qt . ft is V11() ext-real real Element of REAL
CircleMap . (Qt . ft) is set
ft1 . (ft,G) is set
ft1 . [ft,G] is V11() ext-real real set
CircleMap . (ft1 . (ft,G)) is set
ftn is Element of the carrier of [:I[01],(Sspace 0[01]):]
ft1 . ftn is V11() ext-real real Element of the carrier of R^1
ft is V213() V214() V215() Element of bool the carrier of R^1
G is V11() ext-real real Element of the carrier of I[01]
sM0 is V11() ext-real real Element of the carrier of (Sspace 0[01])
[G,sM0] is Element of the carrier of [:I[01],(Sspace 0[01]):]
{G,sM0} is non empty V213() V214() V215() set
{G} is non empty V213() V214() V215() set
{{G,sM0},{G}} is non empty set
ft1 . (G,sM0) is set
[G,sM0] is set
ft1 . [G,sM0] is V11() ext-real real set
Qt . G is V11() ext-real real Element of REAL
g2 is V213() V214() V215() Element of bool the carrier of I[01]
Qt .: g2 is V213() V214() V215() Element of bool the carrier of R^1
ft2 is non empty V213() V214() V215() Element of bool the carrier of I[01]
[:ft2,([#] (Sspace 0[01])):] is non empty V203() V204() V205() Element of bool the carrier of [:I[01],(Sspace 0[01]):]
sM1 is non empty V203() V204() V205() Element of bool the carrier of [:I[01],(Sspace 0[01]):]
ft1 .: sM1 is V213() V214() V215() Element of bool the carrier of R^1
Qt is set
Qt is Element of the carrier of [:I[01],(Sspace 0[01]):]
ft1 . Qt is V11() ext-real real Element of the carrier of R^1
G is V11() ext-real real Element of ft2
F1 is V11() ext-real real Element of the carrier of (Sspace 0[01])
[G,F1] is Element of the carrier of [:I[01],(Sspace 0[01]):]
{G,F1} is non empty V213() V214() V215() set
{G} is non empty V213() V214() V215() set
{{G,F1},{G}} is non empty set
ft1 . (G,F1) is set
[G,F1] is set
ft1 . [G,F1] is V11() ext-real real set
Qt . G is V11() ext-real real Element of REAL
Qt . G is V11() ext-real real Element of the carrier of R^1
Qt .: ft2 is V213() V214() V215() Element of bool the carrier of R^1
j1 is V11() ext-real real Element of the carrier of I[01]
Qt . j1 is V11() ext-real real Element of the carrier of R^1
ftn is V11() ext-real real Element of the carrier of R^1
[j1,j0] is Element of the carrier of [:I[01],I[01]:]
{j1,j0} is non empty V213() V214() V215() set
{j1} is non empty V213() V214() V215() set
{{j1,j0},{j1}} is non empty set
[j0,j0] is Element of the carrier of [:I[01],I[01]:]
{j0,j0} is non empty V213() V214() V215() set
{j0} is non empty V213() V214() V215() set
{{j0,j0},{j0}} is non empty set
dom x is Element of bool the carrier of [:I[01],I[01]:]
dom (x | [: the carrier of I[01],{0}:]) is Element of bool the carrier of [:I[01],I[01]:]
[: the carrier of [:I[01],I[01]:], the carrier of R^1:] is non empty V203() V204() V205() set
bool [: the carrier of [:I[01],I[01]:], the carrier of R^1:] is non empty set
G is non empty Relation-like the carrier of [:I[01],I[01]:] -defined the carrier of R^1 -valued Function-like V26( the carrier of [:I[01],I[01]:]) quasi_total V203() V204() V205() Element of bool [: the carrier of [:I[01],I[01]:], the carrier of R^1:]
CircleMap * G is non empty Relation-like the carrier of [:I[01],I[01]:] -defined the carrier of (Tunit_circle 2) -valued Function-like V26( the carrier of [:I[01],I[01]:]) quasi_total Element of bool [: the carrier of [:I[01],I[01]:], the carrier of (Tunit_circle 2):]
G | [: the carrier of I[01],{0}:] is Relation-like the carrier of [:I[01],I[01]:] -defined the carrier of R^1 -valued Function-like V203() V204() V205() Element of bool [: the carrier of [:I[01],I[01]:], the carrier of R^1:]
(I[01],I[01],R^1,G,j0) 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:]
CircleMap * (I[01],I[01],R^1,G,j0) 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):]
g2 is V11() ext-real real Element of the carrier of I[01]
the non empty Relation-like the carrier of I[01] -defined the carrier of (Tunit_circle 2) -valued Function-like constant V26( the carrier of I[01]) quasi_total continuous Path of S,S . g2 is Element of the carrier of (Tunit_circle 2)
(CircleMap * (I[01],I[01],R^1,G,j0)) . g2 is Element of the carrier of (Tunit_circle 2)
(I[01],I[01],R^1,G,j0) . g2 is V11() ext-real real Element of the carrier of R^1
CircleMap . ((I[01],I[01],R^1,G,j0) . g2) is Element of the carrier of (Tunit_circle 2)
G . (j0,g2) is set
[j0,g2] is set
{j0,g2} is non empty V213() V214() V215() set
{{j0,g2},{j0}} is non empty set
G . [j0,g2] is V11() ext-real real set
CircleMap . (G . (j0,g2)) is set
(CircleMap * G) . (j0,g2) is set
(CircleMap * G) . [j0,g2] is set
I[01] --> ftn 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:]
K178( the carrier of R^1, the carrier of I[01],ftn) 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:]
CircleMap . ftn is Element of the carrier of (Tunit_circle 2)
y . j1 is Element of the carrier of (Tunit_circle 2)
CircleMap * (I[01] --> ftn) 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):]
ft2 is V11() ext-real real Element of the carrier of I[01]
the non empty Relation-like the carrier of I[01] -defined the carrier of (Tunit_circle 2) -valued Function-like constant V26( the carrier of I[01]) quasi_total continuous Path of x,x . ft2 is Element of the carrier of (Tunit_circle 2)
(CircleMap * (I[01] --> ftn)) . ft2 is Element of the carrier of (Tunit_circle 2)
(I[01] --> ftn) . ft2 is V11() ext-real real Element of the carrier of R^1
CircleMap . ((I[01] --> ftn) . ft2) is Element of the carrier of (Tunit_circle 2)
ft2 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:]
ft2 . 0 is V11() ext-real real Element of REAL
CircleMap * ft2 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):]
(I[01] --> ftn) . j0 is V11() ext-real real Element of the carrier of R^1
(I[01],I[01],R^1,G,j1) 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:]
CircleMap * (I[01],I[01],R^1,G,j1) 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):]
Qt is V11() ext-real real Element of the carrier of I[01]
the non empty Relation-like the carrier of I[01] -defined the carrier of (Tunit_circle 2) -valued Function-like constant V26( the carrier of I[01]) quasi_total continuous Path of x,x . Qt is Element of the carrier of (Tunit_circle 2)
(CircleMap * (I[01],I[01],R^1,G,j1)) . Qt is Element of the carrier of (Tunit_circle 2)
(I[01],I[01],R^1,G,j1) . Qt is V11() ext-real real Element of the carrier of R^1
CircleMap . ((I[01],I[01],R^1,G,j1) . Qt) is Element of the carrier of (Tunit_circle 2)
G . (j1,Qt) is set
[j1,Qt] is set
{j1,Qt} is non empty V213() V214() V215() set
{{j1,Qt},{j1}} is non empty set
G . [j1,Qt] is V11() ext-real real set
CircleMap . (G . (j1,Qt)) is set
(CircleMap * G) . (j1,Qt) is set
(CircleMap * G) . [j1,Qt] is set
(I[01],I[01],R^1,G,j1) . 0 is V11() ext-real real Element of REAL
G . (j1,j0) is set
[j1,j0] is set
G . [j1,j0] is V11() ext-real real set
ft1 . (j1,j0) is set
ft1 . [j1,j0] is V11() ext-real real set
(I[01],I[01],R^1,G,j0) . 0 is V11() ext-real real Element of REAL
G . (j0,j0) is set
[j0,j0] is set
G . [j0,j0] is V11() ext-real real set
ft1 . (j0,j0) is set
ft1 . [j0,j0] is V11() ext-real real set
(I[01],I[01],R^1,G,j1) 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:]
(I[01],I[01],R^1,G,j1) . 0 is V11() ext-real real Element of REAL
G . (j0,j1) is set
[j0,j1] is set
{j0,j1} is non empty V213() V214() V215() set
{{j0,j1},{j0}} is non empty set
G . [j0,j1] is V11() ext-real real set
(I[01],I[01],R^1,G,j0) . j1 is V11() ext-real real Element of the carrier of R^1
(I[01],I[01],R^1,G,j1) . 1 is V11() ext-real real Element of REAL
G . (j1,j1) is set
[j1,j1] is set
{j1,j1} is non empty V213() V214() V215() set
{{j1,j1},{j1}} is non empty set
G . [j1,j1] is V11() ext-real real set
(I[01],I[01],R^1,G,j1) . j1 is V11() ext-real real Element of the carrier of R^1
G is V11() ext-real real Element of the carrier of I[01]
[G,0] is Element of [: the carrier of I[01],REAL:]
[: the carrier of I[01],REAL:] is non empty V203() V204() V205() set
{G,0} is non empty V213() V214() V215() set
{G} is non empty V213() V214() V215() set
{{G,0},{G}} is non empty set
G . (G,0) is set
[G,0] is set
G . [G,0] is V11() ext-real real set
ft1 . (G,j0) is set
[G,j0] is set
{G,j0} is non empty V213() V214() V215() set
{{G,j0},{G}} is non empty set
ft1 . [G,j0] is V11() ext-real real set
ft 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 F,ftn
ft . G is V11() ext-real real Element of the carrier of R^1
G . (G,1) is set
[G,1] is set
{G,1} is non empty V213() V214() V215() set
{{G,1},{G}} is non empty set
G . [G,1] is V11() ext-real real set
Qt 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 F,ftn
Qt . G is V11() ext-real real Element of the carrier of R^1
F1 is V11() ext-real real Element of the carrier of I[01]
G . (0,F1) is set
[0,F1] is set
{0,F1} is non empty V213() V214() V215() set
{0} is non empty V213() V214() V215() V216() V217() V218() V315() V317() set
{{0,F1},{0}} is non empty set
G . [0,F1] is V11() ext-real real set
(I[01],I[01],R^1,G,j0) . F1 is V11() ext-real real Element of the carrier of R^1
G . (1,F1) is set
[1,F1] is set
{1,F1} is non empty V213() V214() V215() set
{1} is non empty V213() V214() V215() V216() V217() V218() V315() V317() set
{{1,F1},{1}} is non empty set
G . [1,F1] is V11() ext-real real set
(I[01],I[01],R^1,G,j1) . F1 is V11() ext-real real Element of the carrier of R^1
G is non empty Relation-like the carrier of [:I[01],I[01]:] -defined the carrier of R^1 -valued Function-like V26( the carrier of [:I[01],I[01]:]) quasi_total continuous V203() V204() V205() Homotopy of ft,Qt
CircleMap * G is non empty Relation-like the carrier of [:I[01],I[01]:] -defined the carrier of [:I[01],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],I[01]:]) V26( the carrier of [:I[01],I[01]:]) quasi_total quasi_total continuous Element of bool [: the carrier of [:I[01],I[01]:], the carrier of (Tunit_circle 2):]
F1 is non empty Relation-like the carrier of [:I[01],I[01]:] -defined the carrier of R^1 -valued Function-like V26( the carrier of [:I[01],I[01]:]) quasi_total continuous V203() V204() V205() Homotopy of ft,Qt
CircleMap * F1 is non empty Relation-like the carrier of [:I[01],I[01]:] -defined the carrier of [:I[01],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],I[01]:]) V26( the carrier of [:I[01],I[01]:]) quasi_total quasi_total continuous Element of bool [: the carrier of [:I[01],I[01]:], the carrier of (Tunit_circle 2):]
dom F1 is Element of bool the carrier of [:I[01],I[01]:]
F1 | [: the carrier of I[01],{0}:] is Relation-like the carrier of [:I[01],I[01]:] -defined the carrier of R^1 -valued Function-like V203() V204() V205() Element of bool [: the carrier of [:I[01],I[01]:], the carrier of R^1:]
dom (F1 | [: the carrier of I[01],{0}:]) is Element of bool the carrier of [:I[01],I[01]:]
x is set
(F1 | [: the carrier of I[01],{0}:]) . x is V11() ext-real real Element of REAL
ft1 . x is V11() ext-real real Element of REAL
x1 is set
x2 is set
[x1,x2] is set
{x1,x2} is non empty set
{x1} is non empty set
{{x1,x2},{x1}} is non empty set
F1 . (x1,x2) is set
F1 . [x1,x2] is V11() ext-real real set
ft . x1 is V11() ext-real real Element of REAL
ft1 . (x1,x2) is set
ft1 . [x1,x2] is V11() ext-real real set
FundamentalGroup ((Tunit_circle 2),c[10]) is non empty strict V184() V185() V186() V235() V236() V237() V238() V239() V240() multMagma
the carrier of (FundamentalGroup ((Tunit_circle 2),c[10])) is non empty set
[: the carrier of INT.Group, the carrier of (FundamentalGroup ((Tunit_circle 2),c[10])):] is non empty set
bool [: the carrier of INT.Group, the carrier of (FundamentalGroup ((Tunit_circle 2),c[10])):] is non empty set
Loops c[10] is non empty set
Paths (c[10],c[10]) is non empty set
EqRel ((Tunit_circle 2),c[10]) is non empty Relation-like Loops c[10] -defined Loops c[10] -valued V26( Loops c[10]) quasi_total V264() V269() Element of bool [:(Loops c[10]),(Loops c[10]):]
[:(Loops c[10]),(Loops c[10]):] is non empty set
bool [:(Loops c[10]),(Loops c[10]):] is non empty set
EqRel ((Tunit_circle 2),c[10],c[10]) is Relation-like Paths (c[10],c[10]) -defined Paths (c[10],c[10]) -valued Element of bool [:(Paths (c[10],c[10])),(Paths (c[10],c[10])):]
[:(Paths (c[10],c[10])),(Paths (c[10],c[10])):] is non empty set
bool [:(Paths (c[10],c[10])),(Paths (c[10],c[10])):] is non empty set
S is V11() ext-real real integer V34() Element of INT
(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 continuous Path of c[10] , c[10]
Class ((EqRel ((Tunit_circle 2),c[10])),(S)) is Element of bool (Loops c[10])
bool (Loops c[10]) is non empty set
x is Element of the carrier of (FundamentalGroup ((Tunit_circle 2),c[10]))
[:INT, the carrier of (FundamentalGroup ((Tunit_circle 2),c[10])):] is non empty set
bool [:INT, the carrier of (FundamentalGroup ((Tunit_circle 2),c[10])):] is non empty set
S is non empty Relation-like INT -defined the carrier of (FundamentalGroup ((Tunit_circle 2),c[10])) -valued Function-like V26( INT ) quasi_total Element of bool [:INT, the carrier of (FundamentalGroup ((Tunit_circle 2),c[10])):]
x is non empty Relation-like the carrier of INT.Group -defined the carrier of (FundamentalGroup ((Tunit_circle 2),c[10])) -valued Function-like V26( the carrier of INT.Group) quasi_total Element of bool [: the carrier of INT.Group, the carrier of (FundamentalGroup ((Tunit_circle 2),c[10])):]
y is V11() ext-real real integer set
x . y is set
(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 continuous Path of c[10] , c[10]
Class ((EqRel ((Tunit_circle 2),c[10])),(y)) is Element of bool (Loops c[10])
bool (Loops c[10]) is non empty set
S is non empty Relation-like the carrier of INT.Group -defined the carrier of (FundamentalGroup ((Tunit_circle 2),c[10])) -valued Function-like V26( the carrier of INT.Group) quasi_total Element of bool [: the carrier of INT.Group, the carrier of (FundamentalGroup ((Tunit_circle 2),c[10])):]
x is non empty Relation-like the carrier of INT.Group -defined the carrier of (FundamentalGroup ((Tunit_circle 2),c[10])) -valued Function-like V26( the carrier of INT.Group) quasi_total Element of bool [: the carrier of INT.Group, the carrier of (FundamentalGroup ((Tunit_circle 2),c[10])):]
y is V11() ext-real real integer V34() Element of the carrier of INT.Group
S . y is Element of the carrier of (FundamentalGroup ((Tunit_circle 2),c[10]))
x . y is Element of the carrier of (FundamentalGroup ((Tunit_circle 2),c[10]))
(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 continuous Path of c[10] , c[10]
Class ((EqRel ((Tunit_circle 2),c[10])),(y)) is Element of bool (Loops c[10])
bool (Loops c[10]) is non empty set
() is non empty Relation-like the carrier of INT.Group -defined the carrier of (FundamentalGroup ((Tunit_circle 2),c[10])) -valued Function-like V26( the carrier of INT.Group) quasi_total Element of bool [: the carrier of INT.Group, the carrier of (FundamentalGroup ((Tunit_circle 2),c[10])):]
S is V11() ext-real real integer set
R^1 S is V11() ext-real real Element of the carrier of R^1
() . S is set
x 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
CircleMap * x 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):]
Class ((EqRel ((Tunit_circle 2),c[10])),(CircleMap * x)) is Element of bool (Loops c[10])
bool (Loops c[10]) is non empty set
(CircleMap * x) . 0 is set
j0 is V11() ext-real real Element of the carrier of I[01]
x . j0 is V11() ext-real real Element of the carrier of R^1
CircleMap . (x . j0) is Element of the carrier of (Tunit_circle 2)
CircleMap . (R^1 0) is Element of the carrier of (Tunit_circle 2)
CircleMap . 0 is set
(2 * PI) * 0 is V11() ext-real real Element of REAL
cos ((2 * PI) * 0) is V11() ext-real real Element of REAL
sin ((2 * PI) * 0) is V11() ext-real real Element of REAL
|[(cos ((2 * PI) * 0)),(sin ((2 * PI) * 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)
(CircleMap * x) . 1 is set
j1 is V11() ext-real real Element of the carrier of I[01]
x . j1 is V11() ext-real real Element of the carrier of R^1
CircleMap . (x . j1) is Element of the carrier of (Tunit_circle 2)
CircleMap . (R^1 S) is Element of the carrier of (Tunit_circle 2)
CircleMap . S is set
(2 * PI) * S is V11() ext-real real Element of REAL
((2 * PI) * S) + 0 is V11() ext-real real Element of REAL
cos (((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 (((2 * PI) * S) + 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)
|[(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 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 continuous Path of c[10] , c[10]
(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
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 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 continuous Path of c[10] , c[10]
x is non empty TopSpace-like connected V302() pathwise_connected interval SubSpace of R^1
the carrier of x is non empty V213() V214() V215() set
F is V11() ext-real real Element of the carrier of x
ftm is V11() ext-real real Element of the carrier of x
[: the carrier of [:I[01],I[01]:], the carrier of R^1:] is non empty V203() V204() V205() set
bool [: the carrier of [:I[01],I[01]:], the carrier of R^1:] is non empty set
yt is non empty Relation-like the carrier of I[01] -defined the carrier of x -valued Function-like V26( the carrier of I[01]) quasi_total continuous V203() V204() V205() Path of F,ftm
Pt is non empty Relation-like the carrier of I[01] -defined the carrier of x -valued Function-like V26( the carrier of I[01]) quasi_total continuous V203() V204() V205() Path of F,ftm
R1Homotopy (yt,Pt) is non empty Relation-like the carrier of [:I[01],I[01]:] -defined the carrier of x -valued Function-like V26( the carrier of [:I[01],I[01]:]) quasi_total continuous V203() V204() V205() Element of bool [: the carrier of [:I[01],I[01]:], the carrier of x:]
[: the carrier of [:I[01],I[01]:], the carrier of x:] is non empty V203() V204() V205() set
bool [: the carrier of [:I[01],I[01]:], the carrier of x:] is non empty set
[: the carrier of [:I[01],I[01]:], the carrier of (Tunit_circle 2):] is non empty set
bool [: the carrier of [:I[01],I[01]:], the carrier of (Tunit_circle 2):] is non empty set
Qt is non empty Relation-like the carrier of [:I[01],I[01]:] -defined the carrier of R^1 -valued Function-like V26( the carrier of [:I[01],I[01]:]) quasi_total V203() V204() V205() Element of bool [: the carrier of [:I[01],I[01]:], the carrier of R^1:]
CircleMap * Qt is non empty Relation-like the carrier of [:I[01],I[01]:] -defined the carrier of (Tunit_circle 2) -valued Function-like V26( the carrier of [:I[01],I[01]:]) quasi_total Element of bool [: the carrier of [:I[01],I[01]:], the carrier of (Tunit_circle 2):]
Ft is non empty Relation-like the carrier of [:I[01],I[01]:] -defined the carrier of (Tunit_circle 2) -valued Function-like V26( the carrier of [:I[01],I[01]:]) quasi_total Element of bool [: the carrier of [:I[01],I[01]:], the carrier of (Tunit_circle 2):]
ft0 is V11() ext-real real Element of the carrier of I[01]
Ft . (ft0,0) is set
[ft0,0] is set
{ft0,0} is non empty V213() V214() V215() set
{ft0} is non empty V213() V214() V215() set
{{ft0,0},{ft0}} is non empty set
Ft . [ft0,0] is set
(S) . ft0 is Element of the carrier of (Tunit_circle 2)
Ft . (ft0,1) is set
[ft0,1] is set
{ft0,1} is non empty V213() V214() V215() set
{{ft0,1},{ft0}} is non empty set
Ft . [ft0,1] is set
S . ft0 is Element of the carrier of (Tunit_circle 2)
Ft . (0,ft0) is set
[0,ft0] is set
{0,ft0} is non empty V213() V214() V215() set
{0} is non empty V213() V214() V215() V216() V217() V218() V315() V317() set
{{0,ft0},{0}} is non empty set
Ft . [0,ft0] is set
Ft . (1,ft0) is set
[1,ft0] is set
{1,ft0} is non empty V213() V214() V215() set
{1} is non empty V213() V214() V215() V216() V217() V218() V315() V317() set
{{1,ft0},{1}} is non empty set
Ft . [1,ft0] is set
Qt . (ft0,j0) is set
[ft0,j0] is set
{ft0,j0} is non empty V213() V214() V215() set
{{ft0,j0},{ft0}} is non empty set
Qt . [ft0,j0] is V11() ext-real real set
CircleMap . (Qt . (ft0,j0)) is set
1 - j0 is V11() ext-real real Element of REAL
(S) . ft0 is V11() ext-real real Element of the carrier of R^1
(1 - j0) * ((S) . ft0) is V11() ext-real real Element of REAL
x . ft0 is V11() ext-real real Element of the carrier of R^1
j0 * (x . ft0) is V11() ext-real real set
((1 - j0) * ((S) . ft0)) + (j0 * (x . ft0)) is V11() ext-real real Element of REAL
CircleMap . (((1 - j0) * ((S) . ft0)) + (j0 * (x . ft0))) is set
Qt . (ft0,j1) is set
[ft0,j1] is set
{ft0,j1} is non empty V213() V214() V215() set
{{ft0,j1},{ft0}} is non empty set
Qt . [ft0,j1] is V11() ext-real real set
CircleMap . (Qt . (ft0,j1)) is set
1 - j1 is V11() ext-real real Element of REAL
(1 - j1) * ((S) . ft0) is V11() ext-real real Element of REAL
j1 * (x . ft0) is V11() ext-real real set
((1 - j1) * ((S) . ft0)) + (j1 * (x . ft0)) is V11() ext-real real Element of REAL
CircleMap . (((1 - j1) * ((S) . ft0)) + (j1 * (x . ft0))) is set
Qt . (j0,ft0) is set
[j0,ft0] is set
{j0,ft0} is non empty V213() V214() V215() set
{j0} is non empty V213() V214() V215() set
{{j0,ft0},{j0}} is non empty set
Qt . [j0,ft0] is V11() ext-real real set
CircleMap . (Qt . (j0,ft0)) is set
1 - ft0 is V11() ext-real real Element of REAL
(S) . j0 is V11() ext-real real Element of the carrier of R^1
(1 - ft0) * ((S) . j0) is V11() ext-real real Element of REAL
ft0 * (x . j0) is V11() ext-real real set
((1 - ft0) * ((S) . j0)) + (ft0 * (x . j0)) is V11() ext-real real Element of REAL
CircleMap . (((1 - ft0) * ((S) . j0)) + (ft0 * (x . j0))) is set
(1 - ft0) * (R^1 0) is V11() ext-real real Element of REAL
((1 - ft0) * (R^1 0)) + (ft0 * (x . j0)) is V11() ext-real real Element of REAL
CircleMap . (((1 - ft0) * (R^1 0)) + (ft0 * (x . j0))) is set
ft0 * (R^1 0) is V11() ext-real real set
((1 - ft0) * (R^1 0)) + (ft0 * (R^1 0)) is V11() ext-real real Element of REAL
CircleMap . (((1 - ft0) * (R^1 0)) + (ft0 * (R^1 0))) is set
(1 - ft0) * 0 is V11() ext-real real Element of REAL
ft0 * 0 is V11() ext-real real Element of REAL
((1 - ft0) * 0) + (ft0 * 0) is V11() ext-real real Element of REAL
CircleMap . (((1 - ft0) * 0) + (ft0 * 0)) is set
Qt . (j1,ft0) is set
[j1,ft0] is set
{j1,ft0} is non empty V213() V214() V215() set
{j1} is non empty V213() V214() V215() set
{{j1,ft0},{j1}} is non empty set
Qt . [j1,ft0] is V11() ext-real real set
CircleMap . (Qt . (j1,ft0)) is set
(S) . j1 is V11() ext-real real Element of the carrier of R^1
(1 - ft0) * ((S) . j1) is V11() ext-real real Element of REAL
ft0 * (x . j1) is V11() ext-real real set
((1 - ft0) * ((S) . j1)) + (ft0 * (x . j1)) is V11() ext-real real Element of REAL
CircleMap . (((1 - ft0) * ((S) . j1)) + (ft0 * (x . j1))) is set
(1 - ft0) * (R^1 S) is V11() ext-real real Element of REAL
((1 - ft0) * (R^1 S)) + (ft0 * (x . j1)) is V11() ext-real real Element of REAL
CircleMap . (((1 - ft0) * (R^1 S)) + (ft0 * (x . j1))) is set
ft0 * (R^1 S) is V11() ext-real real set
((1 - ft0) * (R^1 S)) + (ft0 * (R^1 S)) is V11() ext-real real Element of REAL
CircleMap . (((1 - ft0) * (R^1 S)) + (ft0 * (R^1 S))) is set
Class ((EqRel ((Tunit_circle 2),c[10])),(S)) is Element of bool (Loops c[10])
x is V11() ext-real real integer V34() Element of the carrier of INT.Group
y is V11() ext-real real integer V34() Element of the carrier of INT.Group
x * y is V11() ext-real real integer V34() Element of the carrier of INT.Group
the multF of INT.Group is non empty Relation-like [: the carrier of INT.Group, the carrier of INT.Group:] -defined the carrier of INT.Group -valued Function-like V26([: the carrier of INT.Group, the carrier of INT.Group:]) quasi_total V203() V204() V205() Element of bool [:[: the carrier of INT.Group, the carrier of INT.Group:], the carrier of INT.Group:]
[: the carrier of INT.Group, the carrier of INT.Group:] is non empty RAT -valued INT -valued V203() V204() V205() set
[:[: the carrier of INT.Group, the carrier of INT.Group:], the carrier of INT.Group:] is non empty RAT -valued INT -valued V203() V204() V205() set
bool [:[: the carrier of INT.Group, the carrier of INT.Group:], the carrier of INT.Group:] is non empty set
the multF of INT.Group . (x,y) is V11() ext-real real integer V34() Element of the carrier of INT.Group
[x,y] is set
{x,y} is non empty V213() V214() V215() V216() V217() set
{x} is non empty V213() V214() V215() V216() V217() set
{{x,y},{x}} is non empty set
the multF of INT.Group . [x,y] is V11() ext-real real set
K142(x,y) is V11() ext-real real integer V34() Element of INT
() . (x * y) is Element of the carrier of (FundamentalGroup ((Tunit_circle 2),c[10]))
() . x is Element of the carrier of (FundamentalGroup ((Tunit_circle 2),c[10]))
() . y is Element of the carrier of (FundamentalGroup ((Tunit_circle 2),c[10]))
(() . x) * (() . y) is Element of the carrier of (FundamentalGroup ((Tunit_circle 2),c[10]))
the multF of (FundamentalGroup ((Tunit_circle 2),c[10])) is non empty Relation-like [: the carrier of (FundamentalGroup ((Tunit_circle 2),c[10])), the carrier of (FundamentalGroup ((Tunit_circle 2),c[10])):] -defined the carrier of (FundamentalGroup ((Tunit_circle 2),c[10])) -valued Function-like V26([: the carrier of (FundamentalGroup ((Tunit_circle 2),c[10])), the carrier of (FundamentalGroup ((Tunit_circle 2),c[10])):]) quasi_total Element of bool [:[: the carrier of (FundamentalGroup ((Tunit_circle 2),c[10])), the carrier of (FundamentalGroup ((Tunit_circle 2),c[10])):], the carrier of (FundamentalGroup ((Tunit_circle 2),c[10])):]
[: the carrier of (FundamentalGroup ((Tunit_circle 2),c[10])), the carrier of (FundamentalGroup ((Tunit_circle 2),c[10])):] is non empty set
[:[: the carrier of (FundamentalGroup ((Tunit_circle 2),c[10])), the carrier of (FundamentalGroup ((Tunit_circle 2),c[10])):], the carrier of (FundamentalGroup ((Tunit_circle 2),c[10])):] is non empty set
bool [:[: the carrier of (FundamentalGroup ((Tunit_circle 2),c[10])), the carrier of (FundamentalGroup ((Tunit_circle 2),c[10])):], the carrier of (FundamentalGroup ((Tunit_circle 2),c[10])):] is non empty set
the multF of (FundamentalGroup ((Tunit_circle 2),c[10])) . ((() . x),(() . y)) is Element of the carrier of (FundamentalGroup ((Tunit_circle 2),c[10]))
[(() . x),(() . y)] is set
{(() . x),(() . y)} is non empty set
{(() . x)} is non empty set
{{(() . x),(() . y)},{(() . x)}} is non empty set
the multF of (FundamentalGroup ((Tunit_circle 2),c[10])) . [(() . x),(() . y)] is 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 continuous Path of c[10] , c[10]
Class ((EqRel ((Tunit_circle 2),c[10])),S) is Element of bool (Loops c[10])
bool (Loops c[10]) is non empty set
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 continuous Path of c[10] , c[10]
Class ((EqRel ((Tunit_circle 2),c[10])),x) is Element of bool (Loops c[10])
S + 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 continuous Path of c[10] , c[10]
Class ((EqRel ((Tunit_circle 2),c[10])),(S + x)) is Element of bool (Loops c[10])
(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 continuous Path of c[10] , c[10]
Class ((EqRel ((Tunit_circle 2),c[10])),(y)) is Element of bool (Loops c[10])
[: 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
AffineMap (1,x) is non empty Relation-like REAL -defined REAL -valued Function-like one-to-one V26( REAL ) quasi_total onto bijective V203() V204() V205() Element of bool [:REAL,REAL:]
(y) 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 y
R^1 y is V11() ext-real real Element of the carrier of R^1
F is non empty Relation-like the carrier of R^1 -defined the carrier of R^1 -valued Function-like V26( the carrier of R^1) quasi_total V203() V204() V205() Element of bool [: the carrier of R^1, the carrier of R^1:]
F * (y) 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:]
(F * (y)) . 0 is V11() ext-real real Element of REAL
j0 is V11() ext-real real Element of the carrier of I[01]
(y) . j0 is V11() ext-real real Element of the carrier of R^1
F . ((y) . j0) is V11() ext-real real Element of the carrier of R^1
y * j0 is V11() ext-real real set
F . (y * j0) is V11() ext-real real Element of REAL
1 * 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
(1 * 0) + x is V11() ext-real real integer Element of REAL
R^1 x is V11() ext-real real Element of the carrier of R^1
(F * (y)) . 1 is V11() ext-real real Element of REAL
j1 is V11() ext-real real Element of the carrier of I[01]
(y) . j1 is V11() ext-real real Element of the carrier of R^1
F . ((y) . j1) is V11() ext-real real Element of the carrier of R^1
y * j1 is V11() ext-real real set
F . (y * j1) is V11() ext-real real Element of REAL
1 * y is V11() ext-real real integer Element of REAL
(1 * y) + x is V11() ext-real real integer Element of REAL
x + y is V11() ext-real real integer set
R^1 (x + y) is V11() ext-real real Element of the carrier of R^1
(x) 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 x
yt 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 x, R^1 (x + y)
(x) + yt 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 (x + y)
CircleMap * ((x) + yt) 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 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 continuous Path of c[10] , c[10]
(x) + (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 continuous Path of c[10] , c[10]
Pt is V11() ext-real real Element of the carrier of I[01]
(CircleMap * ((x) + yt)) . Pt is Element of the carrier of (Tunit_circle 2)
((x) + (y)) . Pt is Element of the carrier of (Tunit_circle 2)
2 * Pt is V11() ext-real real Element of REAL
((x) + yt) . Pt is V11() ext-real real Element of the carrier of R^1
CircleMap . (((x) + yt) . Pt) is Element of the carrier of (Tunit_circle 2)
(x) . (2 * Pt) is V11() ext-real real Element of REAL
CircleMap . ((x) . (2 * Pt)) is set
x * (2 * Pt) is V11() ext-real real Element of REAL
CircleMap . (x * (2 * Pt)) is set
(2 * PI) * (x * (2 * Pt)) is V11() ext-real real Element of REAL
cos ((2 * PI) * (x * (2 * Pt))) is V11() ext-real real Element of REAL
sin ((2 * PI) * (x * (2 * Pt))) is V11() ext-real real Element of REAL
|[(cos ((2 * PI) * (x * (2 * Pt)))),(sin ((2 * PI) * (x * (2 * Pt))))]| 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) * x is V11() ext-real real Element of REAL
((2 * PI) * x) * (2 * Pt) is V11() ext-real real Element of REAL
cos (((2 * PI) * x) * (2 * Pt)) is V11() ext-real real Element of REAL
sin (((2 * PI) * x) * (2 * Pt)) is V11() ext-real real Element of REAL
|[(cos (((2 * PI) * x) * (2 * Pt))),(sin (((2 * PI) * x) * (2 * Pt)))]| 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)
(x) . (2 * Pt) is set
2 * Pt is V11() ext-real real Element of REAL
(2 * Pt) - 1 is V11() ext-real real Element of REAL
((x) + yt) . Pt is V11() ext-real real Element of the carrier of R^1
CircleMap . (((x) + yt) . Pt) is Element of the carrier of (Tunit_circle 2)
yt . ((2 * Pt) - 1) is V11() ext-real real Element of REAL
CircleMap . (yt . ((2 * Pt) - 1)) is set
(y) . ((2 * Pt) - 1) is V11() ext-real real Element of REAL
F . ((y) . ((2 * Pt) - 1)) is V11() ext-real real Element of REAL
CircleMap . (F . ((y) . ((2 * Pt) - 1))) is set
y * ((2 * Pt) - 1) is V11() ext-real real Element of REAL
F . (y * ((2 * Pt) - 1)) is V11() ext-real real Element of REAL
CircleMap . (F . (y * ((2 * Pt) - 1))) is set
1 * (y * ((2 * Pt) - 1)) is V11() ext-real real Element of REAL
(1 * (y * ((2 * Pt) - 1))) + x is V11() ext-real real Element of REAL
CircleMap . ((1 * (y * ((2 * Pt) - 1))) + x) is set
(y * ((2 * Pt) - 1)) + x is V11() ext-real real Element of REAL
(2 * PI) * ((y * ((2 * Pt) - 1)) + x) is V11() ext-real real Element of REAL
cos ((2 * PI) * ((y * ((2 * Pt) - 1)) + x)) is V11() ext-real real Element of REAL
sin ((2 * PI) * ((y * ((2 * Pt) - 1)) + x)) is V11() ext-real real Element of REAL
|[(cos ((2 * PI) * ((y * ((2 * Pt) - 1)) + x))),(sin ((2 * PI) * ((y * ((2 * Pt) - 1)) + 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) * (y * ((2 * Pt) - 1)) is V11() ext-real real Element of REAL
cos ((2 * PI) * (y * ((2 * Pt) - 1))) is V11() ext-real real Element of REAL
(2 * PI) * x is V11() ext-real real Element of REAL
((2 * PI) * (y * ((2 * Pt) - 1))) + ((2 * PI) * x) is V11() ext-real real Element of REAL
sin (((2 * PI) * (y * ((2 * Pt) - 1))) + ((2 * PI) * x)) is V11() ext-real real Element of REAL
|[(cos ((2 * PI) * (y * ((2 * Pt) - 1)))),(sin (((2 * PI) * (y * ((2 * Pt) - 1))) + ((2 * PI) * 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) * y is V11() ext-real real Element of REAL
((2 * PI) * y) * ((2 * Pt) - 1) is V11() ext-real real Element of REAL
cos (((2 * PI) * y) * ((2 * Pt) - 1)) is V11() ext-real real Element of REAL
sin (((2 * PI) * y) * ((2 * Pt) - 1)) is V11() ext-real real Element of REAL
|[(cos (((2 * PI) * y) * ((2 * Pt) - 1))),(sin (((2 * PI) * y) * ((2 * Pt) - 1)))]| 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)
(y) . ((2 * Pt) - 1) is set
Class ((EqRel ((Tunit_circle 2),c[10])),(x)) is Element of bool (Loops c[10])
Class ((EqRel ((Tunit_circle 2),c[10])),(CircleMap * ((x) + yt))) is Element of bool (Loops c[10])
Class ((EqRel ((Tunit_circle 2),c[10])),((x) + (y))) is Element of bool (Loops c[10])
x is set
dom () is set
y is set
() . x is set
() . y is set
dom () is V213() V214() V215() V216() V217() Element of bool the carrier of INT.Group
bool the carrier of INT.Group is non empty set
S is V11() ext-real real integer set
() . S is 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 continuous Path of c[10] , c[10]
Class ((EqRel ((Tunit_circle 2),c[10])),(S)) is Element of bool (Loops c[10])
bool (Loops c[10]) is non empty set
x is V11() ext-real real integer set
() . x is set
(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 continuous Path of c[10] , c[10]
Class ((EqRel ((Tunit_circle 2),c[10])),(x)) is Element of bool (Loops c[10])
[: the carrier of [:I[01],I[01]:], the carrier of (Tunit_circle 2):] is non empty set
bool [: the carrier of [:I[01],I[01]:], the carrier of (Tunit_circle 2):] is non empty set
F is non empty Relation-like the carrier of [:I[01],I[01]:] -defined the carrier of (Tunit_circle 2) -valued Function-like V26( the carrier of [:I[01],I[01]:]) quasi_total Element of bool [: the carrier of [:I[01],I[01]:], the carrier of (Tunit_circle 2):]
ftm 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:]
ftm . 0 is V11() ext-real real Element of REAL
CircleMap * ftm 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):]
yt is V11() ext-real real Element of the carrier of R^1
Pt 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,yt
Qt 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,yt
Ft is non empty Relation-like the carrier of [:I[01],I[01]:] -defined the carrier of R^1 -valued Function-like V26( the carrier of [:I[01],I[01]:]) quasi_total continuous V203() V204() V205() Homotopy of Pt,Qt
CircleMap * Ft is non empty Relation-like the carrier of [:I[01],I[01]:] -defined the carrier of [:I[01],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],I[01]:]) V26( the carrier of [:I[01],I[01]:]) quasi_total quasi_total continuous Element of bool [: the carrier of [:I[01],I[01]:], the carrier of (Tunit_circle 2):]
(x) 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 x
R^1 x is V11() ext-real real Element of the carrier of R^1
CircleMap * (x) 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):]
j0 is V11() ext-real real Element of the carrier of I[01]
(I[01],I[01],R^1,Ft,j0) 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:]
CircleMap * (I[01],I[01],R^1,Ft,j0) 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):]
ft1 is V11() ext-real real Element of the carrier of I[01]
(CircleMap * (I[01],I[01],R^1,Ft,j0)) . ft1 is Element of the carrier of (Tunit_circle 2)
(I[01],I[01],R^1,Ft,j0) . ft1 is V11() ext-real real Element of the carrier of R^1
CircleMap . ((I[01],I[01],R^1,Ft,j0) . ft1) is Element of the carrier of (Tunit_circle 2)
Ft . (ft1,j0) is set
[ft1,j0] is set
{ft1,j0} is non empty V213() V214() V215() set
{ft1} is non empty V213() V214() V215() set
{{ft1,j0},{ft1}} is non empty set
Ft . [ft1,j0] is V11() ext-real real set
CircleMap . (Ft . (ft1,j0)) is set
F . (ft1,j0) is set
F . [ft1,j0] is set
(S) . ft1 is Element of the carrier of (Tunit_circle 2)
(I[01],I[01],R^1,Ft,j0) . 0 is V11() ext-real real Element of REAL
Ft . (j0,j0) is set
[j0,j0] is set
{j0,j0} is non empty V213() V214() V215() set
{j0} is non empty V213() V214() V215() set
{{j0,j0},{j0}} is non empty set
Ft . [j0,j0] is V11() ext-real real set
j1 is V11() ext-real real Element of the carrier of I[01]
(I[01],I[01],R^1,Ft,j1) 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:]
CircleMap * (I[01],I[01],R^1,Ft,j1) 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):]
ftn is V11() ext-real real Element of the carrier of I[01]
(CircleMap * (I[01],I[01],R^1,Ft,j1)) . ftn is Element of the carrier of (Tunit_circle 2)
(I[01],I[01],R^1,Ft,j1) . ftn is V11() ext-real real Element of the carrier of R^1
CircleMap . ((I[01],I[01],R^1,Ft,j1) . ftn) is Element of the carrier of (Tunit_circle 2)
Ft . (ftn,j1) is set
[ftn,j1] is set
{ftn,j1} is non empty V213() V214() V215() set
{ftn} is non empty V213() V214() V215() set
{{ftn,j1},{ftn}} is non empty set
Ft . [ftn,j1] is V11() ext-real real set
CircleMap . (Ft . (ftn,j1)) is set
F . (ftn,j1) is set
F . [ftn,j1] is set
(x) . ftn is Element of the carrier of (Tunit_circle 2)
ftn 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:]
ftn . 0 is V11() ext-real real Element of REAL
CircleMap * ftn 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):]
(I[01],I[01],R^1,Ft,j1) . 0 is V11() ext-real real Element of REAL
Ft . (j0,j1) is set
[j0,j1] is set
{j0,j1} is non empty V213() V214() V215() set
{{j0,j1},{j0}} is non empty set
Ft . [j0,j1] is V11() ext-real real set
(x) . 0 is V11() ext-real real Element of REAL
x * j0 is V11() ext-real real set
(I[01],I[01],R^1,Ft,j1) . j1 is V11() ext-real real Element of the carrier of R^1
x * 1 is V11() ext-real real integer Element of REAL
(S) . 0 is V11() ext-real real Element of REAL
S * j0 is V11() ext-real real set
(I[01],I[01],R^1,Ft,j0) . j1 is V11() ext-real real Element of the carrier of R^1
S * 1 is V11() ext-real real integer Element of REAL
Ft . (j1,j0) is set
[j1,j0] is set
{j1,j0} is non empty V213() V214() V215() set
{j1} is non empty V213() V214() V215() set
{{j1,j0},{j1}} is non empty set
Ft . [j1,j0] is V11() ext-real real set
Ft . (j1,j1) is set
[j1,j1] is set
{j1,j1} is non empty V213() V214() V215() set
{{j1,j1},{j1}} is non empty set
Ft . [j1,j1] is V11() ext-real real set
rng () is Element of bool the carrier of (FundamentalGroup ((Tunit_circle 2),c[10]))
bool the carrier of (FundamentalGroup ((Tunit_circle 2),c[10])) is non empty set
S is set
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 continuous Path of c[10] , c[10]
Class ((EqRel ((Tunit_circle 2),c[10])),x) is Element of bool (Loops c[10])
bool (Loops c[10]) is non empty set
y 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:]
y . 0 is V11() ext-real real Element of REAL
CircleMap * 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):]
j1 is V11() ext-real real Element of the carrier of I[01]
y . j1 is V11() ext-real real Element of the carrier of R^1
CircleMap . (y . j1) is Element of the carrier of (Tunit_circle 2)
(CircleMap * y) . j1 is Element of the carrier of (Tunit_circle 2)
y . 1 is V11() ext-real real Element of REAL
CircleMap . (y . 1) is set
R^1 (y . 1) is V11() ext-real real Element of the carrier of R^1
dom () is V213() V214() V215() V216() V217() Element of bool the carrier of INT.Group
bool the carrier of INT.Group is non empty set
() . (y . 1) is set
Class ((EqRel ((Tunit_circle 2),c[10])),(CircleMap * y)) is Element of bool (Loops c[10])
S is non empty V11() ext-real positive non negative real set
x 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)
Tcircle (x,S) is non empty strict TopSpace-like connected compact pathwise_connected being_simple_closed_curve SubSpace of TOP-REAL 2
the carrier of (Tcircle (x,S)) is non empty set
y is Element of the carrier of (Tcircle (x,S))
FundamentalGroup ((Tcircle (x,S)),y) is non empty strict V184() V185() V186() V235() V236() V237() V238() V239() V240() multMagma
the carrier of (FundamentalGroup ((Tcircle (x,S)),y)) is non empty set
[: the carrier of (FundamentalGroup ((Tunit_circle 2),c[10])), the carrier of (FundamentalGroup ((Tcircle (x,S)),y)):] is non empty set
bool [: the carrier of (FundamentalGroup ((Tunit_circle 2),c[10])), the carrier of (FundamentalGroup ((Tcircle (x,S)),y)):] is non empty set
S is non empty Relation-like the carrier of (FundamentalGroup ((Tunit_circle 2),c[10])) -defined the carrier of (FundamentalGroup ((Tcircle (x,S)),y)) -valued Function-like V26( the carrier of (FundamentalGroup ((Tunit_circle 2),c[10]))) quasi_total V189( FundamentalGroup ((Tunit_circle 2),c[10]), FundamentalGroup ((Tcircle (x,S)),y)) multiplicative Element of bool [: the carrier of (FundamentalGroup ((Tunit_circle 2),c[10])), the carrier of (FundamentalGroup ((Tcircle (x,S)),y)):]
S * () is non empty Relation-like the carrier of INT.Group -defined the carrier of INT.Group -defined the carrier of (FundamentalGroup ((Tcircle (x,S)),y)) -valued the carrier of (FundamentalGroup ((Tcircle (x,S)),y)) -valued Function-like V26( the carrier of INT.Group) V26( the carrier of INT.Group) quasi_total quasi_total V189( INT.Group , FundamentalGroup ((Tcircle (x,S)),y)) multiplicative Element of bool [: the carrier of INT.Group, the carrier of (FundamentalGroup ((Tcircle (x,S)),y)):]
[: the carrier of INT.Group, the carrier of (FundamentalGroup ((Tcircle (x,S)),y)):] is non empty set
bool [: the carrier of INT.Group, the carrier of (FundamentalGroup ((Tcircle (x,S)),y)):] is non empty set
the non empty V11() ext-real positive non negative real set is non empty V11() ext-real positive non negative real set
the Relation-like NAT -defined Function-like finite V44(2) FinSequence-like FinSubsequence-like V203() V204() V205() Element of the carrier 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)
Tcircle ( the 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 non empty V11() ext-real positive non negative real set ) is non empty strict TopSpace-like connected compact pathwise_connected being_simple_closed_curve SubSpace of TOP-REAL 2
the carrier of (Tcircle ( the 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 non empty V11() ext-real positive non negative real set )) is non empty set
the Element of the carrier of (Tcircle ( the 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 non empty V11() ext-real positive non negative real set )) is Element of the carrier of (Tcircle ( the 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 non empty V11() ext-real positive non negative real set ))
S is non empty TopSpace-like connected compact pathwise_connected being_simple_closed_curve SubSpace of TOP-REAL 2
the carrier of S is non empty set
x is Element of the carrier of S
FundamentalGroup (S,x) is non empty strict V184() V185() V186() V235() V236() V237() V238() V239() V240() multMagma
FundamentalGroup ((Tcircle ( the 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 non empty V11() ext-real positive non negative real set )), the Element of the carrier of (Tcircle ( the 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 non empty V11() ext-real positive non negative real set ))) is non empty strict V184() V185() V186() V235() V236() V237() V238() V239() V240() multMagma
S is non empty TopSpace-like connected compact pathwise_connected being_simple_closed_curve SubSpace of TOP-REAL 2
the carrier of S is non empty set
x is Element of the carrier of S
FundamentalGroup (S,x) is non empty strict V184() V185() V186() V235() V236() V237() V238() V239() V240() multMagma