:: TOPREALB semantic presentation

REAL is non empty V27() V67() V68() V69() V73() non with_non-empty_elements set

NAT is V67() V68() V69() V70() V71() V72() V73() non with_non-empty_elements Element of K6(REAL)

K6(REAL) is non empty set

K744() is non empty strict TopSpace-like V299() SubSpace of R^1

R^1 is non empty strict TopSpace-like V299() TopStruct

the carrier of K744() is non empty V67() V68() V69() set

COMPLEX is non empty V27() V67() V73() set

omega is V67() V68() V69() V70() V71() V72() V73() non with_non-empty_elements set

K6(omega) is non empty set

K7(REAL,REAL) is non empty V51() V52() V53() set

K6(K7(REAL,REAL)) is non empty set

K6(NAT) is non empty set

RAT is non empty V27() V67() V68() V69() V70() V73() set

INT is non empty V27() V67() V68() V69() V70() V71() V73() set

K7(NAT,REAL) is V51() V52() V53() set

K6(K7(NAT,REAL)) is non empty set

K7(NAT,COMPLEX) is V51() set

K6(K7(NAT,COMPLEX)) is non empty set

K7(COMPLEX,COMPLEX) is non empty V51() set

K6(K7(COMPLEX,COMPLEX)) is non empty set

{} is empty trivial Function-like functional V67() V68() V69() V70() V71() V72() V73() set

the empty trivial Function-like functional V67() V68() V69() V70() V71() V72() V73() set is empty trivial Function-like functional V67() V68() V69() V70() V71() V72() V73() set

1 is non empty ordinal natural complex real ext-real positive non negative integer V66() V67() V68() V69() V70() V71() V72() Element of NAT

{{},1} is non empty set

K562() is non empty V138() L9()

the carrier of K562() is non empty set

K567() is non empty V138() V201() V202() V203() V205() V231() V232() V233() V234() V235() V236() L9()

K568() is non empty V138() V203() V205() V234() V235() V236() M31(K567())

K569() is non empty V138() V201() V203() V205() V234() V235() V236() V237() M34(K567(),K568())

K571() is non empty V138() V201() V203() V205() L9()

K572() is non empty V138() V201() V203() V205() V237() M31(K571())

K7(1,1) is non empty V20( RAT ) V20( INT ) V51() V52() V53() V54() set

K6(K7(1,1)) is non empty set

K7(K7(1,1),1) is non empty V20( RAT ) V20( INT ) V51() V52() V53() V54() set

K6(K7(K7(1,1),1)) is non empty set

K7(K7(1,1),REAL) is non empty V51() V52() V53() set

K6(K7(K7(1,1),REAL)) is non empty set

K7(K7(REAL,REAL),REAL) is non empty V51() V52() V53() set

K6(K7(K7(REAL,REAL),REAL)) is non empty set

2 is non empty ordinal natural complex real ext-real positive non negative integer V66() V67() V68() V69() V70() V71() V72() Element of NAT

K7(2,2) is non empty V20( RAT ) V20( INT ) V51() V52() V53() V54() set

K7(K7(2,2),REAL) is non empty V51() V52() V53() set

K6(K7(K7(2,2),REAL)) is non empty set

TOP-REAL 2 is non empty TopSpace-like T_0 T_1 T_2 V136() V161() V162() V163() V164() V165() V166() V167() V221() V222() V254() L19()

the carrier of (TOP-REAL 2) is non empty functional set

K6( the carrier of (TOP-REAL 2)) is non empty set

K7( the carrier of (TOP-REAL 2),REAL) is non empty V51() V52() V53() set

K6(K7( the carrier of (TOP-REAL 2),REAL)) is non empty set

K737() is non empty strict TopSpace-like V299() TopStruct

the carrier of K737() is non empty V67() V68() V69() set

RealSpace is strict V299() MetrStruct

[:K744(),K744():] is non empty strict TopSpace-like TopStruct

the carrier of [:K744(),K744():] is non empty set

[:R^1,R^1:] is non empty strict TopSpace-like TopStruct

the carrier of [:R^1,R^1:] is non empty set

K7( the carrier of [:R^1,R^1:], the carrier of (TOP-REAL 2)) is non empty set

K6(K7( the carrier of [:R^1,R^1:], the carrier of (TOP-REAL 2))) is non empty set

K7(K7(COMPLEX,COMPLEX),COMPLEX) is non empty V51() set

K6(K7(K7(COMPLEX,COMPLEX),COMPLEX)) is non empty set

K7(RAT,RAT) is non empty V20( RAT ) V51() V52() V53() set

K6(K7(RAT,RAT)) is non empty set

K7(K7(RAT,RAT),RAT) is non empty V20( RAT ) V51() V52() V53() set

K6(K7(K7(RAT,RAT),RAT)) is non empty set

K7(INT,INT) is non empty V20( RAT ) V20( INT ) V51() V52() V53() set

K6(K7(INT,INT)) is non empty set

K7(K7(INT,INT),INT) is non empty V20( RAT ) V20( INT ) V51() V52() V53() set

K6(K7(K7(INT,INT),INT)) is non empty set

K7(NAT,NAT) is V20( RAT ) V20( INT ) V51() V52() V53() V54() set

K7(K7(NAT,NAT),NAT) is V20( RAT ) V20( INT ) V51() V52() V53() V54() set

K6(K7(K7(NAT,NAT),NAT)) is non empty set

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

sin is non empty V16() V19( REAL ) V20( REAL ) Function-like total quasi_total continuous V51() V52() V53() Element of K6(K7(REAL,REAL))

cos is non empty V16() V19( REAL ) V20( REAL ) Function-like total quasi_total continuous V51() V52() V53() Element of K6(K7(REAL,REAL))

dom sin is V67() V68() V69() Element of K6(REAL)

dom cos is V67() V68() V69() Element of K6(REAL)

cos 0 is complex real ext-real Element of REAL

sin 0 is complex real ext-real Element of REAL

PI is non empty complex real ext-real positive non negative Element of REAL

PI / 2 is non empty complex real ext-real positive non negative Element of REAL

cos (PI / 2) is complex real ext-real Element of REAL

sin (PI / 2) is complex real ext-real Element of REAL

cos PI is complex real ext-real Element of REAL

- 1 is non empty complex real ext-real non positive negative integer Element of REAL

sin PI is complex real ext-real Element of REAL

PI + (PI / 2) is non empty complex real ext-real positive non negative Element of REAL

cos (PI + (PI / 2)) is complex real ext-real Element of REAL

sin (PI + (PI / 2)) is complex real ext-real Element of REAL

2 * PI is non empty complex real ext-real positive non negative Element of REAL

cos (2 * PI) is complex real ext-real Element of REAL

sin (2 * PI) is complex real ext-real Element of REAL

0. (TOP-REAL 2) is V16() Function-like V34(2) V51() V52() V53() FinSequence-like zero Element of the carrier of (TOP-REAL 2)

the ZeroF of (TOP-REAL 2) is V16() Function-like V34(2) V51() V52() V53() FinSequence-like Element of the carrier of (TOP-REAL 2)

|[0,0]| is V16() Function-like V34(2) V51() V52() V53() FinSequence-like Element of the carrier of (TOP-REAL 2)

sqrt 1 is complex real ext-real Element of REAL

sqrt 2 is complex real ext-real Element of REAL

- 1 is non empty complex real ext-real non positive negative integer set

Euclid 2 is non empty strict Reflexive discerning V245() triangle MetrStruct

the carrier of (Euclid 2) is non empty set

the carrier of R^1 is non empty V67() V68() V69() set

I(01) is strict TopSpace-like V299() SubSpace of K744()

K6( the carrier of R^1) is non empty set

K7( the carrier of R^1, the carrier of R^1) is non empty V51() V52() V53() set

K6(K7( the carrier of R^1, the carrier of R^1)) is non empty set

[.0,PI.] is non empty closed V67() V68() V69() Element of K6(REAL)

].PI,(2 * PI).[ is open V67() V68() V69() Element of K6(REAL)

- (PI / 2) is non empty complex real ext-real non positive negative Element of REAL

[.(- (PI / 2)),(PI / 2).] is non empty closed V67() V68() V69() Element of K6(REAL)

3 is non empty ordinal natural complex real ext-real positive non negative integer V66() V67() V68() V69() V70() V71() V72() Element of NAT

3 / 2 is non empty complex real ext-real positive non negative Element of REAL

(3 / 2) * PI is non empty complex real ext-real positive non negative Element of REAL

].(PI / 2),((3 / 2) * PI).[ is open V67() V68() V69() Element of K6(REAL)

[.(PI / 2),((3 / 2) * PI).] is closed V67() V68() V69() Element of K6(REAL)

].((3 / 2) * PI),(2 * PI).[ is open V67() V68() V69() Element of K6(REAL)

rng sin is V67() V68() V69() set

[.(- 1),1.] is non empty closed V67() V68() V69() Element of K6(REAL)

rng cos is V67() V68() V69() set

R^2-unit_square is non empty functional compact being_simple_closed_curve Element of K6( the carrier of (TOP-REAL 2))

(TOP-REAL 2) | R^2-unit_square is non empty strict TopSpace-like compact V221() V222() V266() SubSpace of TOP-REAL 2

the carrier of ((TOP-REAL 2) | R^2-unit_square) is non empty set

arcsin is V16() V19( REAL ) V20( REAL ) Function-like one-to-one V51() V52() V53() Element of K6(K7(REAL,REAL))

dom arcsin is V67() V68() V69() Element of K6(REAL)

arcsin | [.(- 1),1.] is V16() V19( REAL ) V20( REAL ) Function-like V51() V52() V53() Element of K6(K7(REAL,REAL))

arccos is V16() V19( REAL ) V20( REAL ) Function-like one-to-one V51() V52() V53() Element of K6(K7(REAL,REAL))

rng arccos is V67() V68() V69() Element of K6(REAL)

dom arccos is V67() V68() V69() Element of K6(REAL)

arccos (- 1) is complex real ext-real Element of REAL

arccos 1 is complex real ext-real Element of REAL

arccos | [.(- 1),1.] is V16() V19( REAL ) V20( REAL ) Function-like V51() V52() V53() Element of K6(K7(REAL,REAL))

proj1 is non empty V16() V19( the carrier of (TOP-REAL 2)) V20( REAL ) Function-like total quasi_total V51() V52() V53() continuous Element of K6(K7( the carrier of (TOP-REAL 2),REAL))

R^1 is non empty strict TopSpace-like V299() V303() SubSpace of R^1

the carrier of R^1 is non empty V67() V68() V69() set

Closed-Interval-TSpace ((- 1),1) is non empty strict TopSpace-like V299() SubSpace of R^1

the carrier of (Closed-Interval-TSpace ((- 1),1)) is non empty V67() V68() V69() set

1 - 0 is non empty complex real ext-real positive non negative integer Element of REAL

1 / 2 is non empty complex real ext-real positive non negative Element of REAL

(3 / 2) - (1 / 2) is complex real ext-real Element of REAL

].0,1.[ is non empty open V67() V68() V69() Element of K6(REAL)

].(1 / 2),(3 / 2).[ is open V67() V68() V69() Element of K6(REAL)

p1 is non empty complex real ext-real positive non negative set

(1 / 2) + p1 is non empty complex real ext-real positive non negative Element of REAL

].(1 / 2),((1 / 2) + p1).[ is non empty open V67() V68() V69() Element of K6(REAL)

PI / 1 is non empty complex real ext-real positive non negative Element of REAL

1 * PI is non empty complex real ext-real positive non negative Element of REAL

A is non empty TopSpace-like TopStruct

the carrier of A is non empty set

TUC is non empty TopSpace-like SubSpace of A

cS1 is non empty TopSpace-like SubSpace of TUC

the carrier of cS1 is non empty set

TREC is Element of the carrier of cS1

the carrier of TUC is non empty set

A is TopSpace-like TopStruct

the carrier of A is set

K6( the carrier of A) is non empty set

TUC is TopSpace-like SubSpace of A

cS1 is TopSpace-like SubSpace of TUC

the carrier of cS1 is set

K6( the carrier of cS1) is non empty set

TREC is Element of K6( the carrier of cS1)

the carrier of TUC is set

K6( the carrier of TUC) is non empty set

A is complex real ext-real set

TUC is complex real ext-real set

A * TUC is complex real ext-real set

cS1 is complex real ext-real set

(A * TUC) + cS1 is complex real ext-real set

sin ((A * TUC) + cS1) is complex real ext-real set

AffineMap (A,cS1) is non empty V16() V19( REAL ) V20( REAL ) Function-like total quasi_total continuous V51() V52() V53() Element of K6(K7(REAL,REAL))

sin * (AffineMap (A,cS1)) is non empty V16() V19( REAL ) V20( REAL ) Function-like total quasi_total continuous V51() V52() V53() Element of K6(K7(REAL,REAL))

(sin * (AffineMap (A,cS1))) . TUC is complex real ext-real set

sin . ((A * TUC) + cS1) is complex real ext-real set

(AffineMap (A,cS1)) . TUC is complex real ext-real set

sin . ((AffineMap (A,cS1)) . TUC) is complex real ext-real set

A is complex real ext-real set

TUC is complex real ext-real set

A * TUC is complex real ext-real set

cS1 is complex real ext-real set

(A * TUC) + cS1 is complex real ext-real set

cos ((A * TUC) + cS1) is complex real ext-real set

AffineMap (A,cS1) is non empty V16() V19( REAL ) V20( REAL ) Function-like total quasi_total continuous V51() V52() V53() Element of K6(K7(REAL,REAL))

cos * (AffineMap (A,cS1)) is non empty V16() V19( REAL ) V20( REAL ) Function-like total quasi_total continuous V51() V52() V53() Element of K6(K7(REAL,REAL))

(cos * (AffineMap (A,cS1))) . TUC is complex real ext-real set

cos . ((A * TUC) + cS1) is complex real ext-real set

(AffineMap (A,cS1)) . TUC is complex real ext-real set

cos . ((AffineMap (A,cS1)) . TUC) is complex real ext-real set

A is non empty complex real ext-real set

TUC is complex real ext-real set

AffineMap (A,TUC) is non empty V16() V19( REAL ) V20( REAL ) Function-like total quasi_total continuous V51() V52() V53() Element of K6(K7(REAL,REAL))

rng (AffineMap (A,TUC)) is V67() V68() V69() Element of K6(REAL)

A is complex real ext-real set

TUC is complex real ext-real set

{ ].(A + b

cS1 is set

A is complex real ext-real set

TUC is complex real ext-real set

(A,TUC) is set

{ ].(A + b

TOUCm is set

TREC is complex real ext-real set

X is complex real ext-real integer V66() Element of INT

TREC + X is complex real ext-real set

TOUC is complex real ext-real set

TOUC + X is complex real ext-real set

].(TREC + X),(TOUC + X).[ is open V67() V68() V69() Element of K6(REAL)

(TREC,TOUC) is set

{ ].(TREC + b

A is complex real ext-real set

TUC is complex real ext-real set

(A,TUC) is set

{ ].(A + b

A + 0 is complex real ext-real Element of REAL

TUC + 0 is complex real ext-real Element of REAL

].(A + 0),(TUC + 0).[ is open V67() V68() V69() Element of K6(REAL)

A is complex real ext-real set

TUC is complex real ext-real set

A - TUC is complex real ext-real set

(TUC,A) is non empty set

{ ].(TUC + b

TUC + 1 is complex real ext-real Element of REAL

(TUC + 1) + 0 is complex real ext-real Element of REAL

cS1 is ordinal natural complex real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() Element of NAT

(TUC + 1) + cS1 is complex real ext-real Element of REAL

(A - TUC) + TUC is complex real ext-real set

1 + TUC is complex real ext-real Element of REAL

cS1 + 1 is non empty ordinal natural complex real ext-real positive non negative integer Element of REAL

TUC + (cS1 + 1) is complex real ext-real Element of REAL

cS1 is set

TREC is set

TOUC is complex real ext-real integer V66() Element of INT

TUC + TOUC is complex real ext-real set

A + TOUC is complex real ext-real set

].(TUC + TOUC),(A + TOUC).[ is open V67() V68() V69() Element of K6(REAL)

TOUCm is complex real ext-real integer V66() Element of INT

TUC + TOUCm is complex real ext-real set

A + TOUCm is complex real ext-real set

].(TUC + TOUCm),(A + TOUCm).[ is open V67() V68() V69() Element of K6(REAL)

X is set

Xm is complex real ext-real Element of REAL

TOUC + 1 is complex real ext-real integer Element of REAL

TOUCm - (TOUC + 1) is complex real ext-real integer Element of REAL

(TUC + TOUC) + 1 is complex real ext-real Element of REAL

Y is ordinal natural complex real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() Element of NAT

((TUC + TOUC) + 1) + Y is complex real ext-real Element of REAL

(A + TOUC) - TOUC is complex real ext-real set

Y + 1 is non empty ordinal natural complex real ext-real positive non negative integer Element of REAL

(TUC + TOUC) + (Y + 1) is complex real ext-real Element of REAL

((TUC + TOUC) + (Y + 1)) - TOUC is complex real ext-real Element of REAL

TUC + (Y + 1) is complex real ext-real Element of REAL

TOUCm + 1 is complex real ext-real integer Element of REAL

TOUC - (TOUCm + 1) is complex real ext-real integer Element of REAL

(TUC + TOUCm) + 1 is complex real ext-real Element of REAL

Y is ordinal natural complex real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() Element of NAT

((TUC + TOUCm) + 1) + Y is complex real ext-real Element of REAL

(A + TOUCm) - TOUCm is complex real ext-real set

Y + 1 is non empty ordinal natural complex real ext-real positive non negative integer Element of REAL

(TUC + TOUCm) + (Y + 1) is complex real ext-real Element of REAL

((TUC + TOUCm) + (Y + 1)) - TOUCm is complex real ext-real Element of REAL

TUC + (Y + 1) is complex real ext-real Element of REAL

A is complex real ext-real set

TUC is complex real ext-real set

(A,TUC) is non empty set

{ ].(A + b

K6( the carrier of R^1) is non empty set

K6(K6( the carrier of R^1)) is non empty set

bool the carrier of R^1 is non empty Element of K6(K6( the carrier of R^1))

cS1 is set

TREC is complex real ext-real integer V66() Element of INT

A + TREC is complex real ext-real set

TUC + TREC is complex real ext-real set

].(A + TREC),(TUC + TREC).[ is open V67() V68() V69() Element of K6(REAL)

A is complex real ext-real set

TUC is complex real ext-real set

(A,TUC) is non empty set

{ ].(A + b

(A,TUC) is non empty Element of K6(K6( the carrier of R^1))

cS1 is V67() V68() V69() Element of K6( the carrier of R^1)

TREC is complex real ext-real integer V66() Element of INT

A + TREC is complex real ext-real set

TUC + TREC is complex real ext-real set

].(A + TREC),(TUC + TREC).[ is open V67() V68() V69() Element of K6(REAL)

A is complex real ext-real set

A is V67() V68() V69() Element of K6(REAL)

A is non empty V67() V68() V69() Element of K6(REAL)

(A) is V67() V68() V69() Element of K6( the carrier of R^1)

A is open V67() V68() V69() Element of K6(REAL)

(A) is V67() V68() V69() Element of K6( the carrier of R^1)

A is closed V67() V68() V69() Element of K6(REAL)

(A) is V67() V68() V69() Element of K6( the carrier of R^1)

A is open V67() V68() V69() Element of K6(REAL)

(A) is V67() V68() V69() open Element of K6( the carrier of R^1)

R^1 | (A) is strict TopSpace-like V299() SubSpace of R^1

TUC is V67() V68() V69() Element of K6( the carrier of R^1)

the carrier of (R^1 | (A)) is V67() V68() V69() set

A is closed V67() V68() V69() Element of K6(REAL)

(A) is V67() V68() V69() closed Element of K6( the carrier of R^1)

R^1 | (A) is strict TopSpace-like V299() SubSpace of R^1

TUC is V67() V68() V69() Element of K6( the carrier of R^1)

the carrier of (R^1 | (A)) is V67() V68() V69() set

A is V16() V19( REAL ) V20( REAL ) Function-like V51() V52() V53() Element of K6(K7(REAL,REAL))

dom A is V67() V68() V69() Element of K6(REAL)

((dom A)) is V67() V68() V69() Element of K6( the carrier of R^1)

R^1 | ((dom A)) is strict TopSpace-like V299() SubSpace of R^1

the carrier of (R^1 | ((dom A))) is V67() V68() V69() set

rng A is V67() V68() V69() Element of K6(REAL)

((rng A)) is V67() V68() V69() Element of K6( the carrier of R^1)

R^1 | ((rng A)) is strict TopSpace-like V299() SubSpace of R^1

the carrier of (R^1 | ((rng A))) is V67() V68() V69() set

K7( the carrier of (R^1 | ((dom A))), the carrier of (R^1 | ((rng A)))) is V51() V52() V53() set

K6(K7( the carrier of (R^1 | ((dom A))), the carrier of (R^1 | ((rng A))))) is non empty set

A is V16() V19( REAL ) V20( REAL ) Function-like V51() V52() V53() Element of K6(K7(REAL,REAL))

rng A is V67() V68() V69() Element of K6(REAL)

((rng A)) is V67() V68() V69() Element of K6( the carrier of R^1)

R^1 | ((rng A)) is strict TopSpace-like V299() SubSpace of R^1

the carrier of (R^1 | ((rng A))) is V67() V68() V69() set

(A) is V16() V19( the carrier of (R^1 | ((dom A)))) V20( the carrier of (R^1 | ((rng A)))) Function-like quasi_total V51() V52() V53() Element of K6(K7( the carrier of (R^1 | ((dom A))), the carrier of (R^1 | ((rng A)))))

dom A is V67() V68() V69() Element of K6(REAL)

((dom A)) is V67() V68() V69() Element of K6( the carrier of R^1)

R^1 | ((dom A)) is strict TopSpace-like V299() SubSpace of R^1

the carrier of (R^1 | ((dom A))) is V67() V68() V69() set

K7( the carrier of (R^1 | ((dom A))), the carrier of (R^1 | ((rng A)))) is V51() V52() V53() set

K6(K7( the carrier of (R^1 | ((dom A))), the carrier of (R^1 | ((rng A))))) is non empty set

rng (A) is V67() V68() V69() Element of K6( the carrier of (R^1 | ((rng A))))

K6( the carrier of (R^1 | ((rng A)))) is non empty set

A is V16() V19( REAL ) V20( REAL ) Function-like one-to-one V51() V52() V53() Element of K6(K7(REAL,REAL))

(A) is V16() V19( the carrier of (R^1 | ((dom A)))) V20( the carrier of (R^1 | ((rng A)))) Function-like quasi_total onto V51() V52() V53() Element of K6(K7( the carrier of (R^1 | ((dom A))), the carrier of (R^1 | ((rng A)))))

dom A is V67() V68() V69() Element of K6(REAL)

((dom A)) is V67() V68() V69() Element of K6( the carrier of R^1)

R^1 | ((dom A)) is strict TopSpace-like V299() SubSpace of R^1

the carrier of (R^1 | ((dom A))) is V67() V68() V69() set

rng A is V67() V68() V69() Element of K6(REAL)

((rng A)) is V67() V68() V69() Element of K6( the carrier of R^1)

R^1 | ((rng A)) is strict TopSpace-like V299() SubSpace of R^1

the carrier of (R^1 | ((rng A))) is V67() V68() V69() set

K7( the carrier of (R^1 | ((dom A))), the carrier of (R^1 | ((rng A)))) is V51() V52() V53() set

K6(K7( the carrier of (R^1 | ((dom A))), the carrier of (R^1 | ((rng A))))) is non empty set

[#] REAL is non empty non proper V67() V68() V69() Element of K6(REAL)

(([#] REAL)) is non empty V67() V68() V69() Element of K6( the carrier of R^1)

R^1 | (([#] REAL)) is non empty strict TopSpace-like V299() SubSpace of R^1

[#] R^1 is non empty non proper V67() V68() V69() open closed dense non boundary Element of K6( the carrier of R^1)

A is V16() V19( REAL ) V20( REAL ) Function-like V51() V52() V53() Element of K6(K7(REAL,REAL))

dom A is V67() V68() V69() Element of K6(REAL)

((dom A)) is V67() V68() V69() Element of K6( the carrier of R^1)

R^1 | ((dom A)) is strict TopSpace-like V299() SubSpace of R^1

[#] R^1 is non empty non proper V67() V68() V69() open closed dense non boundary Element of K6( the carrier of R^1)

A is non empty V16() V19( REAL ) V20( REAL ) Function-like total quasi_total V51() V52() V53() Element of K6(K7(REAL,REAL))

rng A is V67() V68() V69() Element of K6(REAL)

((rng A)) is V67() V68() V69() Element of K6( the carrier of R^1)

R^1 | ((rng A)) is strict TopSpace-like V299() SubSpace of R^1

the carrier of (R^1 | ((rng A))) is V67() V68() V69() set

K7( the carrier of R^1, the carrier of (R^1 | ((rng A)))) is V51() V52() V53() set

K6(K7( the carrier of R^1, the carrier of (R^1 | ((rng A))))) is non empty set

dom A is V67() V68() V69() Element of K6(REAL)

((dom A)) is V67() V68() V69() Element of K6( the carrier of R^1)

R^1 | ((dom A)) is strict TopSpace-like V299() SubSpace of R^1

(A) is V16() V19( the carrier of (R^1 | ((dom A)))) V20( the carrier of (R^1 | ((rng A)))) Function-like quasi_total onto V51() V52() V53() Element of K6(K7( the carrier of (R^1 | ((dom A))), the carrier of (R^1 | ((rng A)))))

the carrier of (R^1 | ((dom A))) is V67() V68() V69() set

K7( the carrier of (R^1 | ((dom A))), the carrier of (R^1 | ((rng A)))) is V51() V52() V53() set

K6(K7( the carrier of (R^1 | ((dom A))), the carrier of (R^1 | ((rng A))))) is non empty set

K7( the carrier of R^1, the carrier of R^1) is non empty V51() V52() V53() set

K6(K7( the carrier of R^1, the carrier of R^1)) is non empty set

A is non empty V16() V19( REAL ) V20( REAL ) Function-like total quasi_total V51() V52() V53() Element of K6(K7(REAL,REAL))

dom A is V67() V68() V69() Element of K6(REAL)

rng A is V67() V68() V69() Element of K6(REAL)

TUC is non empty V67() V68() V69() Element of K6(REAL)

(TUC) is non empty V67() V68() V69() Element of K6( the carrier of R^1)

R^1 | (TUC) is non empty strict TopSpace-like V299() SubSpace of R^1

the carrier of (R^1 | (TUC)) is non empty V67() V68() V69() set

K7( the carrier of R^1, the carrier of (R^1 | (TUC))) is non empty V51() V52() V53() set

K6(K7( the carrier of R^1, the carrier of (R^1 | (TUC)))) is non empty set

(sin) is V16() V19( the carrier of (R^1 | ((dom sin)))) V20( the carrier of (R^1 | ((rng sin)))) Function-like quasi_total onto V51() V52() V53() Element of K6(K7( the carrier of (R^1 | ((dom sin))), the carrier of (R^1 | ((rng sin)))))

((dom sin)) is V67() V68() V69() Element of K6( the carrier of R^1)

R^1 | ((dom sin)) is strict TopSpace-like V299() SubSpace of R^1

the carrier of (R^1 | ((dom sin))) is V67() V68() V69() set

rng sin is V67() V68() V69() Element of K6(REAL)

((rng sin)) is V67() V68() V69() Element of K6( the carrier of R^1)

R^1 | ((rng sin)) is strict TopSpace-like V299() SubSpace of R^1

the carrier of (R^1 | ((rng sin))) is V67() V68() V69() set

K7( the carrier of (R^1 | ((dom sin))), the carrier of (R^1 | ((rng sin)))) is V51() V52() V53() set

K6(K7( the carrier of (R^1 | ((dom sin))), the carrier of (R^1 | ((rng sin))))) is non empty set

(cos) is V16() V19( the carrier of (R^1 | ((dom cos)))) V20( the carrier of (R^1 | ((rng cos)))) Function-like quasi_total onto V51() V52() V53() Element of K6(K7( the carrier of (R^1 | ((dom cos))), the carrier of (R^1 | ((rng cos)))))

((dom cos)) is V67() V68() V69() Element of K6( the carrier of R^1)

R^1 | ((dom cos)) is strict TopSpace-like V299() SubSpace of R^1

the carrier of (R^1 | ((dom cos))) is V67() V68() V69() set

rng cos is V67() V68() V69() Element of K6(REAL)

((rng cos)) is V67() V68() V69() Element of K6( the carrier of R^1)

R^1 | ((rng cos)) is strict TopSpace-like V299() SubSpace of R^1

the carrier of (R^1 | ((rng cos))) is V67() V68() V69() set

K7( the carrier of (R^1 | ((dom cos))), the carrier of (R^1 | ((rng cos)))) is V51() V52() V53() set

K6(K7( the carrier of (R^1 | ((dom cos))), the carrier of (R^1 | ((rng cos))))) is non empty set

A is V16() V19( REAL ) V20( REAL ) Function-like continuous V51() V52() V53() Element of K6(K7(REAL,REAL))

dom A is V67() V68() V69() Element of K6(REAL)

((dom A)) is V67() V68() V69() Element of K6( the carrier of R^1)

R^1 | ((dom A)) is strict TopSpace-like V299() SubSpace of R^1

rng A is V67() V68() V69() Element of K6(REAL)

((rng A)) is V67() V68() V69() Element of K6( the carrier of R^1)

R^1 | ((rng A)) is strict TopSpace-like V299() SubSpace of R^1

(A) is V16() V19( the carrier of (R^1 | ((dom A)))) V20( the carrier of (R^1 | ((rng A)))) Function-like quasi_total onto V51() V52() V53() Element of K6(K7( the carrier of (R^1 | ((dom A))), the carrier of (R^1 | ((rng A)))))

the carrier of (R^1 | ((dom A))) is V67() V68() V69() set

the carrier of (R^1 | ((rng A))) is V67() V68() V69() set

K7( the carrier of (R^1 | ((dom A))), the carrier of (R^1 | ((rng A)))) is V51() V52() V53() set

K6(K7( the carrier of (R^1 | ((dom A))), the carrier of (R^1 | ((rng A))))) is non empty set

cS1 is non empty V67() V68() V69() Element of K6(REAL)

(cS1) is non empty V67() V68() V69() Element of K6( the carrier of R^1)

R^1 | (cS1) is non empty strict TopSpace-like V299() SubSpace of R^1

the carrier of (R^1 | (cS1)) is non empty V67() V68() V69() set

TREC is non empty V67() V68() V69() Element of K6(REAL)

(TREC) is non empty V67() V68() V69() Element of K6( the carrier of R^1)

R^1 | (TREC) is non empty strict TopSpace-like V299() SubSpace of R^1

the carrier of (R^1 | (TREC)) is non empty V67() V68() V69() set

K7( the carrier of (R^1 | (cS1)), the carrier of (R^1 | (TREC))) is non empty V51() V52() V53() set

K6(K7( the carrier of (R^1 | (cS1)), the carrier of (R^1 | (TREC)))) is non empty set

K7( the carrier of (R^1 | (cS1)), the carrier of R^1) is non empty V51() V52() V53() set

K6(K7( the carrier of (R^1 | (cS1)), the carrier of R^1)) is non empty set

TOUC is non empty V16() V19( the carrier of (R^1 | (cS1))) V20( the carrier of (R^1 | (TREC))) Function-like total quasi_total V51() V52() V53() Element of K6(K7( the carrier of (R^1 | (cS1)), the carrier of (R^1 | (TREC))))

TOUCm is non empty V16() V19( the carrier of (R^1 | (cS1))) V20( the carrier of R^1) Function-like total quasi_total V51() V52() V53() Element of K6(K7( the carrier of (R^1 | (cS1)), the carrier of R^1))

X is complex real ext-real Element of the carrier of (R^1 | (cS1))

TOUCm . X is complex real ext-real Element of the carrier of R^1

Xm is non empty V67() V68() V69() a_neighborhood of TOUCm . X

A . X is complex real ext-real set

Y is open V67() V68() V69() Neighbourhood of A . X

A1 is open V67() V68() V69() Neighbourhood of X

A .: A1 is V67() V68() V69() Element of K6(REAL)

C is complex real ext-real set

X - C is complex real ext-real set

X + C is complex real ext-real set

].(X - C),(X + C).[ is open V67() V68() V69() Element of K6(REAL)

X + 0 is complex real ext-real Element of REAL

K6( the carrier of (R^1 | (cS1))) is non empty set

Cm is V67() V68() V69() open Element of K6( the carrier of R^1)

[#] (R^1 | (cS1)) is non empty non proper V67() V68() V69() open closed dense non boundary Element of K6( the carrier of (R^1 | (cS1)))

Cm /\ ([#] (R^1 | (cS1))) is V67() V68() V69() Element of K6( the carrier of (R^1 | (cS1)))

Int Cm is V67() V68() V69() open Element of K6( the carrier of R^1)

X - 0 is complex real ext-real Element of REAL

Ym is complex real ext-real Element of the carrier of R^1

A is V67() V68() V69() Element of K6( the carrier of (R^1 | (cS1)))

Q is non empty V67() V68() V69() open a_neighborhood of X

TOUCm .: Q is V67() V68() V69() Element of K6( the carrier of R^1)

TOUCm .: Cm is V67() V68() V69() Element of K6( the carrier of R^1)

(].0,1.[) is non empty V67() V68() V69() open Element of K6( the carrier of R^1)

TUC is non empty complex real ext-real set

cS1 is complex real ext-real set

AffineMap (TUC,cS1) is non empty V16() V19( REAL ) V20( REAL ) Function-like one-to-one total quasi_total onto bijective continuous V51() V52() V53() Element of K6(K7(REAL,REAL))

rng (AffineMap (TUC,cS1)) is V67() V68() V69() Element of K6(REAL)

[#] R^1 is non empty non proper V67() V68() V69() open closed dense non boundary Element of K6( the carrier of R^1)

dom (AffineMap (TUC,cS1)) is V67() V68() V69() Element of K6(REAL)

((dom (AffineMap (TUC,cS1)))) is V67() V68() V69() Element of K6( the carrier of R^1)

R^1 | ((dom (AffineMap (TUC,cS1)))) is strict TopSpace-like V299() SubSpace of R^1

((rng (AffineMap (TUC,cS1)))) is V67() V68() V69() Element of K6( the carrier of R^1)

R^1 | ((rng (AffineMap (TUC,cS1)))) is strict TopSpace-like V299() SubSpace of R^1

TUC is non empty complex real ext-real set

cS1 is complex real ext-real set

AffineMap (TUC,cS1) is non empty V16() V19( REAL ) V20( REAL ) Function-like one-to-one total quasi_total onto bijective continuous V51() V52() V53() Element of K6(K7(REAL,REAL))

dom (AffineMap (TUC,cS1)) is V67() V68() V69() Element of K6(REAL)

((dom (AffineMap (TUC,cS1)))) is V67() V68() V69() Element of K6( the carrier of R^1)

R^1 | ((dom (AffineMap (TUC,cS1)))) is strict TopSpace-like V299() SubSpace of R^1

rng (AffineMap (TUC,cS1)) is V67() V68() V69() Element of K6(REAL)

((rng (AffineMap (TUC,cS1)))) is V67() V68() V69() Element of K6( the carrier of R^1)

R^1 | ((rng (AffineMap (TUC,cS1)))) is strict TopSpace-like V299() SubSpace of R^1

((AffineMap (TUC,cS1))) is V16() V19( the carrier of (R^1 | ((dom (AffineMap (TUC,cS1)))))) V20( the carrier of (R^1 | ((rng (AffineMap (TUC,cS1)))))) Function-like one-to-one quasi_total onto bijective V51() V52() V53() continuous Element of K6(K7( the carrier of (R^1 | ((dom (AffineMap (TUC,cS1))))), the carrier of (R^1 | ((rng (AffineMap (TUC,cS1)))))))

the carrier of (R^1 | ((dom (AffineMap (TUC,cS1))))) is V67() V68() V69() set

the carrier of (R^1 | ((rng (AffineMap (TUC,cS1))))) is V67() V68() V69() set

K7( the carrier of (R^1 | ((dom (AffineMap (TUC,cS1))))), the carrier of (R^1 | ((rng (AffineMap (TUC,cS1)))))) is V51() V52() V53() set

K6(K7( the carrier of (R^1 | ((dom (AffineMap (TUC,cS1))))), the carrier of (R^1 | ((rng (AffineMap (TUC,cS1))))))) is non empty set

K6( the carrier of (R^1 | ((dom (AffineMap (TUC,cS1)))))) is non empty set

TREC is V67() V68() V69() Element of K6( the carrier of (R^1 | ((dom (AffineMap (TUC,cS1))))))

((AffineMap (TUC,cS1))) .: TREC is V67() V68() V69() Element of K6( the carrier of (R^1 | ((rng (AffineMap (TUC,cS1))))))

K6( the carrier of (R^1 | ((rng (AffineMap (TUC,cS1)))))) is non empty set

TUC is TopSpace-like V221() V222() SubSpace of TOP-REAL 2

the carrier of TUC is set

cS1 is non empty functional compact being_simple_closed_curve Element of K6( the carrier of (TOP-REAL 2))

[#] TUC is non proper open closed dense Element of K6( the carrier of TUC)

K6( the carrier of TUC) is non empty set

cS1 is V16() Function-like V34(2) V51() V52() V53() FinSequence-like Element of the carrier of (TOP-REAL 2)

TUC is non empty complex real ext-real positive non negative set

Sphere (cS1,TUC) is non empty functional closed V258( TOP-REAL 2) Element of K6( the carrier of (TOP-REAL 2))

{ b

cS1 `1 is complex real ext-real Element of REAL

cS1 `2 is complex real ext-real Element of REAL

|[(cS1 `1),(cS1 `2)]| is V16() Function-like V34(2) V51() V52() V53() FinSequence-like Element of the carrier of (TOP-REAL 2)

TREC is Element of the carrier of (Euclid 2)

Sphere (TREC,TUC) is Element of K6( the carrier of (Euclid 2))

K6( the carrier of (Euclid 2)) is non empty set

circle ((cS1 `1),(cS1 `2),TUC) is functional Element of K6( the carrier of (TOP-REAL 2))

{ b

TUC is ordinal natural complex real ext-real non negative integer set

TOP-REAL TUC is non empty TopSpace-like T_0 T_1 T_2 V136() V161() V162() V163() V164() V165() V166() V167() V221() V222() V254() L19()

the carrier of (TOP-REAL TUC) is non empty functional set

cS1 is V16() Function-like V34(TUC) V51() V52() V53() FinSequence-like Element of the carrier of (TOP-REAL TUC)

TREC is complex real ext-real set

Sphere (cS1,TREC) is functional closed Element of K6( the carrier of (TOP-REAL TUC))

K6( the carrier of (TOP-REAL TUC)) is non empty set

{ b

(TOP-REAL TUC) | (Sphere (cS1,TREC)) is strict TopSpace-like V221() V222() SubSpace of TOP-REAL TUC

TUC is non empty ordinal natural complex real ext-real positive non negative integer set

TOP-REAL TUC is non empty TopSpace-like T_0 T_1 T_2 V136() V161() V162() V163() V164() V165() V166() V167() V221() V222() V254() L19()

the carrier of (TOP-REAL TUC) is non empty functional set

cS1 is V16() Function-like V34(TUC) V51() V52() V53() FinSequence-like Element of the carrier of (TOP-REAL TUC)

TREC is complex real ext-real non negative set

(TUC,cS1,TREC) is TopSpace-like V221() V222() SubSpace of TOP-REAL TUC

Sphere (cS1,TREC) is non empty functional closed Element of K6( the carrier of (TOP-REAL TUC))

K6( the carrier of (TOP-REAL TUC)) is non empty set

{ b

(TOP-REAL TUC) | (Sphere (cS1,TREC)) is non empty strict TopSpace-like V221() V222() SubSpace of TOP-REAL TUC

TUC is ordinal natural complex real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() Element of NAT

TOP-REAL TUC is non empty TopSpace-like T_0 T_1 T_2 V136() V161() V162() V163() V164() V165() V166() V167() V221() V222() V254() L19()

the carrier of (TOP-REAL TUC) is non empty functional set

cS1 is complex real ext-real set

TREC is V16() Function-like V34(TUC) V51() V52() V53() FinSequence-like Element of the carrier of (TOP-REAL TUC)

(TUC,TREC,cS1) is TopSpace-like V221() V222() SubSpace of TOP-REAL TUC

Sphere (TREC,cS1) is functional closed V258( TOP-REAL TUC) Element of K6( the carrier of (TOP-REAL TUC))

K6( the carrier of (TOP-REAL TUC)) is non empty set

{ b

(TOP-REAL TUC) | (Sphere (TREC,cS1)) is strict TopSpace-like V221() V222() SubSpace of TOP-REAL TUC

the carrier of (TUC,TREC,cS1) is set

[#] (TUC,TREC,cS1) is non proper open closed dense Element of K6( the carrier of (TUC,TREC,cS1))

K6( the carrier of (TUC,TREC,cS1)) is non empty set

TUC is ordinal natural complex real ext-real non negative integer set

TOP-REAL TUC is non empty TopSpace-like T_0 T_1 T_2 V136() V161() V162() V163() V164() V165() V166() V167() V221() V222() V254() L19()

the carrier of (TOP-REAL TUC) is non empty functional set

cS1 is V16() Function-like V34(TUC) V51() V52() V53() FinSequence-like Element of the carrier of (TOP-REAL TUC)

TREC is empty trivial complex real ext-real non positive non negative Function-like functional V67() V68() V69() V70() V71() V72() V73() set

(TUC,cS1,TREC) is TopSpace-like V221() V222() SubSpace of TOP-REAL TUC

Sphere (cS1,TREC) is functional closed Element of K6( the carrier of (TOP-REAL TUC))

K6( the carrier of (TOP-REAL TUC)) is non empty set

{ b

(TOP-REAL TUC) | (Sphere (cS1,TREC)) is strict TopSpace-like V221() V222() SubSpace of TOP-REAL TUC

Euclid TUC is non empty strict Reflexive discerning V245() triangle MetrStruct

the carrier of (Euclid TUC) is non empty set

the carrier of (TUC,cS1,TREC) is set

TOUC is Element of the carrier of (Euclid TUC)

Sphere (TOUC,TREC) is Element of K6( the carrier of (Euclid TUC))

K6( the carrier of (Euclid TUC)) is non empty set

{TOUC} is non empty trivial Element of K6( the carrier of (Euclid TUC))

TUC is complex real ext-real set

(2,(0. (TOP-REAL 2)),TUC) is TopSpace-like V221() V222() SubSpace of TOP-REAL 2

Sphere ((0. (TOP-REAL 2)),TUC) is functional closed V258( TOP-REAL 2) Element of K6( the carrier of (TOP-REAL 2))

{ b

(TOP-REAL 2) | (Sphere ((0. (TOP-REAL 2)),TUC)) is strict TopSpace-like V221() V222() SubSpace of TOP-REAL 2

- TUC is complex real ext-real set

Trectangle ((- TUC),TUC,(- TUC),TUC) is TopSpace-like V221() V222() SubSpace of TOP-REAL 2

closed_inside_of_rectangle ((- TUC),TUC,(- TUC),TUC) is functional Element of K6( the carrier of (TOP-REAL 2))

(TOP-REAL 2) | (closed_inside_of_rectangle ((- TUC),TUC,(- TUC),TUC)) is strict TopSpace-like V221() V222() SubSpace of TOP-REAL 2

the carrier of (2,(0. (TOP-REAL 2)),TUC) is set

the carrier of (Trectangle ((- TUC),TUC,(- TUC),TUC)) is set

TOUC is set

{ b

TOUCm is V16() Function-like V34(2) V51() V52() V53() FinSequence-like Element of the carrier of (TOP-REAL 2)

|.TOUCm.| is complex real ext-real non negative Element of REAL

TOUCm `2 is complex real ext-real Element of REAL

abs (TOUCm `2) is complex real ext-real Element of REAL

TOUCm `1 is complex real ext-real Element of REAL

abs (TOUCm `1) is complex real ext-real Element of REAL

TUC is V16() Function-like V34(2) V51() V52() V53() FinSequence-like Element of the carrier of (TOP-REAL 2)

cS1 is non empty complex real ext-real positive non negative set

(2,TUC,cS1) is non empty strict TopSpace-like V221() V222() SubSpace of TOP-REAL 2

Sphere (TUC,cS1) is non empty functional closed closed compact V258( TOP-REAL 2) V258( TOP-REAL 2) being_simple_closed_curve Element of K6( the carrier of (TOP-REAL 2))

{ b

(TOP-REAL 2) | (Sphere (TUC,cS1)) is non empty strict TopSpace-like compact V221() V222() V266() SubSpace of TOP-REAL 2

the carrier of (2,TUC,cS1) is non empty set

the V16() Function-like V34(2) V51() V52() V53() FinSequence-like Element of the carrier of (TOP-REAL 2) is V16() Function-like V34(2) V51() V52() V53() FinSequence-like Element of the carrier of (TOP-REAL 2)

the non empty complex real ext-real positive non negative set is non empty complex real ext-real positive non negative set

(2, the V16() Function-like V34(2) V51() V52() V53() FinSequence-like Element of the carrier of (TOP-REAL 2), the non empty complex real ext-real positive non negative set ) is non empty strict TopSpace-like compact V221() V222() V266() pathwise_connected () SubSpace of TOP-REAL 2

Sphere ( the V16() Function-like V34(2) V51() V52() V53() FinSequence-like Element of the carrier of (TOP-REAL 2), the non empty complex real ext-real positive non negative set ) is non empty functional closed closed compact V258( TOP-REAL 2) V258( TOP-REAL 2) being_simple_closed_curve Element of K6( the carrier of (TOP-REAL 2))

{ b

(TOP-REAL 2) | (Sphere ( the V16() Function-like V34(2) V51() V52() V53() FinSequence-like Element of the carrier of (TOP-REAL 2), the non empty complex real ext-real positive non negative set )) is non empty strict TopSpace-like compact V221() V222() V266() SubSpace of TOP-REAL 2

TUC is non empty TopSpace-like compact V221() V222() V266() pathwise_connected () SubSpace of TOP-REAL 2

cS1 is non empty TopSpace-like compact V221() V222() V266() pathwise_connected () SubSpace of TOP-REAL 2

the carrier of TUC is non empty set

the topology of TUC is non empty Element of K6(K6( the carrier of TUC))

K6( the carrier of TUC) is non empty set

K6(K6( the carrier of TUC)) is non empty set

TopStruct(# the carrier of TUC, the topology of TUC #) is non empty strict TopSpace-like TopStruct

the carrier of cS1 is non empty set

the topology of cS1 is non empty Element of K6(K6( the carrier of cS1))

K6( the carrier of cS1) is non empty set

K6(K6( the carrier of cS1)) is non empty set

TopStruct(# the carrier of cS1, the topology of cS1 #) is non empty strict TopSpace-like TopStruct

the carrier of TopStruct(# the carrier of TUC, the topology of TUC #) is non empty set

TREC is non empty functional compact being_simple_closed_curve Element of K6( the carrier of (TOP-REAL 2))

(TOP-REAL 2) | TREC is non empty strict TopSpace-like compact V221() V222() V266() SubSpace of TOP-REAL 2

the carrier of ((TOP-REAL 2) | TREC) is non empty set

K7( the carrier of ((TOP-REAL 2) | R^2-unit_square), the carrier of ((TOP-REAL 2) | TREC)) is non empty set

K6(K7( the carrier of ((TOP-REAL 2) | R^2-unit_square), the carrier of ((TOP-REAL 2) | TREC))) is non empty set

TOUC is non empty V16() V19( the carrier of ((TOP-REAL 2) | R^2-unit_square)) V20( the carrier of ((TOP-REAL 2) | TREC)) Function-like total quasi_total Element of K6(K7( the carrier of ((TOP-REAL 2) | R^2-unit_square), the carrier of ((TOP-REAL 2) | TREC)))

TOUC /" is non empty V16() V19( the carrier of ((TOP-REAL 2) | TREC)) V20( the carrier of ((TOP-REAL 2) | R^2-unit_square)) Function-like total quasi_total Element of K6(K7( the carrier of ((TOP-REAL 2) | TREC), the carrier of ((TOP-REAL 2) | R^2-unit_square)))

K7( the carrier of ((TOP-REAL 2) | TREC), the carrier of ((TOP-REAL 2) | R^2-unit_square)) is non empty set

K6(K7( the carrier of ((TOP-REAL 2) | TREC), the carrier of ((TOP-REAL 2) | R^2-unit_square))) is non empty set

[#] TopStruct(# the carrier of TUC, the topology of TUC #) is non empty non proper open closed dense non boundary Element of K6( the carrier of TopStruct(# the carrier of TUC, the topology of TUC #))

K6( the carrier of TopStruct(# the carrier of TUC, the topology of TUC #)) is non empty set

the carrier of TopStruct(# the carrier of cS1, the topology of cS1 #) is non empty set

TOUCm is non empty functional compact being_simple_closed_curve Element of K6( the carrier of (TOP-REAL 2))

(TOP-REAL 2) | TOUCm is non empty strict TopSpace-like compact V221() V222() V266() SubSpace of TOP-REAL 2

the carrier of ((TOP-REAL 2) | TOUCm) is non empty set

K7( the carrier of ((TOP-REAL 2) | R^2-unit_square), the carrier of ((TOP-REAL 2) | TOUCm)) is non empty set

K6(K7( the carrier of ((TOP-REAL 2) | R^2-unit_square), the carrier of ((TOP-REAL 2) | TOUCm))) is non empty set

X is non empty V16() V19( the carrier of ((TOP-REAL 2) | R^2-unit_square)) V20( the carrier of ((TOP-REAL 2) | TOUCm)) Function-like total quasi_total Element of K6(K7( the carrier of ((TOP-REAL 2) | R^2-unit_square), the carrier of ((TOP-REAL 2) | TOUCm)))

[#] TopStruct(# the carrier of cS1, the topology of cS1 #) is non empty non proper open closed dense non boundary Element of K6( the carrier of TopStruct(# the carrier of cS1, the topology of cS1 #))

K6( the carrier of TopStruct(# the carrier of cS1, the topology of cS1 #)) is non empty set

K7( the carrier of TopStruct(# the carrier of TUC, the topology of TUC #), the carrier of TopStruct(# the carrier of cS1, the topology of cS1 #)) is non empty set

K6(K7( the carrier of TopStruct(# the carrier of TUC, the topology of TUC #), the carrier of TopStruct(# the carrier of cS1, the topology of cS1 #))) is non empty set

X * (TOUC /") is non empty V16() V19( the carrier of ((TOP-REAL 2) | TREC)) V20( the carrier of ((TOP-REAL 2) | TOUCm)) Function-like total quasi_total Element of K6(K7( the carrier of ((TOP-REAL 2) | TREC), the carrier of ((TOP-REAL 2) | TOUCm)))

K7( the carrier of ((TOP-REAL 2) | TREC), the carrier of ((TOP-REAL 2) | TOUCm)) is non empty set

K6(K7( the carrier of ((TOP-REAL 2) | TREC), the carrier of ((TOP-REAL 2) | TOUCm))) is non empty set

Xm is non empty V16() V19( the carrier of TopStruct(# the carrier of TUC, the topology of TUC #)) V20( the carrier of TopStruct(# the carrier of cS1, the topology of cS1 #)) Function-like total quasi_total Element of K6(K7( the carrier of TopStruct(# the carrier of TUC, the topology of TUC #), the carrier of TopStruct(# the carrier of cS1, the topology of cS1 #)))

TUC is ordinal natural complex real ext-real non negative integer set

TOP-REAL TUC is non empty TopSpace-like T_0 T_1 T_2 V136() V161() V162() V163() V164() V165() V166() V167() V221() V222() V254() L19()

0. (TOP-REAL TUC) is V16() Function-like V34(TUC) V51() V52() V53() FinSequence-like zero Element of the carrier of (TOP-REAL TUC)

the carrier of (TOP-REAL TUC) is non empty functional set

the ZeroF of (TOP-REAL TUC) is V16() Function-like V34(TUC) V51() V52() V53() FinSequence-like Element of the carrier of (TOP-REAL TUC)

(TUC,(0. (TOP-REAL TUC)),1) is TopSpace-like V221() V222() SubSpace of TOP-REAL TUC

Sphere ((0. (TOP-REAL TUC)),1) is functional closed Element of K6( the carrier of (TOP-REAL TUC))

K6( the carrier of (TOP-REAL TUC)) is non empty set

{ b

(TOP-REAL TUC) | (Sphere ((0. (TOP-REAL TUC)),1)) is strict TopSpace-like V221() V222() SubSpace of TOP-REAL TUC

(2) is TopSpace-like V221() V222() SubSpace of TOP-REAL 2

(2,(0. (TOP-REAL 2)),1) is non empty strict TopSpace-like compact V221() V222() V266() pathwise_connected () SubSpace of TOP-REAL 2

Sphere ((0. (TOP-REAL 2)),1) is non empty functional closed closed compact V258( TOP-REAL 2) V258( TOP-REAL 2) being_simple_closed_curve Element of K6( the carrier of (TOP-REAL 2))

{ b

(TOP-REAL 2) | (Sphere ((0. (TOP-REAL 2)),1)) is non empty strict TopSpace-like compact V221() V222() V266() SubSpace of TOP-REAL 2

the carrier of (2) is set

Sphere (|[0,0]|,1) is non empty functional closed closed compact V258( TOP-REAL 2) V258( TOP-REAL 2) being_simple_closed_curve Element of K6( the carrier of (TOP-REAL 2))

{ b

TREC is non empty ordinal natural complex real ext-real positive non negative integer set

(TREC) is TopSpace-like V221() V222() SubSpace of TOP-REAL TREC

TOP-REAL TREC is non empty TopSpace-like T_0 T_1 T_2 V136() V161() V162() V163() V164() V165() V166() V167() V221() V222() V254() L19()

0. (TOP-REAL TREC) is V16() Function-like V34(TREC) V51() V52() V53() FinSequence-like zero Element of the carrier of (TOP-REAL TREC)

the carrier of (TOP-REAL TREC) is non empty functional set

the ZeroF of (TOP-REAL TREC) is V16() Function-like V34(TREC) V51() V52() V53() FinSequence-like Element of the carrier of (TOP-REAL TREC)

(TREC,(0. (TOP-REAL TREC)),1) is non empty strict TopSpace-like V221() V222() SubSpace of TOP-REAL TREC

Sphere ((0. (TOP-REAL TREC)),1) is non empty functional closed Element of K6( the carrier of (TOP-REAL TREC))

K6( the carrier of (TOP-REAL TREC)) is non empty set

{ b

(TOP-REAL TREC) | (Sphere ((0. (TOP-REAL TREC)),1)) is non empty strict TopSpace-like V221() V222() SubSpace of TOP-REAL TREC

TOUC is non empty ordinal natural complex real ext-real positive non negative integer V66() V67() V68() V69() V70() V71() V72() Element of NAT

TOP-REAL TOUC is non empty TopSpace-like T_0 T_1 T_2 V136() V161() V162() V163() V164() V165() V166() V167() V221() V222() V254() L19()

the carrier of (TOP-REAL TOUC) is non empty functional set

(TOUC) is non empty TopSpace-like V221() V222() SubSpace of TOP-REAL TOUC

0. (TOP-REAL TOUC) is V16() Function-like V34(TOUC) V51() V52() V53() FinSequence-like zero Element of the carrier of (TOP-REAL TOUC)

the ZeroF of (TOP-REAL TOUC) is V16() Function-like V34(TOUC) V51() V52() V53() FinSequence-like Element of the carrier of (TOP-REAL TOUC)

(TOUC,(0. (TOP-REAL TOUC)),1) is non empty strict TopSpace-like V221() V222() SubSpace of TOP-REAL TOUC

Sphere ((0. (TOP-REAL TOUC)),1) is non empty functional closed V258( TOP-REAL TOUC) Element of K6( the carrier of (TOP-REAL TOUC))

K6( the carrier of (TOP-REAL TOUC)) is non empty set

{ b

(TOP-REAL TOUC) | (Sphere ((0. (TOP-REAL TOUC)),1)) is non empty strict TopSpace-like V221() V222() SubSpace of TOP-REAL TOUC

the carrier of (TOUC) is non empty set

TOUCm is V16() Function-like V34(TOUC) V51() V52() V53() FinSequence-like Element of the carrier of (TOP-REAL TOUC)

|.TOUCm.| is complex real ext-real non negative Element of REAL

TREC is complex real ext-real non negative set

(TOUC,(0. (TOP-REAL TOUC)),TREC) is non empty strict TopSpace-like V221() V222() SubSpace of TOP-REAL TOUC

Sphere ((0. (TOP-REAL TOUC)),TREC) is non empty functional closed V258( TOP-REAL TOUC) Element of K6( the carrier of (TOP-REAL TOUC))

{ b

(TOP-REAL TOUC) | (Sphere ((0. (TOP-REAL TOUC)),TREC)) is non empty strict TopSpace-like V221() V222() SubSpace of TOP-REAL TOUC

the carrier of (TOUC,(0. (TOP-REAL TOUC)),TREC) is non empty set

TREC is V16() Function-like V34(2) V51() V52() V53() FinSequence-like Element of the carrier of (TOP-REAL 2)

TREC `1 is complex real ext-real Element of REAL

TREC `2 is complex real ext-real Element of REAL

TOUC is complex real ext-real Element of REAL

TOUCm is complex real ext-real Element of REAL

<*TOUC,TOUCm*> is set

1 ^2 is complex real ext-real Element of REAL

1 * 1 is non empty ordinal natural complex real ext-real positive non negative integer set

|.TREC.| is complex real ext-real non negative Element of REAL

|.TREC.| ^2 is complex real ext-real Element of REAL

|.TREC.| * |.TREC.| is complex real ext-real non negative set

TOUC ^2 is complex real ext-real Element of REAL

TOUC * TOUC is complex real ext-real set

TOUCm ^2 is complex real ext-real Element of REAL

TOUCm * TOUCm is complex real ext-real set

(TOUC ^2) + (TOUCm ^2) is complex real ext-real Element of REAL

- (TOUC ^2) is complex real ext-real Element of REAL

- 0 is empty trivial complex real ext-real non positive non negative Function-like functional integer V67() V68() V69() V70() V71() V72() V73() Element of REAL

(TOUCm ^2) - 1 is complex real ext-real Element of REAL

- (TOUCm ^2) is complex real ext-real Element of REAL

(TOUC ^2) - 1 is complex real ext-real Element of REAL

TREC is V16() Function-like V34(2) V51() V52() V53() FinSequence-like Element of the carrier of (TOP-REAL 2)

TREC `1 is complex real ext-real Element of REAL

TREC `2 is complex real ext-real Element of REAL

1 ^2 is complex real ext-real Element of REAL

1 * 1 is non empty ordinal natural complex real ext-real positive non negative integer set

|.TREC.| is complex real ext-real non negative Element of REAL

|.TREC.| ^2 is complex real ext-real Element of REAL

|.TREC.| * |.TREC.| is complex real ext-real non negative set

(TREC `1) ^2 is complex real ext-real Element of REAL

(TREC `1) * (TREC `1) is complex real ext-real set

(TREC `2) ^2 is complex real ext-real Element of REAL

(TREC `2) * (TREC `2) is complex real ext-real set

((TREC `1) ^2) + ((TREC `2) ^2) is complex real ext-real Element of REAL

TREC is V16() Function-like V34(2) V51() V52() V53() FinSequence-like Element of the carrier of (TOP-REAL 2)

TREC `1 is complex real ext-real Element of REAL

TREC `2 is complex real ext-real Element of REAL

1 ^2 is complex real ext-real Element of REAL

1 * 1 is non empty ordinal natural complex real ext-real positive non negative integer set

|.TREC.| is complex real ext-real non negative Element of REAL

|.TREC.| ^2 is complex real ext-real Element of REAL

|.TREC.| * |.TREC.| is complex real ext-real non negative set

(TREC `1) ^2 is complex real ext-real Element of REAL

(TREC `1) * (TREC `1) is complex real ext-real set

(TREC `2) ^2 is complex real ext-real Element of REAL

(TREC `2) * (TREC `2) is complex real ext-real set

((TREC `1) ^2) + ((TREC `2) ^2) is complex real ext-real Element of REAL

TREC is V16() Function-like V34(2) V51() V52() V53() FinSequence-like Element of the carrier of (TOP-REAL 2)

TREC `2 is complex real ext-real Element of REAL

TREC `1 is complex real ext-real Element of REAL

1 ^2 is complex real ext-real Element of REAL

1 * 1 is non empty ordinal natural complex real ext-real positive non negative integer set

|.TREC.| is complex real ext-real non negative Element of REAL

|.TREC.| ^2 is complex real ext-real Element of REAL

|.TREC.| * |.TREC.| is complex real ext-real non negative set

(TREC `1) ^2 is complex real ext-real Element of REAL

(TREC `1) * (TREC `1) is complex real ext-real set

(TREC `2) ^2 is complex real ext-real Element of REAL

(TREC `2) * (TREC `2) is complex real ext-real set

((TREC `1) ^2) + ((TREC `2) ^2) is complex real ext-real Element of REAL

TREC is V16() Function-like V34(2) V51() V52() V53() FinSequence-like Element of the carrier of (TOP-REAL 2)

TREC `2 is complex real ext-real Element of REAL

TREC `1 is complex real ext-real Element of REAL

1 ^2 is complex real ext-real Element of REAL

1 * 1 is non empty ordinal natural complex real ext-real positive non negative integer set

|.TREC.| is complex real ext-real non negative Element of REAL

|.TREC.| ^2 is complex real ext-real Element of REAL

|.TREC.| * |.TREC.| is complex real ext-real non negative set

(TREC `1) ^2 is complex real ext-real Element of REAL

(TREC `1) * (TREC `1) is complex real ext-real set

(TREC `2) ^2 is complex real ext-real Element of REAL

(TREC `2) * (TREC `2) is complex real ext-real set

((TREC `1) ^2) + ((TREC `2) ^2) is complex real ext-real Element of REAL

p0 is non empty complex real ext-real non positive negative set

p1 is non empty complex real ext-real positive non negative set

Trectangle (p0,p1,p0,p1) is non empty TopSpace-like V221() V222() SubSpace of TOP-REAL 2

closed_inside_of_rectangle (p0,p1,p0,p1) is functional Element of K6( the carrier of (TOP-REAL 2))

(TOP-REAL 2) | (closed_inside_of_rectangle (p0,p1,p0,p1)) is strict TopSpace-like V221() V222() SubSpace of TOP-REAL 2

Trectangle ((- 1),1,(- 1),1) is non empty TopSpace-like V221() V222() SubSpace of TOP-REAL 2

closed_inside_of_rectangle ((- 1),1,(- 1),1) is functional Element of K6( the carrier of (TOP-REAL 2))

(TOP-REAL 2) | (closed_inside_of_rectangle ((- 1),1,(- 1),1)) is strict TopSpace-like V221() V222() SubSpace of TOP-REAL 2

TOUC is non empty ordinal natural complex real ext-real positive non negative integer V66() V67() V68() V69() V70() V71() V72() Element of NAT

TOP-REAL TOUC is non empty TopSpace-like T_0 T_1 T_2 V136() V161() V162() V163() V164() V165() V166() V167() V221() V222() V254() L19()

the carrier of (TOP-REAL TOUC) is non empty functional set

(TOUC) is non empty TopSpace-like V221() V222() SubSpace of TOP-REAL TOUC

0. (TOP-REAL TOUC) is V16() Function-like V34(TOUC) V51() V52() V53() FinSequence-like zero Element of the carrier of (TOP-REAL TOUC)

the ZeroF of (TOP-REAL TOUC) is V16() Function-like V34(TOUC) V51() V52() V53() FinSequence-like Element of the carrier of (TOP-REAL TOUC)

(TOUC,(0. (TOP-REAL TOUC)),1) is non empty strict TopSpace-like V221() V222() SubSpace of TOP-REAL TOUC

Sphere ((0. (TOP-REAL TOUC)),1) is non empty functional closed V258( TOP-REAL TOUC) Element of K6( the carrier of (TOP-REAL TOUC))

K6( the carrier of (TOP-REAL TOUC)) is non empty set

{ b

(TOP-REAL TOUC) | (Sphere ((0. (TOP-REAL TOUC)),1)) is non empty strict TopSpace-like V221() V222() SubSpace of TOP-REAL TOUC

the carrier of (TOUC) is non empty set

TOUCm is non empty complex real ext-real positive non negative set

X is V16() Function-like V34(TOUC) V51() V52() V53() FinSequence-like Element of the carrier of (TOP-REAL TOUC)

(TOUC,X,TOUCm) is non empty strict TopSpace-like V221() V222() SubSpace of TOP-REAL TOUC

Sphere (X,TOUCm) is non empty functional closed V258( TOP-REAL TOUC) Element of K6( the carrier of (TOP-REAL TOUC))

{ b

(TOP-REAL TOUC) | (Sphere (X,TOUCm)) is non empty strict TopSpace-like V221() V222() SubSpace of TOP-REAL TOUC

the carrier of (TOUC,X,TOUCm) is non empty set

K7( the carrier of (TOUC), the carrier of (TOUC,X,TOUCm)) is non empty set

K6(K7( the carrier of (TOUC), the carrier of (TOUC,X,TOUCm))) is non empty set

Xm is non empty V16() V19( the carrier of (TOUC)) V20( the carrier of (TOUC,X,TOUCm)) Function-like total quasi_total Element of K6(K7( the carrier of (TOUC), the carrier of (TOUC,X,TOUCm)))

A1 is V16() Function-like V34(TOUC) V51() V52() V53() FinSequence-like Element of the carrier of (TOP-REAL TOUC)

TOUCm * A1 is V16() Function-like V34(TOUC) V51() V52() V53() FinSequence-like Element of the carrier of (TOP-REAL TOUC)

K547(A1,TOUCm) is V16() V19( NAT ) V20( REAL ) Function-like V51() V52() V53() FinSequence-like FinSequence of REAL

(TOUCm * A1) + X is V16() Function-like V34(TOUC) V51() V52() V53() FinSequence-like Element of the carrier of (TOP-REAL TOUC)

the U6 of (TOP-REAL TOUC) is non empty V16() V19(K7( the carrier of (TOP-REAL TOUC), the carrier of (TOP-REAL TOUC))) V20( the carrier of (TOP-REAL TOUC)) Function-like total quasi_total Function-yielding V312() Element of K6(K7(K7( the carrier of (TOP-REAL TOUC), the carrier of (TOP-REAL TOUC)), the carrier of (TOP-REAL TOUC)))

K7( the carrier of (TOP-REAL TOUC), the carrier of (TOP-REAL TOUC)) is non empty set

K7(K7( the carrier of (TOP-REAL TOUC), the carrier of (TOP-REAL TOUC)), the carrier of (TOP-REAL TOUC)) is non empty set

K6(K7(K7( the carrier of (TOP-REAL TOUC), the carrier of (TOP-REAL TOUC)), the carrier of (TOP-REAL TOUC))) is non empty set

K414( the carrier of (TOP-REAL TOUC), the U6 of (TOP-REAL TOUC),(TOUCm * A1),X) is V16() Function-like V34(TOUC) V51() V52() V53() FinSequence-like Element of the carrier of (TOP-REAL TOUC)

K541((TOUCm * A1),X) is V16() V19( NAT ) V20( REAL ) Function-like V51() V52() V53() FinSequence-like FinSequence of REAL

K7( the carrier of (TOP-REAL TOUC), the carrier of (TOP-REAL TOUC)) is non empty set

K6(K7( the carrier of (TOP-REAL TOUC), the carrier of (TOP-REAL TOUC))) is non empty set

A1 is non empty V16() V19( the carrier of (TOP-REAL TOUC)) V20( the carrier of (TOP-REAL TOUC)) Function-like total quasi_total Function-yielding V312() Element of K6(K7( the carrier of (TOP-REAL TOUC), the carrier of (TOP-REAL TOUC)))

1 / TOUCm is non empty complex real ext-real positive non negative Element of REAL

C is V16() Function-like V34(TOUC) V51() V52() V53() FinSequence-like Element of the carrier of (TOP-REAL TOUC)

C - X is V16() Function-like V34(TOUC) V51() V52() V53() FinSequence-like Element of the carrier of (TOP-REAL TOUC)

- X is V16() Function-like V34(TOUC) V51() V52() V53() FinSequence-like Element of the carrier of (TOP-REAL TOUC)

K543(X) is V16() V19( NAT ) V20( REAL ) Function-like V51() V52() V53() FinSequence-like FinSequence of REAL

K394((TOP-REAL TOUC),C,(- X)) is V16() Function-like V34(TOUC) V51() V52() V53() FinSequence-like Element of the carrier of (TOP-REAL TOUC)

the U6 of (TOP-REAL TOUC) is non empty V16() V19(K7( the carrier of (TOP-REAL TOUC), the carrier of (TOP-REAL TOUC))) V20( the carrier of (TOP-REAL TOUC)) Function-like total quasi_total Function-yielding V312() Element of K6(K7(K7( the carrier of (TOP-REAL TOUC), the carrier of (TOP-REAL TOUC)), the carrier of (TOP-REAL TOUC)))

K7(K7( the carrier of (TOP-REAL TOUC), the carrier of (TOP-REAL TOUC)), the carrier of (TOP-REAL TOUC)) is non empty set

K6(K7(K7( the carrier of (TOP-REAL TOUC), the carrier of (TOP-REAL TOUC)), the carrier of (TOP-REAL TOUC))) is non empty set

K414( the carrier of (TOP-REAL TOUC), the U6 of (TOP-REAL TOUC),C,(- X)) is V16() Function-like V34(TOUC) V51() V52() V53() FinSequence-like Element of the carrier of (TOP-REAL TOUC)

K541(C,(- X)) is V16() V19( NAT ) V20( REAL ) Function-like V51() V52() V53() FinSequence-like FinSequence of REAL

K545(C,X) is V16() V19( NAT ) V20( REAL ) Function-like V51() V52() V53() FinSequence-like FinSequence of REAL

(1 / TOUCm) * (C - X) is V16() Function-like V34(TOUC) V51() V52() V53() FinSequence-like Element of the carrier of (TOP-REAL TOUC)

K547((C - X),(1 / TOUCm)) is V16() V19( NAT ) V20( REAL ) Function-like V51() V52() V53() FinSequence-like FinSequence of REAL

C is non empty V16() V19( the carrier of (TOP-REAL TOUC)) V20( the carrier of (TOP-REAL TOUC)) Function-like total quasi_total Function-yielding V312() Element of K6(K7( the carrier of (TOP-REAL TOUC), the carrier of (TOP-REAL TOUC)))

(TOP-REAL TOUC) --> X is non empty V16() V19( the carrier of (TOP-REAL TOUC)) V20( the carrier of (TOP-REAL TOUC)) Function-like total quasi_total continuous Function-yielding V312() Element of K6(K7( the carrier of (TOP-REAL TOUC), the carrier of (TOP-REAL TOUC)))

the carrier of (TOP-REAL TOUC) --> X is non empty V16() V19( the carrier of (TOP-REAL TOUC)) V20( the carrier of (TOP-REAL TOUC)) Function-like constant total quasi_total Function-yielding V312() Element of K6(K7( the carrier of (TOP-REAL TOUC), the carrier of (TOP-REAL TOUC)))

id (TOP-REAL TOUC) is non empty V16() V19( the carrier of (TOP-REAL TOUC)) V20( the carrier of (TOP-REAL TOUC)) Function-like one-to-one total quasi_total onto bijective continuous being_homeomorphism open Function-yielding V312() Element of K6(K7( the carrier of (TOP-REAL TOUC), the carrier of (TOP-REAL TOUC)))

id the carrier of (TOP-REAL TOUC) is non empty V16() V19( the carrier of (TOP-REAL TOUC)) V20( the carrier of (TOP-REAL TOUC)) Function-like one-to-one total quasi_total Function-yielding V312() Element of K6(K7( the carrier of (TOP-REAL TOUC), the carrier of (TOP-REAL TOUC)))

dom C is functional Element of K6( the carrier of (TOP-REAL TOUC))

C | (Sphere (X,TOUCm)) is V16() V19( the carrier of (TOP-REAL TOUC)) V20( the carrier of (TOP-REAL TOUC)) Function-like Function-yielding V312() Element of K6(K7( the carrier of (TOP-REAL TOUC), the carrier of (TOP-REAL TOUC)))

dom (C | (Sphere (X,TOUCm))) is functional Element of K6( the carrier of (TOP-REAL TOUC))

- (1 / TOUCm) is non empty complex real ext-real non positive negative Element of REAL

Q is V16() Function-like V34(TOUC) V51() V52() V53() FinSequence-like Element of the carrier of (TOP-REAL TOUC)

C . Q is V16() Function-like V34(TOUC) V51() V52() V53() FinSequence-like Element of the carrier of (TOP-REAL TOUC)

(id (TOP-REAL TOUC)) . Q is V16() Function-like V34(TOUC) V51() V52() V53() FinSequence-like Element of the carrier of (TOP-REAL TOUC)

(1 / TOUCm) * ((id (TOP-REAL TOUC)) . Q) is V16() Function-like V34(TOUC) V51() V52()