begin
begin
begin
begin
theorem
for
r being ( (
real ) (
complex real ext-real )
number )
for
i,
j being ( (
integer ) (
complex real ext-real integer )
Integer) holds
CircleMap : ( (
Function-like quasi_total ) ( non
empty V16()
V19( the
carrier of
R^1 : ( (
V303() ) ( non
empty strict TopSpace-like V299()
V303() )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V299() )
TopStruct ) ) : ( ( ) ( non
empty V67()
V68()
V69() )
set ) )
V20( the
carrier of
(Tunit_circle 2 : ( ( ) ( non empty ordinal natural complex real ext-real positive non negative integer V66() V67() V68() V69() V70() V71() V72() ) Element of NAT : ( ( ) ( V67() V68() V69() V70() V71() V72() V73() non with_non-empty_elements ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( non
empty TopSpace-like compact V221()
V222()
V266()
pathwise_connected being_simple_closed_curve )
SubSpace of
TOP-REAL 2 : ( ( ) ( non
empty ordinal natural complex real ext-real positive non
negative integer V66()
V67()
V68()
V69()
V70()
V71()
V72() )
Element of
NAT : ( ( ) (
V67()
V68()
V69()
V70()
V71()
V72()
V73() non
with_non-empty_elements )
Element of
K6(
REAL : ( ( ) ( non
empty V27()
V67()
V68()
V69()
V73() non
with_non-empty_elements )
set ) ) : ( ( ) ( non
empty )
set ) ) ) : ( (
V254() ) ( non
empty TopSpace-like T_0 T_1 T_2 V136()
V161()
V162()
V163()
V164()
V165()
V166()
V167()
V221()
V222()
V254() )
L19()) ) : ( ( ) ( non
empty )
set ) )
Function-like total quasi_total )
Function of ( ( ) ( non
empty V67()
V68()
V69() )
set ) , ( ( ) ( non
empty )
set ) )
. r : ( (
real ) (
complex real ext-real )
number ) : ( ( ) ( )
set )
= |[((cos : ( ( Function-like quasi_total ) ( non empty V16() V19( REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) V20( REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) Function-like total quasi_total continuous V51() V52() V53() ) Element of K6(K7(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ,REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty V51() V52() V53() ) set ) ) : ( ( ) ( non empty ) set ) ) * (AffineMap ((2 : ( ( ) ( non empty ordinal natural complex real ext-real positive non negative integer V66() V67() V68() V69() V70() V71() V72() ) Element of NAT : ( ( ) ( V67() V68() V69() V70() V71() V72() V73() non with_non-empty_elements ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) * PI : ( ( ) ( non empty complex real ext-real positive non negative ) Element of REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) ) : ( ( ) ( non empty complex real ext-real positive non negative ) Element of REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) ,((2 : ( ( ) ( non empty ordinal natural complex real ext-real positive non negative integer V66() V67() V68() V69() V70() V71() V72() ) Element of NAT : ( ( ) ( V67() V68() V69() V70() V71() V72() V73() non with_non-empty_elements ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) * PI : ( ( ) ( non empty complex real ext-real positive non negative ) Element of REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) ) : ( ( ) ( non empty complex real ext-real positive non negative ) Element of REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) * i : ( ( integer ) ( complex real ext-real integer ) Integer) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) )) : ( ( Function-like quasi_total ) ( non empty V16() V19( REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) V20( REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) Function-like one-to-one total quasi_total onto bijective continuous V51() V52() V53() ) Element of K6(K7(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ,REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty V51() V52() V53() ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( Function-like ) ( non empty V16() V19( REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) V20( REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) Function-like total quasi_total continuous V51() V52() V53() ) Element of K6(K7(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ,REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty V51() V52() V53() ) set ) ) : ( ( ) ( non empty ) set ) ) . r : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) ,((sin : ( ( Function-like quasi_total ) ( non empty V16() V19( REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) V20( REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) Function-like total quasi_total continuous V51() V52() V53() ) Element of K6(K7(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ,REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty V51() V52() V53() ) set ) ) : ( ( ) ( non empty ) set ) ) * (AffineMap ((2 : ( ( ) ( non empty ordinal natural complex real ext-real positive non negative integer V66() V67() V68() V69() V70() V71() V72() ) Element of NAT : ( ( ) ( V67() V68() V69() V70() V71() V72() V73() non with_non-empty_elements ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) * PI : ( ( ) ( non empty complex real ext-real positive non negative ) Element of REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) ) : ( ( ) ( non empty complex real ext-real positive non negative ) Element of REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) ,((2 : ( ( ) ( non empty ordinal natural complex real ext-real positive non negative integer V66() V67() V68() V69() V70() V71() V72() ) Element of NAT : ( ( ) ( V67() V68() V69() V70() V71() V72() V73() non with_non-empty_elements ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) * PI : ( ( ) ( non empty complex real ext-real positive non negative ) Element of REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) ) : ( ( ) ( non empty complex real ext-real positive non negative ) Element of REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) * j : ( ( integer ) ( complex real ext-real integer ) Integer) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) )) : ( ( Function-like quasi_total ) ( non empty V16() V19( REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) V20( REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) Function-like one-to-one total quasi_total onto bijective continuous V51() V52() V53() ) Element of K6(K7(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ,REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty V51() V52() V53() ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( Function-like ) ( non empty V16() V19( REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) V20( REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) Function-like total quasi_total continuous V51() V52() V53() ) Element of K6(K7(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ,REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty V51() V52() V53() ) set ) ) : ( ( ) ( non empty ) set ) ) . r : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) ]| : ( ( ) (
V16()
Function-like V34(2 : ( ( ) ( non
empty ordinal natural complex real ext-real positive non
negative integer V66()
V67()
V68()
V69()
V70()
V71()
V72() )
Element of
NAT : ( ( ) (
V67()
V68()
V69()
V70()
V71()
V72()
V73() non
with_non-empty_elements )
Element of
K6(
REAL : ( ( ) ( non
empty V27()
V67()
V68()
V69()
V73() non
with_non-empty_elements )
set ) ) : ( ( ) ( non
empty )
set ) ) ) )
V51()
V52()
V53()
FinSequence-like )
Element of the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty ordinal natural complex real ext-real positive non negative integer V66() V67() V68() V69() V70() V71() V72() ) Element of NAT : ( ( ) ( V67() V68() V69() V70() V71() V72() V73() non with_non-empty_elements ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( (
V254() ) ( non
empty TopSpace-like T_0 T_1 T_2 V136()
V161()
V162()
V163()
V164()
V165()
V166()
V167()
V221()
V222()
V254() )
L19()) : ( ( ) ( non
empty functional )
set ) ) ;
theorem
for
i being ( (
integer ) (
complex real ext-real integer )
Integer)
for
a being ( (
real ) (
complex real ext-real )
number ) holds
CircleMap (R^1 (a : ( ( real ) ( complex real ext-real ) number ) + i : ( ( integer ) ( complex real ext-real integer ) Integer) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) (
complex real ext-real )
Point of ( ( ) ( non
empty V67()
V68()
V69() )
set ) ) : ( (
Function-like quasi_total ) ( non
empty V16()
V19( the
carrier of
(R^1 : ( ( V303() ) ( non empty strict TopSpace-like V299() V303() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V299() ) TopStruct ) ) | (R^1 ].(R^1 (b2 : ( ( real ) ( complex real ext-real ) number ) + b1 : ( ( integer ) ( complex real ext-real integer ) Integer) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) Point of ( ( ) ( non empty V67() V68() V69() ) set ) ) ,((R^1 (b2 : ( ( real ) ( complex real ext-real ) number ) + b1 : ( ( integer ) ( complex real ext-real integer ) Integer) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) Point of ( ( ) ( non empty V67() V68() V69() ) set ) ) + 1 : ( ( ) ( non empty ordinal natural complex real ext-real positive non negative integer V66() V67() V68() V69() V70() V71() V72() ) Element of NAT : ( ( ) ( V67() V68() V69() V70() V71() V72() V73() non with_non-empty_elements ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) .[ : ( ( ) ( non empty open V67() V68() V69() ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V67() V68() V69() open ) Subset of ) ) : ( (
strict ) ( non
empty strict TopSpace-like open V299() )
SubSpace of
R^1 : ( (
V303() ) ( non
empty strict TopSpace-like V299()
V303() )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V299() )
TopStruct ) ) ) : ( ( ) ( non
empty V67()
V68()
V69() )
set ) )
V20( the
carrier of
(Topen_unit_circle (CircleMap : ( ( Function-like quasi_total ) ( non empty V16() V19( the carrier of R^1 : ( ( V303() ) ( non empty strict TopSpace-like V299() V303() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V299() ) TopStruct ) ) : ( ( ) ( non empty V67() V68() V69() ) set ) ) V20( the carrier of (Tunit_circle 2 : ( ( ) ( non empty ordinal natural complex real ext-real positive non negative integer V66() V67() V68() V69() V70() V71() V72() ) Element of NAT : ( ( ) ( V67() V68() V69() V70() V71() V72() V73() non with_non-empty_elements ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( non empty TopSpace-like compact V221() V222() V266() pathwise_connected being_simple_closed_curve ) SubSpace of TOP-REAL 2 : ( ( ) ( non empty ordinal natural complex real ext-real positive non negative integer V66() V67() V68() V69() V70() V71() V72() ) Element of NAT : ( ( ) ( V67() V68() V69() V70() V71() V72() V73() non with_non-empty_elements ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( V254() ) ( non empty TopSpace-like T_0 T_1 T_2 V136() V161() V162() V163() V164() V165() V166() V167() V221() V222() V254() ) L19()) ) : ( ( ) ( non empty ) set ) ) Function-like total quasi_total onto continuous ) Function of ( ( ) ( non empty V67() V68() V69() ) set ) , ( ( ) ( non empty ) set ) ) . (R^1 (b2 : ( ( real ) ( complex real ext-real ) number ) + b1 : ( ( integer ) ( complex real ext-real integer ) Integer) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) Point of ( ( ) ( non empty V67() V68() V69() ) set ) ) ) : ( ( ) ( V16() Function-like FinSequence-like ) Element of the carrier of (Tunit_circle 2 : ( ( ) ( non empty ordinal natural complex real ext-real positive non negative integer V66() V67() V68() V69() V70() V71() V72() ) Element of NAT : ( ( ) ( V67() V68() V69() V70() V71() V72() V73() non with_non-empty_elements ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( non empty TopSpace-like compact V221() V222() V266() pathwise_connected being_simple_closed_curve ) SubSpace of TOP-REAL 2 : ( ( ) ( non empty ordinal natural complex real ext-real positive non negative integer V66() V67() V68() V69() V70() V71() V72() ) Element of NAT : ( ( ) ( V67() V68() V69() V70() V71() V72() V73() non with_non-empty_elements ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( V254() ) ( non empty TopSpace-like T_0 T_1 T_2 V136() V161() V162() V163() V164() V165() V166() V167() V221() V222() V254() ) L19()) ) : ( ( ) ( non empty ) set ) ) ) : ( (
strict ) ( non
empty strict TopSpace-like open V221()
V222() )
SubSpace of
Tunit_circle 2 : ( ( ) ( non
empty ordinal natural complex real ext-real positive non
negative integer V66()
V67()
V68()
V69()
V70()
V71()
V72() )
Element of
NAT : ( ( ) (
V67()
V68()
V69()
V70()
V71()
V72()
V73() non
with_non-empty_elements )
Element of
K6(
REAL : ( ( ) ( non
empty V27()
V67()
V68()
V69()
V73() non
with_non-empty_elements )
set ) ) : ( ( ) ( non
empty )
set ) ) ) : ( ( ) ( non
empty TopSpace-like compact V221()
V222()
V266()
pathwise_connected being_simple_closed_curve )
SubSpace of
TOP-REAL 2 : ( ( ) ( non
empty ordinal natural complex real ext-real positive non
negative integer V66()
V67()
V68()
V69()
V70()
V71()
V72() )
Element of
NAT : ( ( ) (
V67()
V68()
V69()
V70()
V71()
V72()
V73() non
with_non-empty_elements )
Element of
K6(
REAL : ( ( ) ( non
empty V27()
V67()
V68()
V69()
V73() non
with_non-empty_elements )
set ) ) : ( ( ) ( non
empty )
set ) ) ) : ( (
V254() ) ( non
empty TopSpace-like T_0 T_1 T_2 V136()
V161()
V162()
V163()
V164()
V165()
V166()
V167()
V221()
V222()
V254() )
L19()) ) ) : ( ( ) ( non
empty )
set ) )
Function-like total quasi_total )
Function of ( ( ) ( non
empty V67()
V68()
V69() )
set ) , ( ( ) ( non
empty )
set ) )
= (CircleMap (R^1 a : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) Point of ( ( ) ( non empty V67() V68() V69() ) set ) ) ) : ( (
Function-like quasi_total ) ( non
empty V16()
V19( the
carrier of
(R^1 : ( ( V303() ) ( non empty strict TopSpace-like V299() V303() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V299() ) TopStruct ) ) | (R^1 ].(R^1 b2 : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) Point of ( ( ) ( non empty V67() V68() V69() ) set ) ) ,((R^1 b2 : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) Point of ( ( ) ( non empty V67() V68() V69() ) set ) ) + 1 : ( ( ) ( non empty ordinal natural complex real ext-real positive non negative integer V66() V67() V68() V69() V70() V71() V72() ) Element of NAT : ( ( ) ( V67() V68() V69() V70() V71() V72() V73() non with_non-empty_elements ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) .[ : ( ( ) ( non empty open V67() V68() V69() ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V67() V68() V69() open ) Subset of ) ) : ( (
strict ) ( non
empty strict TopSpace-like open V299() )
SubSpace of
R^1 : ( (
V303() ) ( non
empty strict TopSpace-like V299()
V303() )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V299() )
TopStruct ) ) ) : ( ( ) ( non
empty V67()
V68()
V69() )
set ) )
V20( the
carrier of
(Topen_unit_circle (CircleMap : ( ( Function-like quasi_total ) ( non empty V16() V19( the carrier of R^1 : ( ( V303() ) ( non empty strict TopSpace-like V299() V303() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V299() ) TopStruct ) ) : ( ( ) ( non empty V67() V68() V69() ) set ) ) V20( the carrier of (Tunit_circle 2 : ( ( ) ( non empty ordinal natural complex real ext-real positive non negative integer V66() V67() V68() V69() V70() V71() V72() ) Element of NAT : ( ( ) ( V67() V68() V69() V70() V71() V72() V73() non with_non-empty_elements ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( non empty TopSpace-like compact V221() V222() V266() pathwise_connected being_simple_closed_curve ) SubSpace of TOP-REAL 2 : ( ( ) ( non empty ordinal natural complex real ext-real positive non negative integer V66() V67() V68() V69() V70() V71() V72() ) Element of NAT : ( ( ) ( V67() V68() V69() V70() V71() V72() V73() non with_non-empty_elements ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( V254() ) ( non empty TopSpace-like T_0 T_1 T_2 V136() V161() V162() V163() V164() V165() V166() V167() V221() V222() V254() ) L19()) ) : ( ( ) ( non empty ) set ) ) Function-like total quasi_total onto continuous ) Function of ( ( ) ( non empty V67() V68() V69() ) set ) , ( ( ) ( non empty ) set ) ) . (R^1 b2 : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) Point of ( ( ) ( non empty V67() V68() V69() ) set ) ) ) : ( ( ) ( V16() Function-like FinSequence-like ) Element of the carrier of (Tunit_circle 2 : ( ( ) ( non empty ordinal natural complex real ext-real positive non negative integer V66() V67() V68() V69() V70() V71() V72() ) Element of NAT : ( ( ) ( V67() V68() V69() V70() V71() V72() V73() non with_non-empty_elements ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( non empty TopSpace-like compact V221() V222() V266() pathwise_connected being_simple_closed_curve ) SubSpace of TOP-REAL 2 : ( ( ) ( non empty ordinal natural complex real ext-real positive non negative integer V66() V67() V68() V69() V70() V71() V72() ) Element of NAT : ( ( ) ( V67() V68() V69() V70() V71() V72() V73() non with_non-empty_elements ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( V254() ) ( non empty TopSpace-like T_0 T_1 T_2 V136() V161() V162() V163() V164() V165() V166() V167() V221() V222() V254() ) L19()) ) : ( ( ) ( non empty ) set ) ) ) : ( (
strict ) ( non
empty strict TopSpace-like open V221()
V222() )
SubSpace of
Tunit_circle 2 : ( ( ) ( non
empty ordinal natural complex real ext-real positive non
negative integer V66()
V67()
V68()
V69()
V70()
V71()
V72() )
Element of
NAT : ( ( ) (
V67()
V68()
V69()
V70()
V71()
V72()
V73() non
with_non-empty_elements )
Element of
K6(
REAL : ( ( ) ( non
empty V27()
V67()
V68()
V69()
V73() non
with_non-empty_elements )
set ) ) : ( ( ) ( non
empty )
set ) ) ) : ( ( ) ( non
empty TopSpace-like compact V221()
V222()
V266()
pathwise_connected being_simple_closed_curve )
SubSpace of
TOP-REAL 2 : ( ( ) ( non
empty ordinal natural complex real ext-real positive non
negative integer V66()
V67()
V68()
V69()
V70()
V71()
V72() )
Element of
NAT : ( ( ) (
V67()
V68()
V69()
V70()
V71()
V72()
V73() non
with_non-empty_elements )
Element of
K6(
REAL : ( ( ) ( non
empty V27()
V67()
V68()
V69()
V73() non
with_non-empty_elements )
set ) ) : ( ( ) ( non
empty )
set ) ) ) : ( (
V254() ) ( non
empty TopSpace-like T_0 T_1 T_2 V136()
V161()
V162()
V163()
V164()
V165()
V166()
V167()
V221()
V222()
V254() )
L19()) ) ) : ( ( ) ( non
empty )
set ) )
Function-like total quasi_total )
Function of ( ( ) ( non
empty V67()
V68()
V69() )
set ) , ( ( ) ( non
empty )
set ) )
* ((AffineMap (1 : ( ( ) ( non empty ordinal natural complex real ext-real positive non negative integer V66() V67() V68() V69() V70() V71() V72() ) Element of NAT : ( ( ) ( V67() V68() V69() V70() V71() V72() V73() non with_non-empty_elements ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) ,(- i : ( ( integer ) ( complex real ext-real integer ) Integer) ) : ( ( complex ) ( complex real ext-real integer ) set ) )) : ( ( Function-like quasi_total ) ( non empty V16() V19( REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) V20( REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) Function-like one-to-one total quasi_total onto bijective continuous V51() V52() V53() ) Element of K6(K7(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ,REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty V51() V52() V53() ) set ) ) : ( ( ) ( non empty ) set ) ) | ].(a : ( ( real ) ( complex real ext-real ) number ) + i : ( ( integer ) ( complex real ext-real integer ) Integer) ) : ( ( ) ( complex real ext-real ) set ) ,((a : ( ( real ) ( complex real ext-real ) number ) + i : ( ( integer ) ( complex real ext-real integer ) Integer) ) : ( ( ) ( complex real ext-real ) set ) + 1 : ( ( ) ( non empty ordinal natural complex real ext-real positive non negative integer V66() V67() V68() V69() V70() V71() V72() ) Element of NAT : ( ( ) ( V67() V68() V69() V70() V71() V72() V73() non with_non-empty_elements ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) .[ : ( ( ) ( non empty open V67() V68() V69() ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( (
Function-like ) (
V16()
V19(
REAL : ( ( ) ( non
empty V27()
V67()
V68()
V69()
V73() non
with_non-empty_elements )
set ) )
V20(
REAL : ( ( ) ( non
empty V27()
V67()
V68()
V69()
V73() non
with_non-empty_elements )
set ) )
Function-like continuous V51()
V52()
V53() )
Element of
K6(
K7(
REAL : ( ( ) ( non
empty V27()
V67()
V68()
V69()
V73() non
with_non-empty_elements )
set ) ,
REAL : ( ( ) ( non
empty V27()
V67()
V68()
V69()
V73() non
with_non-empty_elements )
set ) ) : ( ( ) ( non
empty V51()
V52()
V53() )
set ) ) : ( ( ) ( non
empty )
set ) ) : ( (
Function-like ) (
V16()
V19(
REAL : ( ( ) ( non
empty V27()
V67()
V68()
V69()
V73() non
with_non-empty_elements )
set ) )
V20( the
carrier of
(Topen_unit_circle (CircleMap : ( ( Function-like quasi_total ) ( non empty V16() V19( the carrier of R^1 : ( ( V303() ) ( non empty strict TopSpace-like V299() V303() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V299() ) TopStruct ) ) : ( ( ) ( non empty V67() V68() V69() ) set ) ) V20( the carrier of (Tunit_circle 2 : ( ( ) ( non empty ordinal natural complex real ext-real positive non negative integer V66() V67() V68() V69() V70() V71() V72() ) Element of NAT : ( ( ) ( V67() V68() V69() V70() V71() V72() V73() non with_non-empty_elements ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( non empty TopSpace-like compact V221() V222() V266() pathwise_connected being_simple_closed_curve ) SubSpace of TOP-REAL 2 : ( ( ) ( non empty ordinal natural complex real ext-real positive non negative integer V66() V67() V68() V69() V70() V71() V72() ) Element of NAT : ( ( ) ( V67() V68() V69() V70() V71() V72() V73() non with_non-empty_elements ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( V254() ) ( non empty TopSpace-like T_0 T_1 T_2 V136() V161() V162() V163() V164() V165() V166() V167() V221() V222() V254() ) L19()) ) : ( ( ) ( non empty ) set ) ) Function-like total quasi_total onto continuous ) Function of ( ( ) ( non empty V67() V68() V69() ) set ) , ( ( ) ( non empty ) set ) ) . (R^1 b2 : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) Point of ( ( ) ( non empty V67() V68() V69() ) set ) ) ) : ( ( ) ( V16() Function-like FinSequence-like ) Element of the carrier of (Tunit_circle 2 : ( ( ) ( non empty ordinal natural complex real ext-real positive non negative integer V66() V67() V68() V69() V70() V71() V72() ) Element of NAT : ( ( ) ( V67() V68() V69() V70() V71() V72() V73() non with_non-empty_elements ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( non empty TopSpace-like compact V221() V222() V266() pathwise_connected being_simple_closed_curve ) SubSpace of TOP-REAL 2 : ( ( ) ( non empty ordinal natural complex real ext-real positive non negative integer V66() V67() V68() V69() V70() V71() V72() ) Element of NAT : ( ( ) ( V67() V68() V69() V70() V71() V72() V73() non with_non-empty_elements ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( V254() ) ( non empty TopSpace-like T_0 T_1 T_2 V136() V161() V162() V163() V164() V165() V166() V167() V221() V222() V254() ) L19()) ) : ( ( ) ( non empty ) set ) ) ) : ( (
strict ) ( non
empty strict TopSpace-like open V221()
V222() )
SubSpace of
Tunit_circle 2 : ( ( ) ( non
empty ordinal natural complex real ext-real positive non
negative integer V66()
V67()
V68()
V69()
V70()
V71()
V72() )
Element of
NAT : ( ( ) (
V67()
V68()
V69()
V70()
V71()
V72()
V73() non
with_non-empty_elements )
Element of
K6(
REAL : ( ( ) ( non
empty V27()
V67()
V68()
V69()
V73() non
with_non-empty_elements )
set ) ) : ( ( ) ( non
empty )
set ) ) ) : ( ( ) ( non
empty TopSpace-like compact V221()
V222()
V266()
pathwise_connected being_simple_closed_curve )
SubSpace of
TOP-REAL 2 : ( ( ) ( non
empty ordinal natural complex real ext-real positive non
negative integer V66()
V67()
V68()
V69()
V70()
V71()
V72() )
Element of
NAT : ( ( ) (
V67()
V68()
V69()
V70()
V71()
V72()
V73() non
with_non-empty_elements )
Element of
K6(
REAL : ( ( ) ( non
empty V27()
V67()
V68()
V69()
V73() non
with_non-empty_elements )
set ) ) : ( ( ) ( non
empty )
set ) ) ) : ( (
V254() ) ( non
empty TopSpace-like T_0 T_1 T_2 V136()
V161()
V162()
V163()
V164()
V165()
V166()
V167()
V221()
V222()
V254() )
L19()) ) ) : ( ( ) ( non
empty )
set ) )
Function-like )
Element of
K6(
K7(
REAL : ( ( ) ( non
empty V27()
V67()
V68()
V69()
V73() non
with_non-empty_elements )
set ) , the
carrier of
(Topen_unit_circle (CircleMap : ( ( Function-like quasi_total ) ( non empty V16() V19( the carrier of R^1 : ( ( V303() ) ( non empty strict TopSpace-like V299() V303() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V299() ) TopStruct ) ) : ( ( ) ( non empty V67() V68() V69() ) set ) ) V20( the carrier of (Tunit_circle 2 : ( ( ) ( non empty ordinal natural complex real ext-real positive non negative integer V66() V67() V68() V69() V70() V71() V72() ) Element of NAT : ( ( ) ( V67() V68() V69() V70() V71() V72() V73() non with_non-empty_elements ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( non empty TopSpace-like compact V221() V222() V266() pathwise_connected being_simple_closed_curve ) SubSpace of TOP-REAL 2 : ( ( ) ( non empty ordinal natural complex real ext-real positive non negative integer V66() V67() V68() V69() V70() V71() V72() ) Element of NAT : ( ( ) ( V67() V68() V69() V70() V71() V72() V73() non with_non-empty_elements ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( V254() ) ( non empty TopSpace-like T_0 T_1 T_2 V136() V161() V162() V163() V164() V165() V166() V167() V221() V222() V254() ) L19()) ) : ( ( ) ( non empty ) set ) ) Function-like total quasi_total onto continuous ) Function of ( ( ) ( non empty V67() V68() V69() ) set ) , ( ( ) ( non empty ) set ) ) . (R^1 b2 : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) Point of ( ( ) ( non empty V67() V68() V69() ) set ) ) ) : ( ( ) ( V16() Function-like FinSequence-like ) Element of the carrier of (Tunit_circle 2 : ( ( ) ( non empty ordinal natural complex real ext-real positive non negative integer V66() V67() V68() V69() V70() V71() V72() ) Element of NAT : ( ( ) ( V67() V68() V69() V70() V71() V72() V73() non with_non-empty_elements ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( non empty TopSpace-like compact V221() V222() V266() pathwise_connected being_simple_closed_curve ) SubSpace of TOP-REAL 2 : ( ( ) ( non empty ordinal natural complex real ext-real positive non negative integer V66() V67() V68() V69() V70() V71() V72() ) Element of NAT : ( ( ) ( V67() V68() V69() V70() V71() V72() V73() non with_non-empty_elements ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( V254() ) ( non empty TopSpace-like T_0 T_1 T_2 V136() V161() V162() V163() V164() V165() V166() V167() V221() V222() V254() ) L19()) ) : ( ( ) ( non empty ) set ) ) ) : ( (
strict ) ( non
empty strict TopSpace-like open V221()
V222() )
SubSpace of
Tunit_circle 2 : ( ( ) ( non
empty ordinal natural complex real ext-real positive non
negative integer V66()
V67()
V68()
V69()
V70()
V71()
V72() )
Element of
NAT : ( ( ) (
V67()
V68()
V69()
V70()
V71()
V72()
V73() non
with_non-empty_elements )
Element of
K6(
REAL : ( ( ) ( non
empty V27()
V67()
V68()
V69()
V73() non
with_non-empty_elements )
set ) ) : ( ( ) ( non
empty )
set ) ) ) : ( ( ) ( non
empty TopSpace-like compact V221()
V222()
V266()
pathwise_connected being_simple_closed_curve )
SubSpace of
TOP-REAL 2 : ( ( ) ( non
empty ordinal natural complex real ext-real positive non
negative integer V66()
V67()
V68()
V69()
V70()
V71()
V72() )
Element of
NAT : ( ( ) (
V67()
V68()
V69()
V70()
V71()
V72()
V73() non
with_non-empty_elements )
Element of
K6(
REAL : ( ( ) ( non
empty V27()
V67()
V68()
V69()
V73() non
with_non-empty_elements )
set ) ) : ( ( ) ( non
empty )
set ) ) ) : ( (
V254() ) ( non
empty TopSpace-like T_0 T_1 T_2 V136()
V161()
V162()
V163()
V164()
V165()
V166()
V167()
V221()
V222()
V254() )
L19()) ) ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) ) ;
theorem
(CircleMap (R^1 0 : ( ( ) ( empty trivial ordinal natural complex real ext-real non positive non negative Function-like functional integer V66() V67() V68() V69() V70() V71() V72() V73() ) Element of NAT : ( ( ) ( V67() V68() V69() V70() V71() V72() V73() non with_non-empty_elements ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( complex real ext-real ) Point of ( ( ) ( non empty V67() V68() V69() ) set ) ) ) : ( (
Function-like quasi_total ) ( non
empty V16()
V19( the
carrier of
(R^1 : ( ( V303() ) ( non empty strict TopSpace-like V299() V303() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V299() ) TopStruct ) ) | (R^1 ].(R^1 0 : ( ( ) ( empty trivial ordinal natural complex real ext-real non positive non negative Function-like functional integer V66() V67() V68() V69() V70() V71() V72() V73() ) Element of NAT : ( ( ) ( V67() V68() V69() V70() V71() V72() V73() non with_non-empty_elements ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( complex real ext-real ) Point of ( ( ) ( non empty V67() V68() V69() ) set ) ) ,((R^1 0 : ( ( ) ( empty trivial ordinal natural complex real ext-real non positive non negative Function-like functional integer V66() V67() V68() V69() V70() V71() V72() V73() ) Element of NAT : ( ( ) ( V67() V68() V69() V70() V71() V72() V73() non with_non-empty_elements ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( complex real ext-real ) Point of ( ( ) ( non empty V67() V68() V69() ) set ) ) + 1 : ( ( ) ( non empty ordinal natural complex real ext-real positive non negative integer V66() V67() V68() V69() V70() V71() V72() ) Element of NAT : ( ( ) ( V67() V68() V69() V70() V71() V72() V73() non with_non-empty_elements ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) .[ : ( ( ) ( non empty open V67() V68() V69() ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V67() V68() V69() open ) Subset of ) ) : ( (
strict ) ( non
empty strict TopSpace-like open V299() )
SubSpace of
R^1 : ( (
V303() ) ( non
empty strict TopSpace-like V299()
V303() )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V299() )
TopStruct ) ) ) : ( ( ) ( non
empty V67()
V68()
V69() )
set ) )
V20( the
carrier of
(Topen_unit_circle (CircleMap : ( ( Function-like quasi_total ) ( non empty V16() V19( the carrier of R^1 : ( ( V303() ) ( non empty strict TopSpace-like V299() V303() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V299() ) TopStruct ) ) : ( ( ) ( non empty V67() V68() V69() ) set ) ) V20( the carrier of (Tunit_circle 2 : ( ( ) ( non empty ordinal natural complex real ext-real positive non negative integer V66() V67() V68() V69() V70() V71() V72() ) Element of NAT : ( ( ) ( V67() V68() V69() V70() V71() V72() V73() non with_non-empty_elements ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( non empty TopSpace-like compact V221() V222() V266() pathwise_connected being_simple_closed_curve ) SubSpace of TOP-REAL 2 : ( ( ) ( non empty ordinal natural complex real ext-real positive non negative integer V66() V67() V68() V69() V70() V71() V72() ) Element of NAT : ( ( ) ( V67() V68() V69() V70() V71() V72() V73() non with_non-empty_elements ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( V254() ) ( non empty TopSpace-like T_0 T_1 T_2 V136() V161() V162() V163() V164() V165() V166() V167() V221() V222() V254() ) L19()) ) : ( ( ) ( non empty ) set ) ) Function-like total quasi_total onto continuous ) Function of ( ( ) ( non empty V67() V68() V69() ) set ) , ( ( ) ( non empty ) set ) ) . (R^1 0 : ( ( ) ( empty trivial ordinal natural complex real ext-real non positive non negative Function-like functional integer V66() V67() V68() V69() V70() V71() V72() V73() ) Element of NAT : ( ( ) ( V67() V68() V69() V70() V71() V72() V73() non with_non-empty_elements ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( complex real ext-real ) Point of ( ( ) ( non empty V67() V68() V69() ) set ) ) ) : ( ( ) ( V16() Function-like FinSequence-like ) Element of the carrier of (Tunit_circle 2 : ( ( ) ( non empty ordinal natural complex real ext-real positive non negative integer V66() V67() V68() V69() V70() V71() V72() ) Element of NAT : ( ( ) ( V67() V68() V69() V70() V71() V72() V73() non with_non-empty_elements ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( non empty TopSpace-like compact V221() V222() V266() pathwise_connected being_simple_closed_curve ) SubSpace of TOP-REAL 2 : ( ( ) ( non empty ordinal natural complex real ext-real positive non negative integer V66() V67() V68() V69() V70() V71() V72() ) Element of NAT : ( ( ) ( V67() V68() V69() V70() V71() V72() V73() non with_non-empty_elements ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( V254() ) ( non empty TopSpace-like T_0 T_1 T_2 V136() V161() V162() V163() V164() V165() V166() V167() V221() V222() V254() ) L19()) ) : ( ( ) ( non empty ) set ) ) ) : ( (
strict ) ( non
empty strict TopSpace-like open V221()
V222() )
SubSpace of
Tunit_circle 2 : ( ( ) ( non
empty ordinal natural complex real ext-real positive non
negative integer V66()
V67()
V68()
V69()
V70()
V71()
V72() )
Element of
NAT : ( ( ) (
V67()
V68()
V69()
V70()
V71()
V72()
V73() non
with_non-empty_elements )
Element of
K6(
REAL : ( ( ) ( non
empty V27()
V67()
V68()
V69()
V73() non
with_non-empty_elements )
set ) ) : ( ( ) ( non
empty )
set ) ) ) : ( ( ) ( non
empty TopSpace-like compact V221()
V222()
V266()
pathwise_connected being_simple_closed_curve )
SubSpace of
TOP-REAL 2 : ( ( ) ( non
empty ordinal natural complex real ext-real positive non
negative integer V66()
V67()
V68()
V69()
V70()
V71()
V72() )
Element of
NAT : ( ( ) (
V67()
V68()
V69()
V70()
V71()
V72()
V73() non
with_non-empty_elements )
Element of
K6(
REAL : ( ( ) ( non
empty V27()
V67()
V68()
V69()
V73() non
with_non-empty_elements )
set ) ) : ( ( ) ( non
empty )
set ) ) ) : ( (
V254() ) ( non
empty TopSpace-like T_0 T_1 T_2 V136()
V161()
V162()
V163()
V164()
V165()
V166()
V167()
V221()
V222()
V254() )
L19()) ) ) : ( ( ) ( non
empty )
set ) )
Function-like one-to-one total quasi_total onto bijective continuous )
Function of ( ( ) ( non
empty V67()
V68()
V69() )
set ) , ( ( ) ( non
empty )
set ) )
" : ( (
Function-like quasi_total ) ( non
empty V16()
V19( the
carrier of
(Topen_unit_circle (CircleMap : ( ( Function-like quasi_total ) ( non empty V16() V19( the carrier of R^1 : ( ( V303() ) ( non empty strict TopSpace-like V299() V303() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V299() ) TopStruct ) ) : ( ( ) ( non empty V67() V68() V69() ) set ) ) V20( the carrier of (Tunit_circle 2 : ( ( ) ( non empty ordinal natural complex real ext-real positive non negative integer V66() V67() V68() V69() V70() V71() V72() ) Element of NAT : ( ( ) ( V67() V68() V69() V70() V71() V72() V73() non with_non-empty_elements ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( non empty TopSpace-like compact V221() V222() V266() pathwise_connected being_simple_closed_curve ) SubSpace of TOP-REAL 2 : ( ( ) ( non empty ordinal natural complex real ext-real positive non negative integer V66() V67() V68() V69() V70() V71() V72() ) Element of NAT : ( ( ) ( V67() V68() V69() V70() V71() V72() V73() non with_non-empty_elements ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( V254() ) ( non empty TopSpace-like T_0 T_1 T_2 V136() V161() V162() V163() V164() V165() V166() V167() V221() V222() V254() ) L19()) ) : ( ( ) ( non empty ) set ) ) Function-like total quasi_total onto continuous ) Function of ( ( ) ( non empty V67() V68() V69() ) set ) , ( ( ) ( non empty ) set ) ) . (R^1 0 : ( ( ) ( empty trivial ordinal natural complex real ext-real non positive non negative Function-like functional integer V66() V67() V68() V69() V70() V71() V72() V73() ) Element of NAT : ( ( ) ( V67() V68() V69() V70() V71() V72() V73() non with_non-empty_elements ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( complex real ext-real ) Point of ( ( ) ( non empty V67() V68() V69() ) set ) ) ) : ( ( ) ( V16() Function-like FinSequence-like ) Element of the carrier of (Tunit_circle 2 : ( ( ) ( non empty ordinal natural complex real ext-real positive non negative integer V66() V67() V68() V69() V70() V71() V72() ) Element of NAT : ( ( ) ( V67() V68() V69() V70() V71() V72() V73() non with_non-empty_elements ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( non empty TopSpace-like compact V221() V222() V266() pathwise_connected being_simple_closed_curve ) SubSpace of TOP-REAL 2 : ( ( ) ( non empty ordinal natural complex real ext-real positive non negative integer V66() V67() V68() V69() V70() V71() V72() ) Element of NAT : ( ( ) ( V67() V68() V69() V70() V71() V72() V73() non with_non-empty_elements ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( V254() ) ( non empty TopSpace-like T_0 T_1 T_2 V136() V161() V162() V163() V164() V165() V166() V167() V221() V222() V254() ) L19()) ) : ( ( ) ( non empty ) set ) ) ) : ( (
strict ) ( non
empty strict TopSpace-like open V221()
V222() )
SubSpace of
Tunit_circle 2 : ( ( ) ( non
empty ordinal natural complex real ext-real positive non
negative integer V66()
V67()
V68()
V69()
V70()
V71()
V72() )
Element of
NAT : ( ( ) (
V67()
V68()
V69()
V70()
V71()
V72()
V73() non
with_non-empty_elements )
Element of
K6(
REAL : ( ( ) ( non
empty V27()
V67()
V68()
V69()
V73() non
with_non-empty_elements )
set ) ) : ( ( ) ( non
empty )
set ) ) ) : ( ( ) ( non
empty TopSpace-like compact V221()
V222()
V266()
pathwise_connected being_simple_closed_curve )
SubSpace of
TOP-REAL 2 : ( ( ) ( non
empty ordinal natural complex real ext-real positive non
negative integer V66()
V67()
V68()
V69()
V70()
V71()
V72() )
Element of
NAT : ( ( ) (
V67()
V68()
V69()
V70()
V71()
V72()
V73() non
with_non-empty_elements )
Element of
K6(
REAL : ( ( ) ( non
empty V27()
V67()
V68()
V69()
V73() non
with_non-empty_elements )
set ) ) : ( ( ) ( non
empty )
set ) ) ) : ( (
V254() ) ( non
empty TopSpace-like T_0 T_1 T_2 V136()
V161()
V162()
V163()
V164()
V165()
V166()
V167()
V221()
V222()
V254() )
L19()) ) ) : ( ( ) ( non
empty )
set ) )
V20( the
carrier of
(R^1 : ( ( V303() ) ( non empty strict TopSpace-like V299() V303() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V299() ) TopStruct ) ) | (R^1 ].(R^1 0 : ( ( ) ( empty trivial ordinal natural complex real ext-real non positive non negative Function-like functional integer V66() V67() V68() V69() V70() V71() V72() V73() ) Element of NAT : ( ( ) ( V67() V68() V69() V70() V71() V72() V73() non with_non-empty_elements ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( complex real ext-real ) Point of ( ( ) ( non empty V67() V68() V69() ) set ) ) ,((R^1 0 : ( ( ) ( empty trivial ordinal natural complex real ext-real non positive non negative Function-like functional integer V66() V67() V68() V69() V70() V71() V72() V73() ) Element of NAT : ( ( ) ( V67() V68() V69() V70() V71() V72() V73() non with_non-empty_elements ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( complex real ext-real ) Point of ( ( ) ( non empty V67() V68() V69() ) set ) ) + 1 : ( ( ) ( non empty ordinal natural complex real ext-real positive non negative integer V66() V67() V68() V69() V70() V71() V72() ) Element of NAT : ( ( ) ( V67() V68() V69() V70() V71() V72() V73() non with_non-empty_elements ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) .[ : ( ( ) ( non empty open V67() V68() V69() ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V67() V68() V69() open ) Subset of ) ) : ( (
strict ) ( non
empty strict TopSpace-like open V299() )
SubSpace of
R^1 : ( (
V303() ) ( non
empty strict TopSpace-like V299()
V303() )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V299() )
TopStruct ) ) ) : ( ( ) ( non
empty V67()
V68()
V69() )
set ) )
Function-like total quasi_total V51()
V52()
V53() )
Element of
K6(
K7( the
carrier of
(Topen_unit_circle (CircleMap : ( ( Function-like quasi_total ) ( non empty V16() V19( the carrier of R^1 : ( ( V303() ) ( non empty strict TopSpace-like V299() V303() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V299() ) TopStruct ) ) : ( ( ) ( non empty V67() V68() V69() ) set ) ) V20( the carrier of (Tunit_circle 2 : ( ( ) ( non empty ordinal natural complex real ext-real positive non negative integer V66() V67() V68() V69() V70() V71() V72() ) Element of NAT : ( ( ) ( V67() V68() V69() V70() V71() V72() V73() non with_non-empty_elements ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( non empty TopSpace-like compact V221() V222() V266() pathwise_connected being_simple_closed_curve ) SubSpace of TOP-REAL 2 : ( ( ) ( non empty ordinal natural complex real ext-real positive non negative integer V66() V67() V68() V69() V70() V71() V72() ) Element of NAT : ( ( ) ( V67() V68() V69() V70() V71() V72() V73() non with_non-empty_elements ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( V254() ) ( non empty TopSpace-like T_0 T_1 T_2 V136() V161() V162() V163() V164() V165() V166() V167() V221() V222() V254() ) L19()) ) : ( ( ) ( non empty ) set ) ) Function-like total quasi_total onto continuous ) Function of ( ( ) ( non empty V67() V68() V69() ) set ) , ( ( ) ( non empty ) set ) ) . (R^1 0 : ( ( ) ( empty trivial ordinal natural complex real ext-real non positive non negative Function-like functional integer V66() V67() V68() V69() V70() V71() V72() V73() ) Element of NAT : ( ( ) ( V67() V68() V69() V70() V71() V72() V73() non with_non-empty_elements ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( complex real ext-real ) Point of ( ( ) ( non empty V67() V68() V69() ) set ) ) ) : ( ( ) ( V16() Function-like FinSequence-like ) Element of the carrier of (Tunit_circle 2 : ( ( ) ( non empty ordinal natural complex real ext-real positive non negative integer V66() V67() V68() V69() V70() V71() V72() ) Element of NAT : ( ( ) ( V67() V68() V69() V70() V71() V72() V73() non with_non-empty_elements ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( non empty TopSpace-like compact V221() V222() V266() pathwise_connected being_simple_closed_curve ) SubSpace of TOP-REAL 2 : ( ( ) ( non empty ordinal natural complex real ext-real positive non negative integer V66() V67() V68() V69() V70() V71() V72() ) Element of NAT : ( ( ) ( V67() V68() V69() V70() V71() V72() V73() non with_non-empty_elements ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( V254() ) ( non empty TopSpace-like T_0 T_1 T_2 V136() V161() V162() V163() V164() V165() V166() V167() V221() V222() V254() ) L19()) ) : ( ( ) ( non empty ) set ) ) ) : ( (
strict ) ( non
empty strict TopSpace-like open V221()
V222() )
SubSpace of
Tunit_circle 2 : ( ( ) ( non
empty ordinal natural complex real ext-real positive non
negative integer V66()
V67()
V68()
V69()
V70()
V71()
V72() )
Element of
NAT : ( ( ) (
V67()
V68()
V69()
V70()
V71()
V72()
V73() non
with_non-empty_elements )
Element of
K6(
REAL : ( ( ) ( non
empty V27()
V67()
V68()
V69()
V73() non
with_non-empty_elements )
set ) ) : ( ( ) ( non
empty )
set ) ) ) : ( ( ) ( non
empty TopSpace-like compact V221()
V222()
V266()
pathwise_connected being_simple_closed_curve )
SubSpace of
TOP-REAL 2 : ( ( ) ( non
empty ordinal natural complex real ext-real positive non
negative integer V66()
V67()
V68()
V69()
V70()
V71()
V72() )
Element of
NAT : ( ( ) (
V67()
V68()
V69()
V70()
V71()
V72()
V73() non
with_non-empty_elements )
Element of
K6(
REAL : ( ( ) ( non
empty V27()
V67()
V68()
V69()
V73() non
with_non-empty_elements )
set ) ) : ( ( ) ( non
empty )
set ) ) ) : ( (
V254() ) ( non
empty TopSpace-like T_0 T_1 T_2 V136()
V161()
V162()
V163()
V164()
V165()
V166()
V167()
V221()
V222()
V254() )
L19()) ) ) : ( ( ) ( non
empty )
set ) , the
carrier of
(R^1 : ( ( V303() ) ( non empty strict TopSpace-like V299() V303() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V299() ) TopStruct ) ) | (R^1 ].(R^1 0 : ( ( ) ( empty trivial ordinal natural complex real ext-real non positive non negative Function-like functional integer V66() V67() V68() V69() V70() V71() V72() V73() ) Element of NAT : ( ( ) ( V67() V68() V69() V70() V71() V72() V73() non with_non-empty_elements ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( complex real ext-real ) Point of ( ( ) ( non empty V67() V68() V69() ) set ) ) ,((R^1 0 : ( ( ) ( empty trivial ordinal natural complex real ext-real non positive non negative Function-like functional integer V66() V67() V68() V69() V70() V71() V72() V73() ) Element of NAT : ( ( ) ( V67() V68() V69() V70() V71() V72() V73() non with_non-empty_elements ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( complex real ext-real ) Point of ( ( ) ( non empty V67() V68() V69() ) set ) ) + 1 : ( ( ) ( non empty ordinal natural complex real ext-real positive non negative integer V66() V67() V68() V69() V70() V71() V72() ) Element of NAT : ( ( ) ( V67() V68() V69() V70() V71() V72() V73() non with_non-empty_elements ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) .[ : ( ( ) ( non empty open V67() V68() V69() ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V67() V68() V69() open ) Subset of ) ) : ( (
strict ) ( non
empty strict TopSpace-like open V299() )
SubSpace of
R^1 : ( (
V303() ) ( non
empty strict TopSpace-like V299()
V303() )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V299() )
TopStruct ) ) ) : ( ( ) ( non
empty V67()
V68()
V69() )
set ) ) : ( ( ) ( non
empty V51()
V52()
V53() )
set ) ) : ( ( ) ( non
empty )
set ) )
= Circle2IntervalR : ( (
Function-like quasi_total ) ( non
empty V16()
V19( the
carrier of
(Topen_unit_circle c[10] : ( ( ) ( V16() Function-like FinSequence-like ) Point of ( ( ) ( non empty ) set ) ) ) : ( (
strict ) ( non
empty strict TopSpace-like open V221()
V222() )
SubSpace of
Tunit_circle 2 : ( ( ) ( non
empty ordinal natural complex real ext-real positive non
negative integer V66()
V67()
V68()
V69()
V70()
V71()
V72() )
Element of
NAT : ( ( ) (
V67()
V68()
V69()
V70()
V71()
V72()
V73() non
with_non-empty_elements )
Element of
K6(
REAL : ( ( ) ( non
empty V27()
V67()
V68()
V69()
V73() non
with_non-empty_elements )
set ) ) : ( ( ) ( non
empty )
set ) ) ) : ( ( ) ( non
empty TopSpace-like compact V221()
V222()
V266()
pathwise_connected being_simple_closed_curve )
SubSpace of
TOP-REAL 2 : ( ( ) ( non
empty ordinal natural complex real ext-real positive non
negative integer V66()
V67()
V68()
V69()
V70()
V71()
V72() )
Element of
NAT : ( ( ) (
V67()
V68()
V69()
V70()
V71()
V72()
V73() non
with_non-empty_elements )
Element of
K6(
REAL : ( ( ) ( non
empty V27()
V67()
V68()
V69()
V73() non
with_non-empty_elements )
set ) ) : ( ( ) ( non
empty )
set ) ) ) : ( (
V254() ) ( non
empty TopSpace-like T_0 T_1 T_2 V136()
V161()
V162()
V163()
V164()
V165()
V166()
V167()
V221()
V222()
V254() )
L19()) ) ) : ( ( ) ( non
empty )
set ) )
V20( the
carrier of
(R^1 : ( ( V303() ) ( non empty strict TopSpace-like V299() V303() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V299() ) TopStruct ) ) | (R^1 ].0 : ( ( ) ( empty trivial ordinal natural complex real ext-real non positive non negative Function-like functional integer V66() V67() V68() V69() V70() V71() V72() V73() ) Element of NAT : ( ( ) ( V67() V68() V69() V70() V71() V72() V73() non with_non-empty_elements ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ordinal natural complex real ext-real positive non negative integer V66() V67() V68() V69() V70() V71() V72() ) Element of NAT : ( ( ) ( V67() V68() V69() V70() V71() V72() V73() non with_non-empty_elements ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) .[ : ( ( ) ( non empty open V67() V68() V69() ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V67() V68() V69() open ) Subset of ) ) : ( (
strict ) ( non
empty strict TopSpace-like open V299() )
SubSpace of
R^1 : ( (
V303() ) ( non
empty strict TopSpace-like V299()
V303() )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V299() )
TopStruct ) ) ) : ( ( ) ( non
empty V67()
V68()
V69() )
set ) )
Function-like total quasi_total V51()
V52()
V53() )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty V67()
V68()
V69() )
set ) ) ;
theorem
(CircleMap (R^1 (1 : ( ( ) ( non empty ordinal natural complex real ext-real positive non negative integer V66() V67() V68() V69() V70() V71() V72() ) Element of NAT : ( ( ) ( V67() V68() V69() V70() V71() V72() V73() non with_non-empty_elements ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) / 2 : ( ( ) ( non empty ordinal natural complex real ext-real positive non negative integer V66() V67() V68() V69() V70() V71() V72() ) Element of NAT : ( ( ) ( V67() V68() V69() V70() V71() V72() V73() non with_non-empty_elements ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( non empty complex real ext-real positive non negative ) Element of REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) ) : ( ( ) ( complex real ext-real ) Point of ( ( ) ( non empty V67() V68() V69() ) set ) ) ) : ( (
Function-like quasi_total ) ( non
empty V16()
V19( the
carrier of
(R^1 : ( ( V303() ) ( non empty strict TopSpace-like V299() V303() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V299() ) TopStruct ) ) | (R^1 ].(R^1 (1 : ( ( ) ( non empty ordinal natural complex real ext-real positive non negative integer V66() V67() V68() V69() V70() V71() V72() ) Element of NAT : ( ( ) ( V67() V68() V69() V70() V71() V72() V73() non with_non-empty_elements ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) / 2 : ( ( ) ( non empty ordinal natural complex real ext-real positive non negative integer V66() V67() V68() V69() V70() V71() V72() ) Element of NAT : ( ( ) ( V67() V68() V69() V70() V71() V72() V73() non with_non-empty_elements ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( non empty complex real ext-real positive non negative ) Element of REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) ) : ( ( ) ( complex real ext-real ) Point of ( ( ) ( non empty V67() V68() V69() ) set ) ) ,((R^1 (1 : ( ( ) ( non empty ordinal natural complex real ext-real positive non negative integer V66() V67() V68() V69() V70() V71() V72() ) Element of NAT : ( ( ) ( V67() V68() V69() V70() V71() V72() V73() non with_non-empty_elements ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) / 2 : ( ( ) ( non empty ordinal natural complex real ext-real positive non negative integer V66() V67() V68() V69() V70() V71() V72() ) Element of NAT : ( ( ) ( V67() V68() V69() V70() V71() V72() V73() non with_non-empty_elements ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( non empty complex real ext-real positive non negative ) Element of REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) ) : ( ( ) ( complex real ext-real ) Point of ( ( ) ( non empty V67() V68() V69() ) set ) ) + 1 : ( ( ) ( non empty ordinal natural complex real ext-real positive non negative integer V66() V67() V68() V69() V70() V71() V72() ) Element of NAT : ( ( ) ( V67() V68() V69() V70() V71() V72() V73() non with_non-empty_elements ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) .[ : ( ( ) ( non empty open V67() V68() V69() ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V67() V68() V69() open ) Subset of ) ) : ( (
strict ) ( non
empty strict TopSpace-like open V299() )
SubSpace of
R^1 : ( (
V303() ) ( non
empty strict TopSpace-like V299()
V303() )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V299() )
TopStruct ) ) ) : ( ( ) ( non
empty V67()
V68()
V69() )
set ) )
V20( the
carrier of
(Topen_unit_circle (CircleMap : ( ( Function-like quasi_total ) ( non empty V16() V19( the carrier of R^1 : ( ( V303() ) ( non empty strict TopSpace-like V299() V303() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V299() ) TopStruct ) ) : ( ( ) ( non empty V67() V68() V69() ) set ) ) V20( the carrier of (Tunit_circle 2 : ( ( ) ( non empty ordinal natural complex real ext-real positive non negative integer V66() V67() V68() V69() V70() V71() V72() ) Element of NAT : ( ( ) ( V67() V68() V69() V70() V71() V72() V73() non with_non-empty_elements ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( non empty TopSpace-like compact V221() V222() V266() pathwise_connected being_simple_closed_curve ) SubSpace of TOP-REAL 2 : ( ( ) ( non empty ordinal natural complex real ext-real positive non negative integer V66() V67() V68() V69() V70() V71() V72() ) Element of NAT : ( ( ) ( V67() V68() V69() V70() V71() V72() V73() non with_non-empty_elements ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( V254() ) ( non empty TopSpace-like T_0 T_1 T_2 V136() V161() V162() V163() V164() V165() V166() V167() V221() V222() V254() ) L19()) ) : ( ( ) ( non empty ) set ) ) Function-like total quasi_total onto continuous ) Function of ( ( ) ( non empty V67() V68() V69() ) set ) , ( ( ) ( non empty ) set ) ) . (R^1 (1 : ( ( ) ( non empty ordinal natural complex real ext-real positive non negative integer V66() V67() V68() V69() V70() V71() V72() ) Element of NAT : ( ( ) ( V67() V68() V69() V70() V71() V72() V73() non with_non-empty_elements ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) / 2 : ( ( ) ( non empty ordinal natural complex real ext-real positive non negative integer V66() V67() V68() V69() V70() V71() V72() ) Element of NAT : ( ( ) ( V67() V68() V69() V70() V71() V72() V73() non with_non-empty_elements ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( non empty complex real ext-real positive non negative ) Element of REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) ) : ( ( ) ( complex real ext-real ) Point of ( ( ) ( non empty V67() V68() V69() ) set ) ) ) : ( ( ) ( V16() Function-like FinSequence-like ) Element of the carrier of (Tunit_circle 2 : ( ( ) ( non empty ordinal natural complex real ext-real positive non negative integer V66() V67() V68() V69() V70() V71() V72() ) Element of NAT : ( ( ) ( V67() V68() V69() V70() V71() V72() V73() non with_non-empty_elements ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( non empty TopSpace-like compact V221() V222() V266() pathwise_connected being_simple_closed_curve ) SubSpace of TOP-REAL 2 : ( ( ) ( non empty ordinal natural complex real ext-real positive non negative integer V66() V67() V68() V69() V70() V71() V72() ) Element of NAT : ( ( ) ( V67() V68() V69() V70() V71() V72() V73() non with_non-empty_elements ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( V254() ) ( non empty TopSpace-like T_0 T_1 T_2 V136() V161() V162() V163() V164() V165() V166() V167() V221() V222() V254() ) L19()) ) : ( ( ) ( non empty ) set ) ) ) : ( (
strict ) ( non
empty strict TopSpace-like open V221()
V222() )
SubSpace of
Tunit_circle 2 : ( ( ) ( non
empty ordinal natural complex real ext-real positive non
negative integer V66()
V67()
V68()
V69()
V70()
V71()
V72() )
Element of
NAT : ( ( ) (
V67()
V68()
V69()
V70()
V71()
V72()
V73() non
with_non-empty_elements )
Element of
K6(
REAL : ( ( ) ( non
empty V27()
V67()
V68()
V69()
V73() non
with_non-empty_elements )
set ) ) : ( ( ) ( non
empty )
set ) ) ) : ( ( ) ( non
empty TopSpace-like compact V221()
V222()
V266()
pathwise_connected being_simple_closed_curve )
SubSpace of
TOP-REAL 2 : ( ( ) ( non
empty ordinal natural complex real ext-real positive non
negative integer V66()
V67()
V68()
V69()
V70()
V71()
V72() )
Element of
NAT : ( ( ) (
V67()
V68()
V69()
V70()
V71()
V72()
V73() non
with_non-empty_elements )
Element of
K6(
REAL : ( ( ) ( non
empty V27()
V67()
V68()
V69()
V73() non
with_non-empty_elements )
set ) ) : ( ( ) ( non
empty )
set ) ) ) : ( (
V254() ) ( non
empty TopSpace-like T_0 T_1 T_2 V136()
V161()
V162()
V163()
V164()
V165()
V166()
V167()
V221()
V222()
V254() )
L19()) ) ) : ( ( ) ( non
empty )
set ) )
Function-like one-to-one total quasi_total onto bijective continuous )
Function of ( ( ) ( non
empty V67()
V68()
V69() )
set ) , ( ( ) ( non
empty )
set ) )
" : ( (
Function-like quasi_total ) ( non
empty V16()
V19( the
carrier of
(Topen_unit_circle (CircleMap : ( ( Function-like quasi_total ) ( non empty V16() V19( the carrier of R^1 : ( ( V303() ) ( non empty strict TopSpace-like V299() V303() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V299() ) TopStruct ) ) : ( ( ) ( non empty V67() V68() V69() ) set ) ) V20( the carrier of (Tunit_circle 2 : ( ( ) ( non empty ordinal natural complex real ext-real positive non negative integer V66() V67() V68() V69() V70() V71() V72() ) Element of NAT : ( ( ) ( V67() V68() V69() V70() V71() V72() V73() non with_non-empty_elements ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( non empty TopSpace-like compact V221() V222() V266() pathwise_connected being_simple_closed_curve ) SubSpace of TOP-REAL 2 : ( ( ) ( non empty ordinal natural complex real ext-real positive non negative integer V66() V67() V68() V69() V70() V71() V72() ) Element of NAT : ( ( ) ( V67() V68() V69() V70() V71() V72() V73() non with_non-empty_elements ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( V254() ) ( non empty TopSpace-like T_0 T_1 T_2 V136() V161() V162() V163() V164() V165() V166() V167() V221() V222() V254() ) L19()) ) : ( ( ) ( non empty ) set ) ) Function-like total quasi_total onto continuous ) Function of ( ( ) ( non empty V67() V68() V69() ) set ) , ( ( ) ( non empty ) set ) ) . (R^1 (1 : ( ( ) ( non empty ordinal natural complex real ext-real positive non negative integer V66() V67() V68() V69() V70() V71() V72() ) Element of NAT : ( ( ) ( V67() V68() V69() V70() V71() V72() V73() non with_non-empty_elements ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) / 2 : ( ( ) ( non empty ordinal natural complex real ext-real positive non negative integer V66() V67() V68() V69() V70() V71() V72() ) Element of NAT : ( ( ) ( V67() V68() V69() V70() V71() V72() V73() non with_non-empty_elements ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( non empty complex real ext-real positive non negative ) Element of REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) ) : ( ( ) ( complex real ext-real ) Point of ( ( ) ( non empty V67() V68() V69() ) set ) ) ) : ( ( ) ( V16() Function-like FinSequence-like ) Element of the carrier of (Tunit_circle 2 : ( ( ) ( non empty ordinal natural complex real ext-real positive non negative integer V66() V67() V68() V69() V70() V71() V72() ) Element of NAT : ( ( ) ( V67() V68() V69() V70() V71() V72() V73() non with_non-empty_elements ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( non empty TopSpace-like compact V221() V222() V266() pathwise_connected being_simple_closed_curve ) SubSpace of TOP-REAL 2 : ( ( ) ( non empty ordinal natural complex real ext-real positive non negative integer V66() V67() V68() V69() V70() V71() V72() ) Element of NAT : ( ( ) ( V67() V68() V69() V70() V71() V72() V73() non with_non-empty_elements ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( V254() ) ( non empty TopSpace-like T_0 T_1 T_2 V136() V161() V162() V163() V164() V165() V166() V167() V221() V222() V254() ) L19()) ) : ( ( ) ( non empty ) set ) ) ) : ( (
strict ) ( non
empty strict TopSpace-like open V221()
V222() )
SubSpace of
Tunit_circle 2 : ( ( ) ( non
empty ordinal natural complex real ext-real positive non
negative integer V66()
V67()
V68()
V69()
V70()
V71()
V72() )
Element of
NAT : ( ( ) (
V67()
V68()
V69()
V70()
V71()
V72()
V73() non
with_non-empty_elements )
Element of
K6(
REAL : ( ( ) ( non
empty V27()
V67()
V68()
V69()
V73() non
with_non-empty_elements )
set ) ) : ( ( ) ( non
empty )
set ) ) ) : ( ( ) ( non
empty TopSpace-like compact V221()
V222()
V266()
pathwise_connected being_simple_closed_curve )
SubSpace of
TOP-REAL 2 : ( ( ) ( non
empty ordinal natural complex real ext-real positive non
negative integer V66()
V67()
V68()
V69()
V70()
V71()
V72() )
Element of
NAT : ( ( ) (
V67()
V68()
V69()
V70()
V71()
V72()
V73() non
with_non-empty_elements )
Element of
K6(
REAL : ( ( ) ( non
empty V27()
V67()
V68()
V69()
V73() non
with_non-empty_elements )
set ) ) : ( ( ) ( non
empty )
set ) ) ) : ( (
V254() ) ( non
empty TopSpace-like T_0 T_1 T_2 V136()
V161()
V162()
V163()
V164()
V165()
V166()
V167()
V221()
V222()
V254() )
L19()) ) ) : ( ( ) ( non
empty )
set ) )
V20( the
carrier of
(R^1 : ( ( V303() ) ( non empty strict TopSpace-like V299() V303() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V299() ) TopStruct ) ) | (R^1 ].(R^1 (1 : ( ( ) ( non empty ordinal natural complex real ext-real positive non negative integer V66() V67() V68() V69() V70() V71() V72() ) Element of NAT : ( ( ) ( V67() V68() V69() V70() V71() V72() V73() non with_non-empty_elements ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) / 2 : ( ( ) ( non empty ordinal natural complex real ext-real positive non negative integer V66() V67() V68() V69() V70() V71() V72() ) Element of NAT : ( ( ) ( V67() V68() V69() V70() V71() V72() V73() non with_non-empty_elements ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( non empty complex real ext-real positive non negative ) Element of REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) ) : ( ( ) ( complex real ext-real ) Point of ( ( ) ( non empty V67() V68() V69() ) set ) ) ,((R^1 (1 : ( ( ) ( non empty ordinal natural complex real ext-real positive non negative integer V66() V67() V68() V69() V70() V71() V72() ) Element of NAT : ( ( ) ( V67() V68() V69() V70() V71() V72() V73() non with_non-empty_elements ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) / 2 : ( ( ) ( non empty ordinal natural complex real ext-real positive non negative integer V66() V67() V68() V69() V70() V71() V72() ) Element of NAT : ( ( ) ( V67() V68() V69() V70() V71() V72() V73() non with_non-empty_elements ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( non empty complex real ext-real positive non negative ) Element of REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) ) : ( ( ) ( complex real ext-real ) Point of ( ( ) ( non empty V67() V68() V69() ) set ) ) + 1 : ( ( ) ( non empty ordinal natural complex real ext-real positive non negative integer V66() V67() V68() V69() V70() V71() V72() ) Element of NAT : ( ( ) ( V67() V68() V69() V70() V71() V72() V73() non with_non-empty_elements ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) .[ : ( ( ) ( non empty open V67() V68() V69() ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V67() V68() V69() open ) Subset of ) ) : ( (
strict ) ( non
empty strict TopSpace-like open V299() )
SubSpace of
R^1 : ( (
V303() ) ( non
empty strict TopSpace-like V299()
V303() )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V299() )
TopStruct ) ) ) : ( ( ) ( non
empty V67()
V68()
V69() )
set ) )
Function-like total quasi_total V51()
V52()
V53() )
Element of
K6(
K7( the
carrier of
(Topen_unit_circle (CircleMap : ( ( Function-like quasi_total ) ( non empty V16() V19( the carrier of R^1 : ( ( V303() ) ( non empty strict TopSpace-like V299() V303() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V299() ) TopStruct ) ) : ( ( ) ( non empty V67() V68() V69() ) set ) ) V20( the carrier of (Tunit_circle 2 : ( ( ) ( non empty ordinal natural complex real ext-real positive non negative integer V66() V67() V68() V69() V70() V71() V72() ) Element of NAT : ( ( ) ( V67() V68() V69() V70() V71() V72() V73() non with_non-empty_elements ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( non empty TopSpace-like compact V221() V222() V266() pathwise_connected being_simple_closed_curve ) SubSpace of TOP-REAL 2 : ( ( ) ( non empty ordinal natural complex real ext-real positive non negative integer V66() V67() V68() V69() V70() V71() V72() ) Element of NAT : ( ( ) ( V67() V68() V69() V70() V71() V72() V73() non with_non-empty_elements ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( V254() ) ( non empty TopSpace-like T_0 T_1 T_2 V136() V161() V162() V163() V164() V165() V166() V167() V221() V222() V254() ) L19()) ) : ( ( ) ( non empty ) set ) ) Function-like total quasi_total onto continuous ) Function of ( ( ) ( non empty V67() V68() V69() ) set ) , ( ( ) ( non empty ) set ) ) . (R^1 (1 : ( ( ) ( non empty ordinal natural complex real ext-real positive non negative integer V66() V67() V68() V69() V70() V71() V72() ) Element of NAT : ( ( ) ( V67() V68() V69() V70() V71() V72() V73() non with_non-empty_elements ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) / 2 : ( ( ) ( non empty ordinal natural complex real ext-real positive non negative integer V66() V67() V68() V69() V70() V71() V72() ) Element of NAT : ( ( ) ( V67() V68() V69() V70() V71() V72() V73() non with_non-empty_elements ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( non empty complex real ext-real positive non negative ) Element of REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) ) : ( ( ) ( complex real ext-real ) Point of ( ( ) ( non empty V67() V68() V69() ) set ) ) ) : ( ( ) ( V16() Function-like FinSequence-like ) Element of the carrier of (Tunit_circle 2 : ( ( ) ( non empty ordinal natural complex real ext-real positive non negative integer V66() V67() V68() V69() V70() V71() V72() ) Element of NAT : ( ( ) ( V67() V68() V69() V70() V71() V72() V73() non with_non-empty_elements ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( non empty TopSpace-like compact V221() V222() V266() pathwise_connected being_simple_closed_curve ) SubSpace of TOP-REAL 2 : ( ( ) ( non empty ordinal natural complex real ext-real positive non negative integer V66() V67() V68() V69() V70() V71() V72() ) Element of NAT : ( ( ) ( V67() V68() V69() V70() V71() V72() V73() non with_non-empty_elements ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( V254() ) ( non empty TopSpace-like T_0 T_1 T_2 V136() V161() V162() V163() V164() V165() V166() V167() V221() V222() V254() ) L19()) ) : ( ( ) ( non empty ) set ) ) ) : ( (
strict ) ( non
empty strict TopSpace-like open V221()
V222() )
SubSpace of
Tunit_circle 2 : ( ( ) ( non
empty ordinal natural complex real ext-real positive non
negative integer V66()
V67()
V68()
V69()
V70()
V71()
V72() )
Element of
NAT : ( ( ) (
V67()
V68()
V69()
V70()
V71()
V72()
V73() non
with_non-empty_elements )
Element of
K6(
REAL : ( ( ) ( non
empty V27()
V67()
V68()
V69()
V73() non
with_non-empty_elements )
set ) ) : ( ( ) ( non
empty )
set ) ) ) : ( ( ) ( non
empty TopSpace-like compact V221()
V222()
V266()
pathwise_connected being_simple_closed_curve )
SubSpace of
TOP-REAL 2 : ( ( ) ( non
empty ordinal natural complex real ext-real positive non
negative integer V66()
V67()
V68()
V69()
V70()
V71()
V72() )
Element of
NAT : ( ( ) (
V67()
V68()
V69()
V70()
V71()
V72()
V73() non
with_non-empty_elements )
Element of
K6(
REAL : ( ( ) ( non
empty V27()
V67()
V68()
V69()
V73() non
with_non-empty_elements )
set ) ) : ( ( ) ( non
empty )
set ) ) ) : ( (
V254() ) ( non
empty TopSpace-like T_0 T_1 T_2 V136()
V161()
V162()
V163()
V164()
V165()
V166()
V167()
V221()
V222()
V254() )
L19()) ) ) : ( ( ) ( non
empty )
set ) , the
carrier of
(R^1 : ( ( V303() ) ( non empty strict TopSpace-like V299() V303() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V299() ) TopStruct ) ) | (R^1 ].(R^1 (1 : ( ( ) ( non empty ordinal natural complex real ext-real positive non negative integer V66() V67() V68() V69() V70() V71() V72() ) Element of NAT : ( ( ) ( V67() V68() V69() V70() V71() V72() V73() non with_non-empty_elements ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) / 2 : ( ( ) ( non empty ordinal natural complex real ext-real positive non negative integer V66() V67() V68() V69() V70() V71() V72() ) Element of NAT : ( ( ) ( V67() V68() V69() V70() V71() V72() V73() non with_non-empty_elements ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( non empty complex real ext-real positive non negative ) Element of REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) ) : ( ( ) ( complex real ext-real ) Point of ( ( ) ( non empty V67() V68() V69() ) set ) ) ,((R^1 (1 : ( ( ) ( non empty ordinal natural complex real ext-real positive non negative integer V66() V67() V68() V69() V70() V71() V72() ) Element of NAT : ( ( ) ( V67() V68() V69() V70() V71() V72() V73() non with_non-empty_elements ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) / 2 : ( ( ) ( non empty ordinal natural complex real ext-real positive non negative integer V66() V67() V68() V69() V70() V71() V72() ) Element of NAT : ( ( ) ( V67() V68() V69() V70() V71() V72() V73() non with_non-empty_elements ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( non empty complex real ext-real positive non negative ) Element of REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) ) : ( ( ) ( complex real ext-real ) Point of ( ( ) ( non empty V67() V68() V69() ) set ) ) + 1 : ( ( ) ( non empty ordinal natural complex real ext-real positive non negative integer V66() V67() V68() V69() V70() V71() V72() ) Element of NAT : ( ( ) ( V67() V68() V69() V70() V71() V72() V73() non with_non-empty_elements ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) .[ : ( ( ) ( non empty open V67() V68() V69() ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V67() V68() V69() open ) Subset of ) ) : ( (
strict ) ( non
empty strict TopSpace-like open V299() )
SubSpace of
R^1 : ( (
V303() ) ( non
empty strict TopSpace-like V299()
V303() )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V299() )
TopStruct ) ) ) : ( ( ) ( non
empty V67()
V68()
V69() )
set ) ) : ( ( ) ( non
empty V51()
V52()
V53() )
set ) ) : ( ( ) ( non
empty )
set ) )
= Circle2IntervalL : ( (
Function-like quasi_total ) ( non
empty V16()
V19( the
carrier of
(Topen_unit_circle c[-10] : ( ( ) ( V16() Function-like FinSequence-like ) Point of ( ( ) ( non empty ) set ) ) ) : ( (
strict ) ( non
empty strict TopSpace-like open V221()
V222() )
SubSpace of
Tunit_circle 2 : ( ( ) ( non
empty ordinal natural complex real ext-real positive non
negative integer V66()
V67()
V68()
V69()
V70()
V71()
V72() )
Element of
NAT : ( ( ) (
V67()
V68()
V69()
V70()
V71()
V72()
V73() non
with_non-empty_elements )
Element of
K6(
REAL : ( ( ) ( non
empty V27()
V67()
V68()
V69()
V73() non
with_non-empty_elements )
set ) ) : ( ( ) ( non
empty )
set ) ) ) : ( ( ) ( non
empty TopSpace-like compact V221()
V222()
V266()
pathwise_connected being_simple_closed_curve )
SubSpace of
TOP-REAL 2 : ( ( ) ( non
empty ordinal natural complex real ext-real positive non
negative integer V66()
V67()
V68()
V69()
V70()
V71()
V72() )
Element of
NAT : ( ( ) (
V67()
V68()
V69()
V70()
V71()
V72()
V73() non
with_non-empty_elements )
Element of
K6(
REAL : ( ( ) ( non
empty V27()
V67()
V68()
V69()
V73() non
with_non-empty_elements )
set ) ) : ( ( ) ( non
empty )
set ) ) ) : ( (
V254() ) ( non
empty TopSpace-like T_0 T_1 T_2 V136()
V161()
V162()
V163()
V164()
V165()
V166()
V167()
V221()
V222()
V254() )
L19()) ) ) : ( ( ) ( non
empty )
set ) )
V20( the
carrier of
(R^1 : ( ( V303() ) ( non empty strict TopSpace-like V299() V303() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V299() ) TopStruct ) ) | (R^1 ].(1 : ( ( ) ( non empty ordinal natural complex real ext-real positive non negative integer V66() V67() V68() V69() V70() V71() V72() ) Element of NAT : ( ( ) ( V67() V68() V69() V70() V71() V72() V73() non with_non-empty_elements ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) / 2 : ( ( ) ( non empty ordinal natural complex real ext-real positive non negative integer V66() V67() V68() V69() V70() V71() V72() ) Element of NAT : ( ( ) ( V67() V68() V69() V70() V71() V72() V73() non with_non-empty_elements ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( non empty complex real ext-real positive non negative ) Element of REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) ,(3 : ( ( ) ( non empty ordinal natural complex real ext-real positive non negative integer V66() V67() V68() V69() V70() V71() V72() ) Element of NAT : ( ( ) ( V67() V68() V69() V70() V71() V72() V73() non with_non-empty_elements ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) / 2 : ( ( ) ( non empty ordinal natural complex real ext-real positive non negative integer V66() V67() V68() V69() V70() V71() V72() ) Element of NAT : ( ( ) ( V67() V68() V69() V70() V71() V72() V73() non with_non-empty_elements ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( non empty complex real ext-real positive non negative ) Element of REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) .[ : ( ( ) ( non empty open V67() V68() V69() ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V67() V68() V69() open ) Subset of ) ) : ( (
strict ) ( non
empty strict TopSpace-like open V299() )
SubSpace of
R^1 : ( (
V303() ) ( non
empty strict TopSpace-like V299()
V303() )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V299() )
TopStruct ) ) ) : ( ( ) ( non
empty V67()
V68()
V69() )
set ) )
Function-like total quasi_total V51()
V52()
V53() )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty V67()
V68()
V69() )
set ) ) ;
theorem
ex
F being ( ( ) ( )
Subset-Family of ) st
(
F : ( ( ) ( )
Subset-Family of )
= {(CircleMap : ( ( Function-like quasi_total ) ( non empty V16() V19( the carrier of R^1 : ( ( V303() ) ( non empty strict TopSpace-like V299() V303() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V299() ) TopStruct ) ) : ( ( ) ( non empty V67() V68() V69() ) set ) ) V20( the carrier of (Tunit_circle 2 : ( ( ) ( non empty ordinal natural complex real ext-real positive non negative integer V66() V67() V68() V69() V70() V71() V72() ) Element of NAT : ( ( ) ( V67() V68() V69() V70() V71() V72() V73() non with_non-empty_elements ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( non empty TopSpace-like compact V221() V222() V266() pathwise_connected being_simple_closed_curve ) SubSpace of TOP-REAL 2 : ( ( ) ( non empty ordinal natural complex real ext-real positive non negative integer V66() V67() V68() V69() V70() V71() V72() ) Element of NAT : ( ( ) ( V67() V68() V69() V70() V71() V72() V73() non with_non-empty_elements ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( V254() ) ( non empty TopSpace-like T_0 T_1 T_2 V136() V161() V162() V163() V164() V165() V166() V167() V221() V222() V254() ) L19()) ) : ( ( ) ( non empty ) set ) ) Function-like total quasi_total onto continuous ) Function of ( ( ) ( non empty V67() V68() V69() ) set ) , ( ( ) ( non empty ) set ) ) .: ].0 : ( ( ) ( empty trivial ordinal natural complex real ext-real non positive non negative Function-like functional integer V66() V67() V68() V69() V70() V71() V72() V73() ) Element of NAT : ( ( ) ( V67() V68() V69() V70() V71() V72() V73() non with_non-empty_elements ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ordinal natural complex real ext-real positive non negative integer V66() V67() V68() V69() V70() V71() V72() ) Element of NAT : ( ( ) ( V67() V68() V69() V70() V71() V72() V73() non with_non-empty_elements ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) .[ : ( ( ) ( non empty open V67() V68() V69() ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of K6( the carrier of (Tunit_circle 2 : ( ( ) ( non empty ordinal natural complex real ext-real positive non negative integer V66() V67() V68() V69() V70() V71() V72() ) Element of NAT : ( ( ) ( V67() V68() V69() V70() V71() V72() V73() non with_non-empty_elements ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( non empty TopSpace-like compact V221() V222() V266() pathwise_connected being_simple_closed_curve ) SubSpace of TOP-REAL 2 : ( ( ) ( non empty ordinal natural complex real ext-real positive non negative integer V66() V67() V68() V69() V70() V71() V72() ) Element of NAT : ( ( ) ( V67() V68() V69() V70() V71() V72() V73() non with_non-empty_elements ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( V254() ) ( non empty TopSpace-like T_0 T_1 T_2 V136() V161() V162() V163() V164() V165() V166() V167() V221() V222() V254() ) L19()) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,(CircleMap : ( ( Function-like quasi_total ) ( non empty V16() V19( the carrier of R^1 : ( ( V303() ) ( non empty strict TopSpace-like V299() V303() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V299() ) TopStruct ) ) : ( ( ) ( non empty V67() V68() V69() ) set ) ) V20( the carrier of (Tunit_circle 2 : ( ( ) ( non empty ordinal natural complex real ext-real positive non negative integer V66() V67() V68() V69() V70() V71() V72() ) Element of NAT : ( ( ) ( V67() V68() V69() V70() V71() V72() V73() non with_non-empty_elements ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( non empty TopSpace-like compact V221() V222() V266() pathwise_connected being_simple_closed_curve ) SubSpace of TOP-REAL 2 : ( ( ) ( non empty ordinal natural complex real ext-real positive non negative integer V66() V67() V68() V69() V70() V71() V72() ) Element of NAT : ( ( ) ( V67() V68() V69() V70() V71() V72() V73() non with_non-empty_elements ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( V254() ) ( non empty TopSpace-like T_0 T_1 T_2 V136() V161() V162() V163() V164() V165() V166() V167() V221() V222() V254() ) L19()) ) : ( ( ) ( non empty ) set ) ) Function-like total quasi_total onto continuous ) Function of ( ( ) ( non empty V67() V68() V69() ) set ) , ( ( ) ( non empty ) set ) ) .: ].(1 : ( ( ) ( non empty ordinal natural complex real ext-real positive non negative integer V66() V67() V68() V69() V70() V71() V72() ) Element of NAT : ( ( ) ( V67() V68() V69() V70() V71() V72() V73() non with_non-empty_elements ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) / 2 : ( ( ) ( non empty ordinal natural complex real ext-real positive non negative integer V66() V67() V68() V69() V70() V71() V72() ) Element of NAT : ( ( ) ( V67() V68() V69() V70() V71() V72() V73() non with_non-empty_elements ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( non empty complex real ext-real positive non negative ) Element of REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) ,(3 : ( ( ) ( non empty ordinal natural complex real ext-real positive non negative integer V66() V67() V68() V69() V70() V71() V72() ) Element of NAT : ( ( ) ( V67() V68() V69() V70() V71() V72() V73() non with_non-empty_elements ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) / 2 : ( ( ) ( non empty ordinal natural complex real ext-real positive non negative integer V66() V67() V68() V69() V70() V71() V72() ) Element of NAT : ( ( ) ( V67() V68() V69() V70() V71() V72() V73() non with_non-empty_elements ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( non empty complex real ext-real positive non negative ) Element of REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) .[ : ( ( ) ( non empty open V67() V68() V69() ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of K6( the carrier of (Tunit_circle 2 : ( ( ) ( non empty ordinal natural complex real ext-real positive non negative integer V66() V67() V68() V69() V70() V71() V72() ) Element of NAT : ( ( ) ( V67() V68() V69() V70() V71() V72() V73() non with_non-empty_elements ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( non empty TopSpace-like compact V221() V222() V266() pathwise_connected being_simple_closed_curve ) SubSpace of TOP-REAL 2 : ( ( ) ( non empty ordinal natural complex real ext-real positive non negative integer V66() V67() V68() V69() V70() V71() V72() ) Element of NAT : ( ( ) ( V67() V68() V69() V70() V71() V72() V73() non with_non-empty_elements ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( V254() ) ( non empty TopSpace-like T_0 T_1 T_2 V136() V161() V162() V163() V164() V165() V166() V167() V221() V222() V254() ) L19()) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) } : ( ( ) ( non
empty )
Element of
K6(
K6( the
carrier of
(Tunit_circle 2 : ( ( ) ( non empty ordinal natural complex real ext-real positive non negative integer V66() V67() V68() V69() V70() V71() V72() ) Element of NAT : ( ( ) ( V67() V68() V69() V70() V71() V72() V73() non with_non-empty_elements ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( non
empty TopSpace-like compact V221()
V222()
V266()
pathwise_connected being_simple_closed_curve )
SubSpace of
TOP-REAL 2 : ( ( ) ( non
empty ordinal natural complex real ext-real positive non
negative integer V66()
V67()
V68()
V69()
V70()
V71()
V72() )
Element of
NAT : ( ( ) (
V67()
V68()
V69()
V70()
V71()
V72()
V73() non
with_non-empty_elements )
Element of
K6(
REAL : ( ( ) ( non
empty V27()
V67()
V68()
V69()
V73() non
with_non-empty_elements )
set ) ) : ( ( ) ( non
empty )
set ) ) ) : ( (
V254() ) ( non
empty TopSpace-like T_0 T_1 T_2 V136()
V161()
V162()
V163()
V164()
V165()
V166()
V167()
V221()
V222()
V254() )
L19()) ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) ) &
F : ( ( ) ( )
Subset-Family of ) is ( ( ) ( )
Cover of ( ( ) ( non
empty )
set ) ) &
F : ( ( ) ( )
Subset-Family of ) is
open & ( for
U being ( ( ) ( )
Subset of ) holds
( (
U : ( ( ) ( )
Subset of )
= CircleMap : ( (
Function-like quasi_total ) ( non
empty V16()
V19( the
carrier of
R^1 : ( (
V303() ) ( non
empty strict TopSpace-like V299()
V303() )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V299() )
TopStruct ) ) : ( ( ) ( non
empty V67()
V68()
V69() )
set ) )
V20( the
carrier of
(Tunit_circle 2 : ( ( ) ( non empty ordinal natural complex real ext-real positive non negative integer V66() V67() V68() V69() V70() V71() V72() ) Element of NAT : ( ( ) ( V67() V68() V69() V70() V71() V72() V73() non with_non-empty_elements ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( non
empty TopSpace-like compact V221()
V222()
V266()
pathwise_connected being_simple_closed_curve )
SubSpace of
TOP-REAL 2 : ( ( ) ( non
empty ordinal natural complex real ext-real positive non
negative integer V66()
V67()
V68()
V69()
V70()
V71()
V72() )
Element of
NAT : ( ( ) (
V67()
V68()
V69()
V70()
V71()
V72()
V73() non
with_non-empty_elements )
Element of
K6(
REAL : ( ( ) ( non
empty V27()
V67()
V68()
V69()
V73() non
with_non-empty_elements )
set ) ) : ( ( ) ( non
empty )
set ) ) ) : ( (
V254() ) ( non
empty TopSpace-like T_0 T_1 T_2 V136()
V161()
V162()
V163()
V164()
V165()
V166()
V167()
V221()
V222()
V254() )
L19()) ) : ( ( ) ( non
empty )
set ) )
Function-like total quasi_total onto continuous )
Function of ( ( ) ( non
empty V67()
V68()
V69() )
set ) , ( ( ) ( non
empty )
set ) )
.: ].0 : ( ( ) ( empty trivial ordinal natural complex real ext-real non positive non negative Function-like functional integer V66() V67() V68() V69() V70() V71() V72() V73() ) Element of NAT : ( ( ) ( V67() V68() V69() V70() V71() V72() V73() non with_non-empty_elements ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ordinal natural complex real ext-real positive non negative integer V66() V67() V68() V69() V70() V71() V72() ) Element of NAT : ( ( ) ( V67() V68() V69() V70() V71() V72() V73() non with_non-empty_elements ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) .[ : ( ( ) ( non
empty open V67()
V68()
V69() )
Element of
K6(
REAL : ( ( ) ( non
empty V27()
V67()
V68()
V69()
V73() non
with_non-empty_elements )
set ) ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
Element of
K6( the
carrier of
(Tunit_circle 2 : ( ( ) ( non empty ordinal natural complex real ext-real positive non negative integer V66() V67() V68() V69() V70() V71() V72() ) Element of NAT : ( ( ) ( V67() V68() V69() V70() V71() V72() V73() non with_non-empty_elements ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( non
empty TopSpace-like compact V221()
V222()
V266()
pathwise_connected being_simple_closed_curve )
SubSpace of
TOP-REAL 2 : ( ( ) ( non
empty ordinal natural complex real ext-real positive non
negative integer V66()
V67()
V68()
V69()
V70()
V71()
V72() )
Element of
NAT : ( ( ) (
V67()
V68()
V69()
V70()
V71()
V72()
V73() non
with_non-empty_elements )
Element of
K6(
REAL : ( ( ) ( non
empty V27()
V67()
V68()
V69()
V73() non
with_non-empty_elements )
set ) ) : ( ( ) ( non
empty )
set ) ) ) : ( (
V254() ) ( non
empty TopSpace-like T_0 T_1 T_2 V136()
V161()
V162()
V163()
V164()
V165()
V166()
V167()
V221()
V222()
V254() )
L19()) ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) ) implies (
union (IntIntervals (0 : ( ( ) ( empty trivial ordinal natural complex real ext-real non positive non negative Function-like functional integer V66() V67() V68() V69() V70() V71() V72() V73() ) Element of NAT : ( ( ) ( V67() V68() V69() V70() V71() V72() V73() non with_non-empty_elements ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ordinal natural complex real ext-real positive non negative integer V66() V67() V68() V69() V70() V71() V72() ) Element of NAT : ( ( ) ( V67() V68() V69() V70() V71() V72() V73() non with_non-empty_elements ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) )) : ( (
open ) ( non
empty open )
Subset-Family of ) : ( ( ) (
V67()
V68()
V69() )
Element of
K6( the
carrier of
R^1 : ( (
V303() ) ( non
empty strict TopSpace-like V299()
V303() )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V299() )
TopStruct ) ) : ( ( ) ( non
empty V67()
V68()
V69() )
set ) ) : ( ( ) ( non
empty )
set ) )
= CircleMap : ( (
Function-like quasi_total ) ( non
empty V16()
V19( the
carrier of
R^1 : ( (
V303() ) ( non
empty strict TopSpace-like V299()
V303() )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V299() )
TopStruct ) ) : ( ( ) ( non
empty V67()
V68()
V69() )
set ) )
V20( the
carrier of
(Tunit_circle 2 : ( ( ) ( non empty ordinal natural complex real ext-real positive non negative integer V66() V67() V68() V69() V70() V71() V72() ) Element of NAT : ( ( ) ( V67() V68() V69() V70() V71() V72() V73() non with_non-empty_elements ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( non
empty TopSpace-like compact V221()
V222()
V266()
pathwise_connected being_simple_closed_curve )
SubSpace of
TOP-REAL 2 : ( ( ) ( non
empty ordinal natural complex real ext-real positive non
negative integer V66()
V67()
V68()
V69()
V70()
V71()
V72() )
Element of
NAT : ( ( ) (
V67()
V68()
V69()
V70()
V71()
V72()
V73() non
with_non-empty_elements )
Element of
K6(
REAL : ( ( ) ( non
empty V27()
V67()
V68()
V69()
V73() non
with_non-empty_elements )
set ) ) : ( ( ) ( non
empty )
set ) ) ) : ( (
V254() ) ( non
empty TopSpace-like T_0 T_1 T_2 V136()
V161()
V162()
V163()
V164()
V165()
V166()
V167()
V221()
V222()
V254() )
L19()) ) : ( ( ) ( non
empty )
set ) )
Function-like total quasi_total onto continuous )
Function of ( ( ) ( non
empty V67()
V68()
V69() )
set ) , ( ( ) ( non
empty )
set ) )
" U : ( ( ) ( )
Subset of ) : ( ( ) (
V67()
V68()
V69() )
Element of
K6( the
carrier of
R^1 : ( (
V303() ) ( non
empty strict TopSpace-like V299()
V303() )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V299() )
TopStruct ) ) : ( ( ) ( non
empty V67()
V68()
V69() )
set ) ) : ( ( ) ( non
empty )
set ) ) & ( for
d being ( ( ) (
V67()
V68()
V69() )
Subset of ) st
d : ( ( ) (
V67()
V68()
V69() )
Subset of )
in IntIntervals (
0 : ( ( ) (
empty trivial ordinal natural complex real ext-real non
positive non
negative Function-like functional integer V66()
V67()
V68()
V69()
V70()
V71()
V72()
V73() )
Element of
NAT : ( ( ) (
V67()
V68()
V69()
V70()
V71()
V72()
V73() non
with_non-empty_elements )
Element of
K6(
REAL : ( ( ) ( non
empty V27()
V67()
V68()
V69()
V73() non
with_non-empty_elements )
set ) ) : ( ( ) ( non
empty )
set ) ) ) ,1 : ( ( ) ( non
empty ordinal natural complex real ext-real positive non
negative integer V66()
V67()
V68()
V69()
V70()
V71()
V72() )
Element of
NAT : ( ( ) (
V67()
V68()
V69()
V70()
V71()
V72()
V73() non
with_non-empty_elements )
Element of
K6(
REAL : ( ( ) ( non
empty V27()
V67()
V68()
V69()
V73() non
with_non-empty_elements )
set ) ) : ( ( ) ( non
empty )
set ) ) ) ) : ( (
open ) ( non
empty open )
Subset-Family of ) holds
for
f being ( (
Function-like quasi_total ) (
V16()
V19( the
carrier of
(R^1 : ( ( V303() ) ( non empty strict TopSpace-like V299() V303() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V299() ) TopStruct ) ) | b3 : ( ( ) ( V67() V68() V69() ) Subset of ) ) : ( (
strict ) (
strict TopSpace-like V299() )
SubSpace of
R^1 : ( (
V303() ) ( non
empty strict TopSpace-like V299()
V303() )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V299() )
TopStruct ) ) ) : ( ( ) (
V67()
V68()
V69() )
set ) )
V20( the
carrier of
((Tunit_circle 2 : ( ( ) ( non empty ordinal natural complex real ext-real positive non negative integer V66() V67() V68() V69() V70() V71() V72() ) Element of NAT : ( ( ) ( V67() V68() V69() V70() V71() V72() V73() non with_non-empty_elements ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( non empty TopSpace-like compact V221() V222() V266() pathwise_connected being_simple_closed_curve ) SubSpace of TOP-REAL 2 : ( ( ) ( non empty ordinal natural complex real ext-real positive non negative integer V66() V67() V68() V69() V70() V71() V72() ) Element of NAT : ( ( ) ( V67() V68() V69() V70() V71() V72() V73() non with_non-empty_elements ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( V254() ) ( non empty TopSpace-like T_0 T_1 T_2 V136() V161() V162() V163() V164() V165() V166() V167() V221() V222() V254() ) L19()) ) | b2 : ( ( ) ( ) Subset of ) ) : ( (
strict ) (
strict TopSpace-like V221()
V222() )
SubSpace of
Tunit_circle 2 : ( ( ) ( non
empty ordinal natural complex real ext-real positive non
negative integer V66()
V67()
V68()
V69()
V70()
V71()
V72() )
Element of
NAT : ( ( ) (
V67()
V68()
V69()
V70()
V71()
V72()
V73() non
with_non-empty_elements )
Element of
K6(
REAL : ( ( ) ( non
empty V27()
V67()
V68()
V69()
V73() non
with_non-empty_elements )
set ) ) : ( ( ) ( non
empty )
set ) ) ) : ( ( ) ( non
empty TopSpace-like compact V221()
V222()
V266()
pathwise_connected being_simple_closed_curve )
SubSpace of
TOP-REAL 2 : ( ( ) ( non
empty ordinal natural complex real ext-real positive non
negative integer V66()
V67()
V68()
V69()
V70()
V71()
V72() )
Element of
NAT : ( ( ) (
V67()
V68()
V69()
V70()
V71()
V72()
V73() non
with_non-empty_elements )
Element of
K6(
REAL : ( ( ) ( non
empty V27()
V67()
V68()
V69()
V73() non
with_non-empty_elements )
set ) ) : ( ( ) ( non
empty )
set ) ) ) : ( (
V254() ) ( non
empty TopSpace-like T_0 T_1 T_2 V136()
V161()
V162()
V163()
V164()
V165()
V166()
V167()
V221()
V222()
V254() )
L19()) ) ) : ( ( ) ( )
set ) )
Function-like quasi_total )
Function of ( ( ) (
V67()
V68()
V69() )
set ) , ( ( ) ( )
set ) ) st
f : ( (
Function-like quasi_total ) (
V16()
V19( the
carrier of
(R^1 : ( ( V303() ) ( non empty strict TopSpace-like V299() V303() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V299() ) TopStruct ) ) | b3 : ( ( ) ( V67() V68() V69() ) Subset of ) ) : ( (
strict ) (
strict TopSpace-like V299() )
SubSpace of
R^1 : ( (
V303() ) ( non
empty strict TopSpace-like V299()
V303() )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V299() )
TopStruct ) ) ) : ( ( ) (
V67()
V68()
V69() )
set ) )
V20( the
carrier of
((Tunit_circle 2 : ( ( ) ( non empty ordinal natural complex real ext-real positive non negative integer V66() V67() V68() V69() V70() V71() V72() ) Element of NAT : ( ( ) ( V67() V68() V69() V70() V71() V72() V73() non with_non-empty_elements ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( non empty TopSpace-like compact V221() V222() V266() pathwise_connected being_simple_closed_curve ) SubSpace of TOP-REAL 2 : ( ( ) ( non empty ordinal natural complex real ext-real positive non negative integer V66() V67() V68() V69() V70() V71() V72() ) Element of NAT : ( ( ) ( V67() V68() V69() V70() V71() V72() V73() non with_non-empty_elements ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( V254() ) ( non empty TopSpace-like T_0 T_1 T_2 V136() V161() V162() V163() V164() V165() V166() V167() V221() V222() V254() ) L19()) ) | b2 : ( ( ) ( ) Subset of ) ) : ( (
strict ) (
strict TopSpace-like V221()
V222() )
SubSpace of
Tunit_circle 2 : ( ( ) ( non
empty ordinal natural complex real ext-real positive non
negative integer V66()
V67()
V68()
V69()
V70()
V71()
V72() )
Element of
NAT : ( ( ) (
V67()
V68()
V69()
V70()
V71()
V72()
V73() non
with_non-empty_elements )
Element of
K6(
REAL : ( ( ) ( non
empty V27()
V67()
V68()
V69()
V73() non
with_non-empty_elements )
set ) ) : ( ( ) ( non
empty )
set ) ) ) : ( ( ) ( non
empty TopSpace-like compact V221()
V222()
V266()
pathwise_connected being_simple_closed_curve )
SubSpace of
TOP-REAL 2 : ( ( ) ( non
empty ordinal natural complex real ext-real positive non
negative integer V66()
V67()
V68()
V69()
V70()
V71()
V72() )
Element of
NAT : ( ( ) (
V67()
V68()
V69()
V70()
V71()
V72()
V73() non
with_non-empty_elements )
Element of
K6(
REAL : ( ( ) ( non
empty V27()
V67()
V68()
V69()
V73() non
with_non-empty_elements )
set ) ) : ( ( ) ( non
empty )
set ) ) ) : ( (
V254() ) ( non
empty TopSpace-like T_0 T_1 T_2 V136()
V161()
V162()
V163()
V164()
V165()
V166()
V167()
V221()
V222()
V254() )
L19()) ) ) : ( ( ) ( )
set ) )
Function-like quasi_total )
Function of ( ( ) (
V67()
V68()
V69() )
set ) , ( ( ) ( )
set ) )
= CircleMap : ( (
Function-like quasi_total ) ( non
empty V16()
V19( the
carrier of
R^1 : ( (
V303() ) ( non
empty strict TopSpace-like V299()
V303() )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V299() )
TopStruct ) ) : ( ( ) ( non
empty V67()
V68()
V69() )
set ) )
V20( the
carrier of
(Tunit_circle 2 : ( ( ) ( non empty ordinal natural complex real ext-real positive non negative integer V66() V67() V68() V69() V70() V71() V72() ) Element of NAT : ( ( ) ( V67() V68() V69() V70() V71() V72() V73() non with_non-empty_elements ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( non
empty TopSpace-like compact V221()
V222()
V266()
pathwise_connected being_simple_closed_curve )
SubSpace of
TOP-REAL 2 : ( ( ) ( non
empty ordinal natural complex real ext-real positive non
negative integer V66()
V67()
V68()
V69()
V70()
V71()
V72() )
Element of
NAT : ( ( ) (
V67()
V68()
V69()
V70()
V71()
V72()
V73() non
with_non-empty_elements )
Element of
K6(
REAL : ( ( ) ( non
empty V27()
V67()
V68()
V69()
V73() non
with_non-empty_elements )
set ) ) : ( ( ) ( non
empty )
set ) ) ) : ( (
V254() ) ( non
empty TopSpace-like T_0 T_1 T_2 V136()
V161()
V162()
V163()
V164()
V165()
V166()
V167()
V221()
V222()
V254() )
L19()) ) : ( ( ) ( non
empty )
set ) )
Function-like total quasi_total onto continuous )
Function of ( ( ) ( non
empty V67()
V68()
V69() )
set ) , ( ( ) ( non
empty )
set ) )
| d : ( ( ) (
V67()
V68()
V69() )
Subset of ) : ( (
Function-like ) (
V16()
V19( the
carrier of
R^1 : ( (
V303() ) ( non
empty strict TopSpace-like V299()
V303() )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V299() )
TopStruct ) ) : ( ( ) ( non
empty V67()
V68()
V69() )
set ) )
V20( the
carrier of
(Tunit_circle 2 : ( ( ) ( non empty ordinal natural complex real ext-real positive non negative integer V66() V67() V68() V69() V70() V71() V72() ) Element of NAT : ( ( ) ( V67() V68() V69() V70() V71() V72() V73() non with_non-empty_elements ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( non
empty TopSpace-like compact V221()
V222()
V266()
pathwise_connected being_simple_closed_curve )
SubSpace of
TOP-REAL 2 : ( ( ) ( non
empty ordinal natural complex real ext-real positive non
negative integer V66()
V67()
V68()
V69()
V70()
V71()
V72() )
Element of
NAT : ( ( ) (
V67()
V68()
V69()
V70()
V71()
V72()
V73() non
with_non-empty_elements )
Element of
K6(
REAL : ( ( ) ( non
empty V27()
V67()
V68()
V69()
V73() non
with_non-empty_elements )
set ) ) : ( ( ) ( non
empty )
set ) ) ) : ( (
V254() ) ( non
empty TopSpace-like T_0 T_1 T_2 V136()
V161()
V162()
V163()
V164()
V165()
V166()
V167()
V221()
V222()
V254() )
L19()) ) : ( ( ) ( non
empty )
set ) )
Function-like )
Element of
K6(
K7( the
carrier of
R^1 : ( (
V303() ) ( non
empty strict TopSpace-like V299()
V303() )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V299() )
TopStruct ) ) : ( ( ) ( non
empty V67()
V68()
V69() )
set ) , the
carrier of
(Tunit_circle 2 : ( ( ) ( non empty ordinal natural complex real ext-real positive non negative integer V66() V67() V68() V69() V70() V71() V72() ) Element of NAT : ( ( ) ( V67() V68() V69() V70() V71() V72() V73() non with_non-empty_elements ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( non
empty TopSpace-like compact V221()
V222()
V266()
pathwise_connected being_simple_closed_curve )
SubSpace of
TOP-REAL 2 : ( ( ) ( non
empty ordinal natural complex real ext-real positive non
negative integer V66()
V67()
V68()
V69()
V70()
V71()
V72() )
Element of
NAT : ( ( ) (
V67()
V68()
V69()
V70()
V71()
V72()
V73() non
with_non-empty_elements )
Element of
K6(
REAL : ( ( ) ( non
empty V27()
V67()
V68()
V69()
V73() non
with_non-empty_elements )
set ) ) : ( ( ) ( non
empty )
set ) ) ) : ( (
V254() ) ( non
empty TopSpace-like T_0 T_1 T_2 V136()
V161()
V162()
V163()
V164()
V165()
V166()
V167()
V221()
V222()
V254() )
L19()) ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) ) holds
f : ( (
Function-like quasi_total ) (
V16()
V19( the
carrier of
(R^1 : ( ( V303() ) ( non empty strict TopSpace-like V299() V303() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V299() ) TopStruct ) ) | b3 : ( ( ) ( V67() V68() V69() ) Subset of ) ) : ( (
strict ) (
strict TopSpace-like V299() )
SubSpace of
R^1 : ( (
V303() ) ( non
empty strict TopSpace-like V299()
V303() )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V299() )
TopStruct ) ) ) : ( ( ) (
V67()
V68()
V69() )
set ) )
V20( the
carrier of
((Tunit_circle 2 : ( ( ) ( non empty ordinal natural complex real ext-real positive non negative integer V66() V67() V68() V69() V70() V71() V72() ) Element of NAT : ( ( ) ( V67() V68() V69() V70() V71() V72() V73() non with_non-empty_elements ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( non empty TopSpace-like compact V221() V222() V266() pathwise_connected being_simple_closed_curve ) SubSpace of TOP-REAL 2 : ( ( ) ( non empty ordinal natural complex real ext-real positive non negative integer V66() V67() V68() V69() V70() V71() V72() ) Element of NAT : ( ( ) ( V67() V68() V69() V70() V71() V72() V73() non with_non-empty_elements ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( V254() ) ( non empty TopSpace-like T_0 T_1 T_2 V136() V161() V162() V163() V164() V165() V166() V167() V221() V222() V254() ) L19()) ) | b2 : ( ( ) ( ) Subset of ) ) : ( (
strict ) (
strict TopSpace-like V221()
V222() )
SubSpace of
Tunit_circle 2 : ( ( ) ( non
empty ordinal natural complex real ext-real positive non
negative integer V66()
V67()
V68()
V69()
V70()
V71()
V72() )
Element of
NAT : ( ( ) (
V67()
V68()
V69()
V70()
V71()
V72()
V73() non
with_non-empty_elements )
Element of
K6(
REAL : ( ( ) ( non
empty V27()
V67()
V68()
V69()
V73() non
with_non-empty_elements )
set ) ) : ( ( ) ( non
empty )
set ) ) ) : ( ( ) ( non
empty TopSpace-like compact V221()
V222()
V266()
pathwise_connected being_simple_closed_curve )
SubSpace of
TOP-REAL 2 : ( ( ) ( non
empty ordinal natural complex real ext-real positive non
negative integer V66()
V67()
V68()
V69()
V70()
V71()
V72() )
Element of
NAT : ( ( ) (
V67()
V68()
V69()
V70()
V71()
V72()
V73() non
with_non-empty_elements )
Element of
K6(
REAL : ( ( ) ( non
empty V27()
V67()
V68()
V69()
V73() non
with_non-empty_elements )
set ) ) : ( ( ) ( non
empty )
set ) ) ) : ( (
V254() ) ( non
empty TopSpace-like T_0 T_1 T_2 V136()
V161()
V162()
V163()
V164()
V165()
V166()
V167()
V221()
V222()
V254() )
L19()) ) ) : ( ( ) ( )
set ) )
Function-like quasi_total )
Function of ( ( ) (
V67()
V68()
V69() )
set ) , ( ( ) ( )
set ) ) is
being_homeomorphism ) ) ) & (
U : ( ( ) ( )
Subset of )
= CircleMap : ( (
Function-like quasi_total ) ( non
empty V16()
V19( the
carrier of
R^1 : ( (
V303() ) ( non
empty strict TopSpace-like V299()
V303() )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V299() )
TopStruct ) ) : ( ( ) ( non
empty V67()
V68()
V69() )
set ) )
V20( the
carrier of
(Tunit_circle 2 : ( ( ) ( non empty ordinal natural complex real ext-real positive non negative integer V66() V67() V68() V69() V70() V71() V72() ) Element of NAT : ( ( ) ( V67() V68() V69() V70() V71() V72() V73() non with_non-empty_elements ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( non
empty TopSpace-like compact V221()
V222()
V266()
pathwise_connected being_simple_closed_curve )
SubSpace of
TOP-REAL 2 : ( ( ) ( non
empty ordinal natural complex real ext-real positive non
negative integer V66()
V67()
V68()
V69()
V70()
V71()
V72() )
Element of
NAT : ( ( ) (
V67()
V68()
V69()
V70()
V71()
V72()
V73() non
with_non-empty_elements )
Element of
K6(
REAL : ( ( ) ( non
empty V27()
V67()
V68()
V69()
V73() non
with_non-empty_elements )
set ) ) : ( ( ) ( non
empty )
set ) ) ) : ( (
V254() ) ( non
empty TopSpace-like T_0 T_1 T_2 V136()
V161()
V162()
V163()
V164()
V165()
V166()
V167()
V221()
V222()
V254() )
L19()) ) : ( ( ) ( non
empty )
set ) )
Function-like total quasi_total onto continuous )
Function of ( ( ) ( non
empty V67()
V68()
V69() )
set ) , ( ( ) ( non
empty )
set ) )
.: ].(1 : ( ( ) ( non empty ordinal natural complex real ext-real positive non negative integer V66() V67() V68() V69() V70() V71() V72() ) Element of NAT : ( ( ) ( V67() V68() V69() V70() V71() V72() V73() non with_non-empty_elements ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) / 2 : ( ( ) ( non empty ordinal natural complex real ext-real positive non negative integer V66() V67() V68() V69() V70() V71() V72() ) Element of NAT : ( ( ) ( V67() V68() V69() V70() V71() V72() V73() non with_non-empty_elements ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( non empty complex real ext-real positive non negative ) Element of REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) ,(3 : ( ( ) ( non empty ordinal natural complex real ext-real positive non negative integer V66() V67() V68() V69() V70() V71() V72() ) Element of NAT : ( ( ) ( V67() V68() V69() V70() V71() V72() V73() non with_non-empty_elements ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) / 2 : ( ( ) ( non empty ordinal natural complex real ext-real positive non negative integer V66() V67() V68() V69() V70() V71() V72() ) Element of NAT : ( ( ) ( V67() V68() V69() V70() V71() V72() V73() non with_non-empty_elements ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( non empty complex real ext-real positive non negative ) Element of REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) .[ : ( ( ) ( non
empty open V67()
V68()
V69() )
Element of
K6(
REAL : ( ( ) ( non
empty V27()
V67()
V68()
V69()
V73() non
with_non-empty_elements )
set ) ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
Element of
K6( the
carrier of
(Tunit_circle 2 : ( ( ) ( non empty ordinal natural complex real ext-real positive non negative integer V66() V67() V68() V69() V70() V71() V72() ) Element of NAT : ( ( ) ( V67() V68() V69() V70() V71() V72() V73() non with_non-empty_elements ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( non
empty TopSpace-like compact V221()
V222()
V266()
pathwise_connected being_simple_closed_curve )
SubSpace of
TOP-REAL 2 : ( ( ) ( non
empty ordinal natural complex real ext-real positive non
negative integer V66()
V67()
V68()
V69()
V70()
V71()
V72() )
Element of
NAT : ( ( ) (
V67()
V68()
V69()
V70()
V71()
V72()
V73() non
with_non-empty_elements )
Element of
K6(
REAL : ( ( ) ( non
empty V27()
V67()
V68()
V69()
V73() non
with_non-empty_elements )
set ) ) : ( ( ) ( non
empty )
set ) ) ) : ( (
V254() ) ( non
empty TopSpace-like T_0 T_1 T_2 V136()
V161()
V162()
V163()
V164()
V165()
V166()
V167()
V221()
V222()
V254() )
L19()) ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) ) implies (
union (IntIntervals ((1 : ( ( ) ( non empty ordinal natural complex real ext-real positive non negative integer V66() V67() V68() V69() V70() V71() V72() ) Element of NAT : ( ( ) ( V67() V68() V69() V70() V71() V72() V73() non with_non-empty_elements ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) / 2 : ( ( ) ( non empty ordinal natural complex real ext-real positive non negative integer V66() V67() V68() V69() V70() V71() V72() ) Element of NAT : ( ( ) ( V67() V68() V69() V70() V71() V72() V73() non with_non-empty_elements ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( non empty complex real ext-real positive non negative ) Element of REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) ,(3 : ( ( ) ( non empty ordinal natural complex real ext-real positive non negative integer V66() V67() V68() V69() V70() V71() V72() ) Element of NAT : ( ( ) ( V67() V68() V69() V70() V71() V72() V73() non with_non-empty_elements ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) / 2 : ( ( ) ( non empty ordinal natural complex real ext-real positive non negative integer V66() V67() V68() V69() V70() V71() V72() ) Element of NAT : ( ( ) ( V67() V68() V69() V70() V71() V72() V73() non with_non-empty_elements ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( non empty complex real ext-real positive non negative ) Element of REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) )) : ( (
open ) ( non
empty open )
Subset-Family of ) : ( ( ) (
V67()
V68()
V69() )
Element of
K6( the
carrier of
R^1 : ( (
V303() ) ( non
empty strict TopSpace-like V299()
V303() )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V299() )
TopStruct ) ) : ( ( ) ( non
empty V67()
V68()
V69() )
set ) ) : ( ( ) ( non
empty )
set ) )
= CircleMap : ( (
Function-like quasi_total ) ( non
empty V16()
V19( the
carrier of
R^1 : ( (
V303() ) ( non
empty strict TopSpace-like V299()
V303() )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V299() )
TopStruct ) ) : ( ( ) ( non
empty V67()
V68()
V69() )
set ) )
V20( the
carrier of
(Tunit_circle 2 : ( ( ) ( non empty ordinal natural complex real ext-real positive non negative integer V66() V67() V68() V69() V70() V71() V72() ) Element of NAT : ( ( ) ( V67() V68() V69() V70() V71() V72() V73() non with_non-empty_elements ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( non
empty TopSpace-like compact V221()
V222()
V266()
pathwise_connected being_simple_closed_curve )
SubSpace of
TOP-REAL 2 : ( ( ) ( non
empty ordinal natural complex real ext-real positive non
negative integer V66()
V67()
V68()
V69()
V70()
V71()
V72() )
Element of
NAT : ( ( ) (
V67()
V68()
V69()
V70()
V71()
V72()
V73() non
with_non-empty_elements )
Element of
K6(
REAL : ( ( ) ( non
empty V27()
V67()
V68()
V69()
V73() non
with_non-empty_elements )
set ) ) : ( ( ) ( non
empty )
set ) ) ) : ( (
V254() ) ( non
empty TopSpace-like T_0 T_1 T_2 V136()
V161()
V162()
V163()
V164()
V165()
V166()
V167()
V221()
V222()
V254() )
L19()) ) : ( ( ) ( non
empty )
set ) )
Function-like total quasi_total onto continuous )
Function of ( ( ) ( non
empty V67()
V68()
V69() )
set ) , ( ( ) ( non
empty )
set ) )
" U : ( ( ) ( )
Subset of ) : ( ( ) (
V67()
V68()
V69() )
Element of
K6( the
carrier of
R^1 : ( (
V303() ) ( non
empty strict TopSpace-like V299()
V303() )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V299() )
TopStruct ) ) : ( ( ) ( non
empty V67()
V68()
V69() )
set ) ) : ( ( ) ( non
empty )
set ) ) & ( for
d being ( ( ) (
V67()
V68()
V69() )
Subset of ) st
d : ( ( ) (
V67()
V68()
V69() )
Subset of )
in IntIntervals (
(1 : ( ( ) ( non empty ordinal natural complex real ext-real positive non negative integer V66() V67() V68() V69() V70() V71() V72() ) Element of NAT : ( ( ) ( V67() V68() V69() V70() V71() V72() V73() non with_non-empty_elements ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) / 2 : ( ( ) ( non empty ordinal natural complex real ext-real positive non negative integer V66() V67() V68() V69() V70() V71() V72() ) Element of NAT : ( ( ) ( V67() V68() V69() V70() V71() V72() V73() non with_non-empty_elements ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( non
empty complex real ext-real positive non
negative )
Element of
REAL : ( ( ) ( non
empty V27()
V67()
V68()
V69()
V73() non
with_non-empty_elements )
set ) ) ,
(3 : ( ( ) ( non empty ordinal natural complex real ext-real positive non negative integer V66() V67() V68() V69() V70() V71() V72() ) Element of NAT : ( ( ) ( V67() V68() V69() V70() V71() V72() V73() non with_non-empty_elements ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) / 2 : ( ( ) ( non empty ordinal natural complex real ext-real positive non negative integer V66() V67() V68() V69() V70() V71() V72() ) Element of NAT : ( ( ) ( V67() V68() V69() V70() V71() V72() V73() non with_non-empty_elements ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( non
empty complex real ext-real positive non
negative )
Element of
REAL : ( ( ) ( non
empty V27()
V67()
V68()
V69()
V73() non
with_non-empty_elements )
set ) ) ) : ( (
open ) ( non
empty open )
Subset-Family of ) holds
for
f being ( (
Function-like quasi_total ) (
V16()
V19( the
carrier of
(R^1 : ( ( V303() ) ( non empty strict TopSpace-like V299() V303() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V299() ) TopStruct ) ) | b3 : ( ( ) ( V67() V68() V69() ) Subset of ) ) : ( (
strict ) (
strict TopSpace-like V299() )
SubSpace of
R^1 : ( (
V303() ) ( non
empty strict TopSpace-like V299()
V303() )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V299() )
TopStruct ) ) ) : ( ( ) (
V67()
V68()
V69() )
set ) )
V20( the
carrier of
((Tunit_circle 2 : ( ( ) ( non empty ordinal natural complex real ext-real positive non negative integer V66() V67() V68() V69() V70() V71() V72() ) Element of NAT : ( ( ) ( V67() V68() V69() V70() V71() V72() V73() non with_non-empty_elements ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( non empty TopSpace-like compact V221() V222() V266() pathwise_connected being_simple_closed_curve ) SubSpace of TOP-REAL 2 : ( ( ) ( non empty ordinal natural complex real ext-real positive non negative integer V66() V67() V68() V69() V70() V71() V72() ) Element of NAT : ( ( ) ( V67() V68() V69() V70() V71() V72() V73() non with_non-empty_elements ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( V254() ) ( non empty TopSpace-like T_0 T_1 T_2 V136() V161() V162() V163() V164() V165() V166() V167() V221() V222() V254() ) L19()) ) | b2 : ( ( ) ( ) Subset of ) ) : ( (
strict ) (
strict TopSpace-like V221()
V222() )
SubSpace of
Tunit_circle 2 : ( ( ) ( non
empty ordinal natural complex real ext-real positive non
negative integer V66()
V67()
V68()
V69()
V70()
V71()
V72() )
Element of
NAT : ( ( ) (
V67()
V68()
V69()
V70()
V71()
V72()
V73() non
with_non-empty_elements )
Element of
K6(
REAL : ( ( ) ( non
empty V27()
V67()
V68()
V69()
V73() non
with_non-empty_elements )
set ) ) : ( ( ) ( non
empty )
set ) ) ) : ( ( ) ( non
empty TopSpace-like compact V221()
V222()
V266()
pathwise_connected being_simple_closed_curve )
SubSpace of
TOP-REAL 2 : ( ( ) ( non
empty ordinal natural complex real ext-real positive non
negative integer V66()
V67()
V68()
V69()
V70()
V71()
V72() )
Element of
NAT : ( ( ) (
V67()
V68()
V69()
V70()
V71()
V72()
V73() non
with_non-empty_elements )
Element of
K6(
REAL : ( ( ) ( non
empty V27()
V67()
V68()
V69()
V73() non
with_non-empty_elements )
set ) ) : ( ( ) ( non
empty )
set ) ) ) : ( (
V254() ) ( non
empty TopSpace-like T_0 T_1 T_2 V136()
V161()
V162()
V163()
V164()
V165()
V166()
V167()
V221()
V222()
V254() )
L19()) ) ) : ( ( ) ( )
set ) )
Function-like quasi_total )
Function of ( ( ) (
V67()
V68()
V69() )
set ) , ( ( ) ( )
set ) ) st
f : ( (
Function-like quasi_total ) (
V16()
V19( the
carrier of
(R^1 : ( ( V303() ) ( non empty strict TopSpace-like V299() V303() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V299() ) TopStruct ) ) | b3 : ( ( ) ( V67() V68() V69() ) Subset of ) ) : ( (
strict ) (
strict TopSpace-like V299() )
SubSpace of
R^1 : ( (
V303() ) ( non
empty strict TopSpace-like V299()
V303() )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V299() )
TopStruct ) ) ) : ( ( ) (
V67()
V68()
V69() )
set ) )
V20( the
carrier of
((Tunit_circle 2 : ( ( ) ( non empty ordinal natural complex real ext-real positive non negative integer V66() V67() V68() V69() V70() V71() V72() ) Element of NAT : ( ( ) ( V67() V68() V69() V70() V71() V72() V73() non with_non-empty_elements ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( non empty TopSpace-like compact V221() V222() V266() pathwise_connected being_simple_closed_curve ) SubSpace of TOP-REAL 2 : ( ( ) ( non empty ordinal natural complex real ext-real positive non negative integer V66() V67() V68() V69() V70() V71() V72() ) Element of NAT : ( ( ) ( V67() V68() V69() V70() V71() V72() V73() non with_non-empty_elements ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( V254() ) ( non empty TopSpace-like T_0 T_1 T_2 V136() V161() V162() V163() V164() V165() V166() V167() V221() V222() V254() ) L19()) ) | b2 : ( ( ) ( ) Subset of ) ) : ( (
strict ) (
strict TopSpace-like V221()
V222() )
SubSpace of
Tunit_circle 2 : ( ( ) ( non
empty ordinal natural complex real ext-real positive non
negative integer V66()
V67()
V68()
V69()
V70()
V71()
V72() )
Element of
NAT : ( ( ) (
V67()
V68()
V69()
V70()
V71()
V72()
V73() non
with_non-empty_elements )
Element of
K6(
REAL : ( ( ) ( non
empty V27()
V67()
V68()
V69()
V73() non
with_non-empty_elements )
set ) ) : ( ( ) ( non
empty )
set ) ) ) : ( ( ) ( non
empty TopSpace-like compact V221()
V222()
V266()
pathwise_connected being_simple_closed_curve )
SubSpace of
TOP-REAL 2 : ( ( ) ( non
empty ordinal natural complex real ext-real positive non
negative integer V66()
V67()
V68()
V69()
V70()
V71()
V72() )
Element of
NAT : ( ( ) (
V67()
V68()
V69()
V70()
V71()
V72()
V73() non
with_non-empty_elements )
Element of
K6(
REAL : ( ( ) ( non
empty V27()
V67()
V68()
V69()
V73() non
with_non-empty_elements )
set ) ) : ( ( ) ( non
empty )
set ) ) ) : ( (
V254() ) ( non
empty TopSpace-like T_0 T_1 T_2 V136()
V161()
V162()
V163()
V164()
V165()
V166()
V167()
V221()
V222()
V254() )
L19()) ) ) : ( ( ) ( )
set ) )
Function-like quasi_total )
Function of ( ( ) (
V67()
V68()
V69() )
set ) , ( ( ) ( )
set ) )
= CircleMap : ( (
Function-like quasi_total ) ( non
empty V16()
V19( the
carrier of
R^1 : ( (
V303() ) ( non
empty strict TopSpace-like V299()
V303() )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V299() )
TopStruct ) ) : ( ( ) ( non
empty V67()
V68()
V69() )
set ) )
V20( the
carrier of
(Tunit_circle 2 : ( ( ) ( non empty ordinal natural complex real ext-real positive non negative integer V66() V67() V68() V69() V70() V71() V72() ) Element of NAT : ( ( ) ( V67() V68() V69() V70() V71() V72() V73() non with_non-empty_elements ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( non
empty TopSpace-like compact V221()
V222()
V266()
pathwise_connected being_simple_closed_curve )
SubSpace of
TOP-REAL 2 : ( ( ) ( non
empty ordinal natural complex real ext-real positive non
negative integer V66()
V67()
V68()
V69()
V70()
V71()
V72() )
Element of
NAT : ( ( ) (
V67()
V68()
V69()
V70()
V71()
V72()
V73() non
with_non-empty_elements )
Element of
K6(
REAL : ( ( ) ( non
empty V27()
V67()
V68()
V69()
V73() non
with_non-empty_elements )
set ) ) : ( ( ) ( non
empty )
set ) ) ) : ( (
V254() ) ( non
empty TopSpace-like T_0 T_1 T_2 V136()
V161()
V162()
V163()
V164()
V165()
V166()
V167()
V221()
V222()
V254() )
L19()) ) : ( ( ) ( non
empty )
set ) )
Function-like total quasi_total onto continuous )
Function of ( ( ) ( non
empty V67()
V68()
V69() )
set ) , ( ( ) ( non
empty )
set ) )
| d : ( ( ) (
V67()
V68()
V69() )
Subset of ) : ( (
Function-like ) (
V16()
V19( the
carrier of
R^1 : ( (
V303() ) ( non
empty strict TopSpace-like V299()
V303() )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V299() )
TopStruct ) ) : ( ( ) ( non
empty V67()
V68()
V69() )
set ) )
V20( the
carrier of
(Tunit_circle 2 : ( ( ) ( non empty ordinal natural complex real ext-real positive non negative integer V66() V67() V68() V69() V70() V71() V72() ) Element of NAT : ( ( ) ( V67() V68() V69() V70() V71() V72() V73() non with_non-empty_elements ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( non
empty TopSpace-like compact V221()
V222()
V266()
pathwise_connected being_simple_closed_curve )
SubSpace of
TOP-REAL 2 : ( ( ) ( non
empty ordinal natural complex real ext-real positive non
negative integer V66()
V67()
V68()
V69()
V70()
V71()
V72() )
Element of
NAT : ( ( ) (
V67()
V68()
V69()
V70()
V71()
V72()
V73() non
with_non-empty_elements )
Element of
K6(
REAL : ( ( ) ( non
empty V27()
V67()
V68()
V69()
V73() non
with_non-empty_elements )
set ) ) : ( ( ) ( non
empty )
set ) ) ) : ( (
V254() ) ( non
empty TopSpace-like T_0 T_1 T_2 V136()
V161()
V162()
V163()
V164()
V165()
V166()
V167()
V221()
V222()
V254() )
L19()) ) : ( ( ) ( non
empty )
set ) )
Function-like )
Element of
K6(
K7( the
carrier of
R^1 : ( (
V303() ) ( non
empty strict TopSpace-like V299()
V303() )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V299() )
TopStruct ) ) : ( ( ) ( non
empty V67()
V68()
V69() )
set ) , the
carrier of
(Tunit_circle 2 : ( ( ) ( non empty ordinal natural complex real ext-real positive non negative integer V66() V67() V68() V69() V70() V71() V72() ) Element of NAT : ( ( ) ( V67() V68() V69() V70() V71() V72() V73() non with_non-empty_elements ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( non
empty TopSpace-like compact V221()
V222()
V266()
pathwise_connected being_simple_closed_curve )
SubSpace of
TOP-REAL 2 : ( ( ) ( non
empty ordinal natural complex real ext-real positive non
negative integer V66()
V67()
V68()
V69()
V70()
V71()
V72() )
Element of
NAT : ( ( ) (
V67()
V68()
V69()
V70()
V71()
V72()
V73() non
with_non-empty_elements )
Element of
K6(
REAL : ( ( ) ( non
empty V27()
V67()
V68()
V69()
V73() non
with_non-empty_elements )
set ) ) : ( ( ) ( non
empty )
set ) ) ) : ( (
V254() ) ( non
empty TopSpace-like T_0 T_1 T_2 V136()
V161()
V162()
V163()
V164()
V165()
V166()
V167()
V221()
V222()
V254() )
L19()) ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) ) holds
f : ( (
Function-like quasi_total ) (
V16()
V19( the
carrier of
(R^1 : ( ( V303() ) ( non empty strict TopSpace-like V299() V303() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V299() ) TopStruct ) ) | b3 : ( ( ) ( V67() V68() V69() ) Subset of ) ) : ( (
strict ) (
strict TopSpace-like V299() )
SubSpace of
R^1 : ( (
V303() ) ( non
empty strict TopSpace-like V299()
V303() )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V299() )
TopStruct ) ) ) : ( ( ) (
V67()
V68()
V69() )
set ) )
V20( the
carrier of
((Tunit_circle 2 : ( ( ) ( non empty ordinal natural complex real ext-real positive non negative integer V66() V67() V68() V69() V70() V71() V72() ) Element of NAT : ( ( ) ( V67() V68() V69() V70() V71() V72() V73() non with_non-empty_elements ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( non empty TopSpace-like compact V221() V222() V266() pathwise_connected being_simple_closed_curve ) SubSpace of TOP-REAL 2 : ( ( ) ( non empty ordinal natural complex real ext-real positive non negative integer V66() V67() V68() V69() V70() V71() V72() ) Element of NAT : ( ( ) ( V67() V68() V69() V70() V71() V72() V73() non with_non-empty_elements ) Element of K6(REAL : ( ( ) ( non empty V27() V67() V68() V69() V73() non with_non-empty_elements ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( V254() ) ( non empty TopSpace-like T_0 T_1 T_2 V136() V161() V162() V163() V164() V165() V166() V167() V221() V222() V254() ) L19()) ) | b2 : ( ( ) ( ) Subset of ) ) : ( (
strict ) (
strict TopSpace-like V221()
V222() )
SubSpace of
Tunit_circle 2 : ( ( ) ( non
empty ordinal natural complex real ext-real positive non
negative integer V66()
V67()
V68()
V69()
V70()
V71()
V72() )
Element of
NAT : ( ( ) (
V67()
V68()
V69()
V70()
V71()
V72()
V73() non
with_non-empty_elements )
Element of
K6(
REAL : ( ( ) ( non
empty V27()
V67()
V68()
V69()
V73() non
with_non-empty_elements )
set ) ) : ( ( ) ( non
empty )
set ) ) ) : ( ( ) ( non
empty TopSpace-like compact V221()
V222()
V266()
pathwise_connected being_simple_closed_curve )
SubSpace of
TOP-REAL 2 : ( ( ) ( non
empty ordinal natural complex real ext-real positive non
negative integer V66()
V67()
V68()
V69()
V70()
V71()
V72() )
Element of
NAT : ( ( ) (
V67()
V68()
V69()
V70()
V71()
V72()
V73() non
with_non-empty_elements )
Element of
K6(
REAL : ( ( ) ( non
empty V27()
V67()
V68()
V69()
V73() non
with_non-empty_elements )
set ) ) : ( ( ) ( non
empty )
set ) ) ) : ( (
V254() ) ( non
empty TopSpace-like T_0 T_1 T_2 V136()
V161()
V162()
V163()
V164()
V165()
V166()
V167()
V221()
V222()
V254() )
L19()) ) ) : ( ( ) ( )
set ) )
Function-like quasi_total )
Function of ( ( ) (
V67()
V68()
V69() )
set ) , ( ( ) ( )
set ) ) is
being_homeomorphism ) ) ) ) ) ) ;