:: BORSUK_7 semantic presentation

REAL is non empty V32() V195() V196() V197() V201() set

NAT is V195() V196() V197() V198() V199() V200() V201() Element of bool REAL

bool REAL is V74() set

I[01] is non empty strict TopSpace-like V224() V231() pathwise_connected connected SubSpace of R^1

R^1 is non empty strict TopSpace-like V231() pathwise_connected connected TopStruct

the carrier of I[01] is non empty V195() V196() V197() set

[:I[01],I[01]:] is non empty strict TopSpace-like TopStruct

the carrier of [:I[01],I[01]:] is non empty set

COMPLEX is non empty V32() V195() V201() set

RAT is non empty V32() V195() V196() V197() V198() V201() set

INT is non empty V32() V195() V196() V197() V198() V199() V201() set

[:COMPLEX,COMPLEX:] is Relation-like complex-yielding set

bool [:COMPLEX,COMPLEX:] is set

[:[:COMPLEX,COMPLEX:],COMPLEX:] is Relation-like complex-yielding set

bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is set

[:REAL,REAL:] is Relation-like complex-yielding ext-real-valued real-valued set

bool [:REAL,REAL:] is set

[:[:REAL,REAL:],REAL:] is Relation-like complex-yielding ext-real-valued real-valued set

bool [:[:REAL,REAL:],REAL:] is set

[:RAT,RAT:] is Relation-like RAT -valued complex-yielding ext-real-valued real-valued set

bool [:RAT,RAT:] is set

[:[:RAT,RAT:],RAT:] is Relation-like RAT -valued complex-yielding ext-real-valued real-valued set

bool [:[:RAT,RAT:],RAT:] is set

[:INT,INT:] is Relation-like RAT -valued INT -valued complex-yielding ext-real-valued real-valued set

bool [:INT,INT:] is set

[:[:INT,INT:],INT:] is Relation-like RAT -valued INT -valued complex-yielding ext-real-valued real-valued set

bool [:[:INT,INT:],INT:] is set

[:NAT,NAT:] is Relation-like RAT -valued INT -valued complex-yielding ext-real-valued real-valued natural-valued set

[:[:NAT,NAT:],NAT:] is Relation-like RAT -valued INT -valued complex-yielding ext-real-valued real-valued natural-valued set

bool [:[:NAT,NAT:],NAT:] is set

NAT is V195() V196() V197() V198() V199() V200() V201() set

bool NAT is set

bool NAT is set

{} is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty V32() FinSequence-like FinSubsequence-like FinSequence-membered complex-yielding ext-real-valued real-valued natural-valued Function-yielding V178() V195() V196() V197() V198() V199() V200() V201() complex-functions-membered ext-real-functions-membered real-functions-membered rational-functions-membered integer-functions-membered natural-functions-membered complex-functions-valued ext-real-functions-valued real-functions-valued rational-functions-valued integer-functions-valued natural-functions-valued set

the Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty V32() FinSequence-like FinSubsequence-like FinSequence-membered complex-yielding ext-real-valued real-valued natural-valued Function-yielding V178() V195() V196() V197() V198() V199() V200() V201() complex-functions-membered ext-real-functions-membered real-functions-membered rational-functions-membered integer-functions-membered natural-functions-membered complex-functions-valued ext-real-functions-valued real-functions-valued rational-functions-valued integer-functions-valued natural-functions-valued set is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty V32() FinSequence-like FinSubsequence-like FinSequence-membered complex-yielding ext-real-valued real-valued natural-valued Function-yielding V178() V195() V196() V197() V198() V199() V200() V201() complex-functions-membered ext-real-functions-membered real-functions-membered rational-functions-membered integer-functions-membered natural-functions-membered complex-functions-valued ext-real-functions-valued real-functions-valued rational-functions-valued integer-functions-valued natural-functions-valued set

1 is non empty complex ordinal natural real integer non irrational ext-real positive non negative V195() V196() V197() V198() V199() V200() Element of NAT

{{},1} is non empty set

[:NAT,REAL:] is Relation-like complex-yielding ext-real-valued real-valued set

bool [:NAT,REAL:] is set

[:NAT,COMPLEX:] is Relation-like complex-yielding set

bool [:NAT,COMPLEX:] is set

[:1,1:] is Relation-like RAT -valued INT -valued complex-yielding ext-real-valued real-valued natural-valued set

bool [:1,1:] is set

[:[:1,1:],1:] is Relation-like RAT -valued INT -valued complex-yielding ext-real-valued real-valued natural-valued set

bool [:[:1,1:],1:] is set

[:[:1,1:],REAL:] is Relation-like complex-yielding ext-real-valued real-valued set

bool [:[:1,1:],REAL:] is set

2 is non empty complex ordinal natural real integer non irrational ext-real positive non negative V195() V196() V197() V198() V199() V200() Element of NAT

[:2,2:] is Relation-like RAT -valued INT -valued complex-yielding ext-real-valued real-valued natural-valued set

[:[:2,2:],REAL:] is Relation-like complex-yielding ext-real-valued real-valued set

bool [:[:2,2:],REAL:] is set

TOP-REAL 2 is non empty non trivial V47() TopSpace-like V89() V117() V118() V119() V120() V121() V122() V123() strict complex-functions-membered real-functions-membered having_trivial_Fundamental_Group RLTopStruct

the carrier of (TOP-REAL 2) is functional non empty non trivial V32() complex-functions-membered ext-real-functions-membered real-functions-membered set

3 is non empty complex ordinal natural real integer non irrational ext-real positive non negative V195() V196() V197() V198() V199() V200() Element of NAT

TOP-REAL 3 is non empty non trivial V47() TopSpace-like V89() V117() V118() V119() V120() V121() V122() V123() strict complex-functions-membered real-functions-membered having_trivial_Fundamental_Group RLTopStruct

the carrier of (TOP-REAL 3) is functional non empty non trivial V32() complex-functions-membered ext-real-functions-membered real-functions-membered set

INT.Group is non empty non trivial V47() V91() L9()

addint is Relation-like [:INT,INT:] -defined RAT -valued INT -valued Function-like total quasi_total complex-yielding ext-real-valued real-valued Element of bool [:[:INT,INT:],INT:]

G9(INT,addint) is V91() L9()

the carrier of INT.Group is non empty non trivial V32() set

I[01] is non empty strict TopSpace-like V224() V231() pathwise_connected connected TopStruct

the carrier of I[01] is non empty V195() V196() V197() set

RealSpace is strict V231() MetrStruct

[:I[01],I[01]:] is non empty strict TopSpace-like TopStruct

the carrier of [:I[01],I[01]:] is non empty set

K708() is non empty strict TopSpace-like V231() pathwise_connected V240() connected SubSpace of R^1

the carrier of K708() is non empty V195() V196() V197() set

bool the carrier of K708() is V74() set

bool (bool the carrier of K708()) is set

Tunit_circle 2 is non empty TopSpace-like V241() complex-functions-membered real-functions-membered SubSpace of TOP-REAL 2

0. (TOP-REAL 2) is Relation-like NAT -defined Function-like V32() V39(2) zero FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL 2)

the ZeroF of (TOP-REAL 2) is Relation-like NAT -defined Function-like V32() V39(2) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL 2)

Tcircle ((0. (TOP-REAL 2)),1) is non empty strict TopSpace-like pathwise_connected V241() complex-functions-membered real-functions-membered connected SubSpace of TOP-REAL 2

Sphere ((0. (TOP-REAL 2)),1) is functional non empty closed V214( TOP-REAL 2) complex-functions-membered ext-real-functions-membered real-functions-membered Element of bool the carrier of (TOP-REAL 2)

bool the carrier of (TOP-REAL 2) is V74() set

(TOP-REAL 2) | (Sphere ((0. (TOP-REAL 2)),1)) is non empty strict TopSpace-like complex-functions-membered real-functions-membered SubSpace of TOP-REAL 2

the carrier of (Tunit_circle 2) is functional non empty complex-functions-membered ext-real-functions-membered real-functions-membered set

[: the carrier of K708(), the carrier of (Tunit_circle 2):] is Relation-like set

bool [: the carrier of K708(), the carrier of (Tunit_circle 2):] is set

CircleMap is Relation-like the carrier of K708() -defined the carrier of K708() -defined the carrier of (Tunit_circle 2) -valued the carrier of (Tunit_circle 2) -valued Function-like non empty total total quasi_total quasi_total onto continuous Function-yielding V178() complex-functions-valued ext-real-functions-valued real-functions-valued Element of bool [: the carrier of K708(), the carrier of (Tunit_circle 2):]

c[10] is Relation-like Function-like complex-yielding ext-real-valued real-valued Element of the carrier of (Tunit_circle 2)

0 is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty complex ordinal natural real integer non irrational V32() FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative complex-yielding ext-real-valued real-valued natural-valued Function-yielding V178() V195() V196() V197() V198() V199() V200() V201() complex-functions-membered ext-real-functions-membered real-functions-membered rational-functions-membered integer-functions-membered natural-functions-membered complex-functions-valued ext-real-functions-valued real-functions-valued rational-functions-valued integer-functions-valued natural-functions-valued Element of NAT

|[1,0]| is Relation-like NAT -defined NAT -defined Function-like non empty V32() V39(2) V39(2) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL 2)

<*1*> is Relation-like NAT -defined Function-like non empty V32() V39(1) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued set

[1,1] is set

{1,1} is non empty V195() V196() V197() V198() V199() V200() set

{1} is non empty V195() V196() V197() V198() V199() V200() set

{{1,1},{1}} is non empty set

{[1,1]} is Relation-like Function-like non empty set

<*0*> is Relation-like NAT -defined Function-like non empty V32() V39(1) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued set

[1,0] is set

{1,0} is non empty V195() V196() V197() V198() V199() V200() set

{{1,0},{1}} is non empty set

{[1,0]} is Relation-like Function-like non empty set

<*1*> ^ <*0*> is Relation-like NAT -defined NAT -defined Function-like non empty V32() V39(1 + 1) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued set

1 + 1 is non empty complex ordinal natural real integer non irrational ext-real positive non negative V195() V196() V197() V198() V199() V200() Element of NAT

Topen_unit_circle c[10] is non empty strict TopSpace-like V245( Tunit_circle 2) complex-functions-membered real-functions-membered SubSpace of Tunit_circle 2

the carrier of (Topen_unit_circle c[10]) is functional non empty complex-functions-membered ext-real-functions-membered real-functions-membered set

].0,1.[ is non empty V195() V196() V197() open Element of bool REAL

R^1 ].0,1.[ is non empty open V195() V196() V197() Element of bool the carrier of K708()

K708() | (R^1 ].0,1.[) is non empty strict TopSpace-like V231() V245(K708()) V245(K708()) SubSpace of K708()

the carrier of (K708() | (R^1 ].0,1.[)) is non empty V195() V196() V197() set

[: the carrier of (Topen_unit_circle c[10]), the carrier of (K708() | (R^1 ].0,1.[)):] is Relation-like complex-yielding ext-real-valued real-valued set

bool [: the carrier of (Topen_unit_circle c[10]), the carrier of (K708() | (R^1 ].0,1.[)):] is set

c[-10] is Relation-like Function-like complex-yielding ext-real-valued real-valued Element of the carrier of (Tunit_circle 2)

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

|[(- 1),0]| is Relation-like NAT -defined NAT -defined Function-like non empty V32() V39(2) V39(2) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL 2)

<*(- 1)*> is Relation-like NAT -defined Function-like non empty V32() V39(1) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued set

[1,(- 1)] is set

{1,(- 1)} is non empty V195() V196() V197() V198() V199() set

{{1,(- 1)},{1}} is non empty set

{[1,(- 1)]} is Relation-like Function-like non empty set

<*(- 1)*> ^ <*0*> is Relation-like NAT -defined NAT -defined Function-like non empty V32() V39(1 + 1) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued set

Topen_unit_circle c[-10] is non empty strict TopSpace-like V245( Tunit_circle 2) complex-functions-membered real-functions-membered SubSpace of Tunit_circle 2

the carrier of (Topen_unit_circle c[-10]) is functional non empty complex-functions-membered ext-real-functions-membered real-functions-membered set

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

2 " is non empty complex real ext-real positive non negative set

1 * (2 ") is non empty complex real ext-real positive non negative set

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

3 * (2 ") is non empty complex real ext-real positive non negative set

].(1 / 2),(3 / 2).[ is non empty V195() V196() V197() open Element of bool REAL

R^1 ].(1 / 2),(3 / 2).[ is non empty open V195() V196() V197() Element of bool the carrier of K708()

K708() | (R^1 ].(1 / 2),(3 / 2).[) is non empty strict TopSpace-like V231() V245(K708()) V245(K708()) SubSpace of K708()

the carrier of (K708() | (R^1 ].(1 / 2),(3 / 2).[)) is non empty V195() V196() V197() set

[: the carrier of (Topen_unit_circle c[-10]), the carrier of (K708() | (R^1 ].(1 / 2),(3 / 2).[)):] is Relation-like complex-yielding ext-real-valued real-valued set

bool [: the carrier of (Topen_unit_circle c[-10]), the carrier of (K708() | (R^1 ].(1 / 2),(3 / 2).[)):] is set

[: the carrier of I[01], the carrier of K708():] is Relation-like complex-yielding ext-real-valued real-valued set

bool [: the carrier of I[01], the carrier of K708():] is set

R^1 0 is complex real ext-real Element of the carrier of K708()

[: the carrier of I[01], the carrier of (Tunit_circle 2):] is Relation-like set

bool [: the carrier of I[01], the carrier of (Tunit_circle 2):] is set

K684((Tunit_circle 2),c[10]) is non empty non trivial V47() V91() L9()

the carrier of K684((Tunit_circle 2),c[10]) is non empty non trivial V32() set

[: the carrier of INT.Group, the carrier of K684((Tunit_circle 2),c[10]):] is Relation-like set

bool [: the carrier of INT.Group, the carrier of K684((Tunit_circle 2),c[10]):] is set

[: the carrier of I[01], the carrier of I[01]:] is Relation-like complex-yielding ext-real-valued real-valued set

bool [: the carrier of I[01], the carrier of I[01]:] is set

bool the carrier of [:I[01],I[01]:] is V74() set

[: the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2):] is Relation-like set

bool [: the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2):] is set

the carrier of R^1 is non empty V195() V196() V197() set

[: the carrier of (TOP-REAL 2), the carrier of R^1:] is Relation-like complex-yielding ext-real-valued real-valued set

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

K942() is set

{{}} is functional non empty complex-functions-membered set

{{}} * is functional non empty FinSequence-membered M29({{}})

[:({{}} *),{{}}:] is Relation-like set

bool [:({{}} *),{{}}:] is set

PFuncs (({{}} *),{{}}) is set

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

PI * (2 ") is non empty complex real ext-real positive non negative set

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

[.(- (PI / 2)),(PI / 2).] is V195() V196() V197() closed Element of bool REAL

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

[.(PI / 2),((3 / 2) * PI).] is V195() V196() V197() closed Element of bool REAL

[.(- (PI / 2)),0.] is V195() V196() V197() closed Element of bool REAL

[.0,(PI / 2).] is V195() V196() V197() closed Element of bool REAL

[.(PI / 2),PI.] is V195() V196() V197() closed Element of bool REAL

[.PI,((3 / 2) * PI).] is V195() V196() V197() closed Element of bool REAL

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

[.((3 / 2) * PI),(2 * PI).] is V195() V196() V197() closed Element of bool REAL

].(- (PI / 2)),(PI / 2).[ is V195() V196() V197() open Element of bool REAL

].(PI / 2),((3 / 2) * PI).[ is V195() V196() V197() open Element of bool REAL

].(- (PI / 2)),0.[ is V195() V196() V197() open Element of bool REAL

].0,(PI / 2).[ is V195() V196() V197() open Element of bool REAL

].(PI / 2),PI.[ is V195() V196() V197() open Element of bool REAL

].PI,((3 / 2) * PI).[ is V195() V196() V197() open Element of bool REAL

].((3 / 2) * PI),(2 * PI).[ is V195() V196() V197() open Element of bool REAL

[.0,PI.] is V195() V196() V197() closed Element of bool REAL

[.PI,(2 * PI).] is V195() V196() V197() closed Element of bool REAL

].0,PI.[ is V195() V196() V197() open Element of bool REAL

].PI,(2 * PI).[ is V195() V196() V197() open Element of bool REAL

sin is Relation-like REAL -defined REAL -valued Function-like non empty total quasi_total complex-yielding ext-real-valued real-valued continuous Element of bool [:REAL,REAL:]

dom sin is non empty V195() V196() V197() Element of bool REAL

cos is Relation-like REAL -defined REAL -valued Function-like non empty total quasi_total complex-yielding ext-real-valued real-valued continuous Element of bool [:REAL,REAL:]

dom cos is non empty V195() V196() V197() Element of bool REAL

cos 0 is complex real ext-real Element of REAL

sin 0 is complex real ext-real Element of REAL

[#] REAL is V195() V196() V197() closed open Element of bool REAL

R^1 ([#] REAL) is open closed V195() V196() V197() Element of bool the carrier of K708()

K708() | (R^1 ([#] REAL)) is strict TopSpace-like closed V231() V245(K708()) SubSpace of K708()

[: the carrier of K708(), the carrier of K708():] is Relation-like complex-yielding ext-real-valued real-valued set

bool [: the carrier of K708(), the carrier of K708():] is set

Ciso is Relation-like the carrier of INT.Group -defined the carrier of K684((Tunit_circle 2),c[10]) -valued Function-like one-to-one non empty total quasi_total onto bijective Element of bool [: the carrier of INT.Group, the carrier of K684((Tunit_circle 2),c[10]):]

K681((Tunit_circle 2),c[10]) is set

K680((Tunit_circle 2),c[10],c[10]) is set

EqRel ((Tunit_circle 2),c[10]) is Relation-like K681((Tunit_circle 2),c[10]) -defined K681((Tunit_circle 2),c[10]) -valued Element of bool [:K681((Tunit_circle 2),c[10]),K681((Tunit_circle 2),c[10]):]

[:K681((Tunit_circle 2),c[10]),K681((Tunit_circle 2),c[10]):] is Relation-like set

bool [:K681((Tunit_circle 2),c[10]),K681((Tunit_circle 2),c[10]):] is set

EqRel ((Tunit_circle 2),c[10],c[10]) is Relation-like K680((Tunit_circle 2),c[10],c[10]) -defined K680((Tunit_circle 2),c[10],c[10]) -valued Element of bool [:K680((Tunit_circle 2),c[10],c[10]),K680((Tunit_circle 2),c[10],c[10]):]

[:K680((Tunit_circle 2),c[10],c[10]),K680((Tunit_circle 2),c[10],c[10]):] is Relation-like set

bool [:K680((Tunit_circle 2),c[10],c[10]),K680((Tunit_circle 2),c[10],c[10]):] is set

absreal is Relation-like REAL -defined REAL -valued Function-like non empty total quasi_total complex-yielding ext-real-valued real-valued Element of bool [:REAL,REAL:]

sqrreal is Relation-like REAL -defined REAL -valued Function-like non empty total quasi_total complex-yielding ext-real-valued real-valued Element of bool [:REAL,REAL:]

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

bool the carrier of R^1 is V74() set

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

0. (TOP-REAL 3) is Relation-like NAT -defined Function-like V32() V39(3) zero FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL 3)

the ZeroF of (TOP-REAL 3) is Relation-like NAT -defined Function-like V32() V39(3) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL 3)

|[0,0,0]| is Relation-like NAT -defined Function-like non empty V32() V39(3) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL 3)

<*0*> ^ <*0*> is Relation-like NAT -defined Function-like non empty V32() V39(1 + 1) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued set

(<*0*> ^ <*0*>) ^ <*0*> is Relation-like NAT -defined Function-like non empty V32() V39((1 + 1) + 1) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued set

(1 + 1) + 1 is non empty complex ordinal natural real integer non irrational ext-real positive non negative V195() V196() V197() V198() V199() V200() Element of NAT

[.0,1.] is V195() V196() V197() closed Element of bool REAL

0[01] is complex real ext-real Element of the carrier of I[01]

1[01] is complex real ext-real Element of the carrier of I[01]

+infty is non empty non real ext-real positive non negative set

-infty is non empty non real ext-real non positive negative set

Seg 3 is non empty V32() V39(3) V195() V196() V197() V198() V199() V200() Element of bool NAT

{ b

{1,2,3} is V195() V196() V197() V198() V199() V200() set

1r is complex Element of COMPLEX

Re 1r is complex real ext-real Element of REAL

Im 1r is complex real ext-real Element of REAL

<i> is complex Element of COMPLEX

(0,1) --> (0,1) is Relation-like REAL -defined {0,1} -defined REAL -valued Function-like non empty total quasi_total complex-yielding ext-real-valued real-valued Element of bool [:{0,1},REAL:]

{0,1} is non empty V195() V196() V197() V198() V199() V200() set

[:{0,1},REAL:] is Relation-like complex-yielding ext-real-valued real-valued set

bool [:{0,1},REAL:] is set

0 .--> 0 is Relation-like REAL -defined {0} -defined RAT -valued INT -valued Function-like one-to-one constant trivial complex-yielding ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing Function-yielding V178() set

{0} is functional non empty V195() V196() V197() V198() V199() V200() complex-functions-membered set

{0} --> 0 is Relation-like non non-empty {0} -defined RAT -valued INT -valued {0} -valued Function-like constant non empty total quasi_total complex-yielding ext-real-valued real-valued natural-valued Function-yielding V178() complex-functions-valued Element of bool [:{0},{0}:]

[:{0},{0}:] is Relation-like RAT -valued INT -valued complex-yielding ext-real-valued real-valued natural-valued set

bool [:{0},{0}:] is set

1 .--> 1 is Relation-like REAL -defined {1} -defined RAT -valued INT -valued Function-like one-to-one constant trivial complex-yielding ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing set

{1} --> 1 is Relation-like non-empty {1} -defined RAT -valued INT -valued {1} -valued Function-like constant non empty total quasi_total complex-yielding ext-real-valued real-valued natural-valued Element of bool [:{1},{1}:]

[:{1},{1}:] is Relation-like RAT -valued INT -valued complex-yielding ext-real-valued real-valued natural-valued set

bool [:{1},{1}:] is set

(0 .--> 0) +* (1 .--> 1) is Relation-like REAL -defined RAT -valued INT -valued Function-like complex-yielding ext-real-valued real-valued natural-valued set

|.0.| is complex real non irrational ext-real Element of REAL

Re 0 is complex real ext-real Element of REAL

(Re 0) ^2 is complex real ext-real non negative Element of REAL

(Re 0) * (Re 0) is complex real ext-real non negative set

Im 0 is complex real ext-real Element of REAL

(Im 0) ^2 is complex real ext-real non negative Element of REAL

(Im 0) * (Im 0) is complex real ext-real non negative set

((Re 0) ^2) + ((Im 0) ^2) is complex real ext-real non negative Element of REAL

sqrt (((Re 0) ^2) + ((Im 0) ^2)) is complex real ext-real non negative Element of REAL

diffreal is Relation-like [:REAL,REAL:] -defined REAL -valued Function-like total quasi_total complex-yielding ext-real-valued real-valued Element of bool [:[:REAL,REAL:],REAL:]

K143() is Relation-like [:REAL,REAL:] -defined REAL -valued Function-like total quasi_total complex-yielding ext-real-valued real-valued Element of bool [:[:REAL,REAL:],REAL:]

id REAL is Relation-like REAL -defined REAL -valued Function-like one-to-one non empty total quasi_total complex-yielding ext-real-valued real-valued increasing non-decreasing Element of bool [:REAL,REAL:]

K141() is Relation-like REAL -defined REAL -valued Function-like non empty total quasi_total complex-yielding ext-real-valued real-valued Element of bool [:REAL,REAL:]

K738(REAL,K143(),(id REAL),K141()) is Relation-like [:REAL,REAL:] -defined REAL -valued Function-like total quasi_total complex-yielding ext-real-valued real-valued Element of bool [:[:REAL,REAL:],REAL:]

IRRAT is non empty V195() V196() V197() Element of bool REAL

<i> is complex set

Euclid 2 is non empty strict Reflexive discerning symmetric triangle complex-functions-membered real-functions-membered MetrStruct

REAL 2 is functional non empty FinSequence-membered complex-functions-membered ext-real-functions-membered real-functions-membered M29( REAL )

K513(2,REAL) is functional non empty FinSequence-membered M29( REAL )

Pitag_dist 2 is Relation-like [:(REAL 2),(REAL 2):] -defined REAL -valued Function-like total quasi_total complex-yielding ext-real-valued real-valued Element of bool [:[:(REAL 2),(REAL 2):],REAL:]

[:(REAL 2),(REAL 2):] is Relation-like set

[:[:(REAL 2),(REAL 2):],REAL:] is Relation-like complex-yielding ext-real-valued real-valued set

bool [:[:(REAL 2),(REAL 2):],REAL:] is set

MetrStruct(# (REAL 2),(Pitag_dist 2) #) is strict MetrStruct

TopSpaceMetr (Euclid 2) is non empty strict TopSpace-like TopStruct

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

[: the carrier of (TopSpaceMetr (Euclid 2)), the carrier of (TopSpaceMetr (Euclid 2)):] is Relation-like set

bool [: the carrier of (TopSpaceMetr (Euclid 2)), the carrier of (TopSpaceMetr (Euclid 2)):] is set

0c is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty complex V32() FinSequence-like FinSubsequence-like FinSequence-membered complex-yielding ext-real-valued real-valued natural-valued Function-yielding V178() V195() V196() V197() V198() V199() V200() V201() complex-functions-membered ext-real-functions-membered real-functions-membered rational-functions-membered integer-functions-membered natural-functions-membered complex-functions-valued ext-real-functions-valued real-functions-valued rational-functions-valued integer-functions-valued natural-functions-valued Element of COMPLEX

cpx2euc 0c is Relation-like NAT -defined Function-like V32() V39(2) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL 2)

Re 0c is complex real ext-real Element of REAL

Im 0c is complex real ext-real Element of REAL

|[(Re 0c),(Im 0c)]| is Relation-like NAT -defined Function-like non empty V32() V39(2) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL 2)

<*(Re 0c)*> is Relation-like NAT -defined Function-like non empty V32() V39(1) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued set

[1,(Re 0c)] is set

{1,(Re 0c)} is non empty V195() V196() V197() set

{{1,(Re 0c)},{1}} is non empty set

{[1,(Re 0c)]} is Relation-like Function-like non empty set

<*(Im 0c)*> is Relation-like NAT -defined Function-like non empty V32() V39(1) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued set

[1,(Im 0c)] is set

{1,(Im 0c)} is non empty V195() V196() V197() set

{{1,(Im 0c)},{1}} is non empty set

{[1,(Im 0c)]} is Relation-like Function-like non empty set

<*(Re 0c)*> ^ <*(Im 0c)*> is Relation-like NAT -defined Function-like non empty V32() V39(1 + 1) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued set

euc2cpx (0. (TOP-REAL 2)) is complex Element of COMPLEX

(0. (TOP-REAL 2)) `1 is complex real ext-real Element of REAL

K382((0. (TOP-REAL 2)),1) is complex real ext-real Element of REAL

(0. (TOP-REAL 2)) `2 is complex real ext-real Element of REAL

K382((0. (TOP-REAL 2)),2) is complex real ext-real Element of REAL

((0. (TOP-REAL 2)) `2) * <i> is complex set

((0. (TOP-REAL 2)) `1) + (((0. (TOP-REAL 2)) `2) * <i>) is complex set

[: the carrier of R^1, the carrier of R^1:] is Relation-like complex-yielding ext-real-valued real-valued set

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

|[0,0]| is Relation-like NAT -defined Function-like non empty V32() V39(2) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL 2)

[.0,1.[ is V195() V196() V197() Element of bool REAL

R^1 [.0,1.[ is V195() V196() V197() Element of bool the carrier of K708()

R^1 | (R^1 ].0,1.[) is non empty strict TopSpace-like V231() V245( R^1 ) V245(K708()) SubSpace of R^1

[: the carrier of I[01], the carrier of I[01]:] is Relation-like complex-yielding ext-real-valued real-valued set

TC2 is complex real ext-real set

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

TC2 is complex real ext-real set

TC2 + (1 / 2) is complex real ext-real set

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

Q + (1 / 2) is non empty complex real ext-real positive non negative set

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

TC2 is complex real ext-real Element of IRRAT

TC2 is complex real ext-real set

TC2 ^2 is complex real ext-real non negative set

TC2 * TC2 is complex real ext-real non negative set

TC3 is complex real ext-real set

TC3 ^2 is complex real ext-real non negative set

TC3 * TC3 is complex real ext-real non negative set

- TC3 is complex real ext-real set

- (- TC3) is complex real ext-real set

- Q is complex real integer ext-real non positive set

TC2 is complex real ext-real set

frac TC2 is complex real ext-real Element of REAL

[\TC2/] is complex real integer ext-real set

TC2 - [\TC2/] is complex real ext-real set

- [\TC2/] is complex real integer ext-real set

TC2 + (- [\TC2/]) is complex real ext-real set

TC3 is complex real ext-real set

frac TC3 is complex real ext-real Element of REAL

[\TC3/] is complex real integer ext-real set

TC3 - [\TC3/] is complex real ext-real set

- [\TC3/] is complex real integer ext-real set

TC3 + (- [\TC3/]) is complex real ext-real set

TC2 - TC3 is complex real ext-real set

- TC3 is complex real ext-real set

TC2 + (- TC3) is complex real ext-real set

frac (TC2 - TC3) is complex real ext-real Element of REAL

[\(TC2 - TC3)/] is complex real integer ext-real set

(TC2 - TC3) - [\(TC2 - TC3)/] is complex real ext-real set

- [\(TC2 - TC3)/] is complex real integer ext-real set

(TC2 - TC3) + (- [\(TC2 - TC3)/]) is complex real ext-real set

(frac TC2) - (frac TC3) is complex real ext-real Element of REAL

- (frac TC3) is complex real ext-real set

(frac TC2) + (- (frac TC3)) is complex real ext-real set

(TC2 - TC3) - (frac TC2) is complex real ext-real Element of REAL

- (frac TC2) is complex real ext-real set

(TC2 - TC3) + (- (frac TC2)) is complex real ext-real set

((TC2 - TC3) - (frac TC2)) + (frac TC3) is complex real ext-real Element of REAL

TC2 - (frac TC2) is complex real ext-real Element of REAL

TC2 + (- (frac TC2)) is complex real ext-real set

TC3 - (frac TC3) is complex real ext-real Element of REAL

TC3 + (- (frac TC3)) is complex real ext-real set

(TC2 - (frac TC2)) - (TC3 - (frac TC3)) is complex real ext-real Element of REAL

- (TC3 - (frac TC3)) is complex real ext-real set

(TC2 - (frac TC2)) + (- (TC3 - (frac TC3))) is complex real ext-real set

- (frac TC2) is complex real ext-real Element of REAL

(- (frac TC2)) + (frac TC3) is complex real ext-real Element of REAL

(TC2 - TC3) + ((- (frac TC2)) + (frac TC3)) is complex real ext-real Element of REAL

- (frac TC3) is complex real ext-real Element of REAL

(- (frac TC3)) + (frac TC3) is complex real ext-real Element of REAL

(TC2 - TC3) + Q is complex real ext-real set

(TC2 - TC3) - ((frac TC2) - (frac TC3)) is complex real ext-real Element of REAL

- ((frac TC2) - (frac TC3)) is complex real ext-real set

(TC2 - TC3) + (- ((frac TC2) - (frac TC3))) is complex real ext-real set

1 + (frac TC3) is complex real ext-real Element of REAL

(frac TC2) + Q is complex real ext-real Element of REAL

(TC2 - TC3) - 1 is complex real ext-real Element of REAL

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

(TC2 - TC3) + (- 1) is complex real ext-real set

TC2 is complex real ext-real set

frac TC2 is complex real ext-real Element of REAL

[\TC2/] is complex real integer ext-real set

TC2 - [\TC2/] is complex real ext-real set

- [\TC2/] is complex real integer ext-real set

TC2 + (- [\TC2/]) is complex real ext-real set

TC3 is complex real ext-real set

frac TC3 is complex real ext-real Element of REAL

[\TC3/] is complex real integer ext-real set

TC3 - [\TC3/] is complex real ext-real set

- [\TC3/] is complex real integer ext-real set

TC3 + (- [\TC3/]) is complex real ext-real set

TC2 - TC3 is complex real ext-real set

- TC3 is complex real ext-real set

TC2 + (- TC3) is complex real ext-real set

frac (TC2 - TC3) is complex real ext-real Element of REAL

[\(TC2 - TC3)/] is complex real integer ext-real set

(TC2 - TC3) - [\(TC2 - TC3)/] is complex real ext-real set

- [\(TC2 - TC3)/] is complex real integer ext-real set

(TC2 - TC3) + (- [\(TC2 - TC3)/]) is complex real ext-real set

(frac TC2) - (frac TC3) is complex real ext-real Element of REAL

- (frac TC3) is complex real ext-real set

(frac TC2) + (- (frac TC3)) is complex real ext-real set

((frac TC2) - (frac TC3)) + 1 is complex real ext-real Element of REAL

(TC2 - TC3) - (frac TC2) is complex real ext-real Element of REAL

- (frac TC2) is complex real ext-real set

(TC2 - TC3) + (- (frac TC2)) is complex real ext-real set

((TC2 - TC3) - (frac TC2)) + (frac TC3) is complex real ext-real Element of REAL

(((TC2 - TC3) - (frac TC2)) + (frac TC3)) - 1 is complex real ext-real Element of REAL

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

(((TC2 - TC3) - (frac TC2)) + (frac TC3)) + (- 1) is complex real ext-real set

TC2 - (frac TC2) is complex real ext-real Element of REAL

TC2 + (- (frac TC2)) is complex real ext-real set

TC3 - (frac TC3) is complex real ext-real Element of REAL

TC3 + (- (frac TC3)) is complex real ext-real set

(TC2 - (frac TC2)) - (TC3 - (frac TC3)) is complex real ext-real Element of REAL

- (TC3 - (frac TC3)) is complex real ext-real set

(TC2 - (frac TC2)) + (- (TC3 - (frac TC3))) is complex real ext-real set

((TC2 - (frac TC2)) - (TC3 - (frac TC3))) - 1 is complex real ext-real Element of REAL

((TC2 - (frac TC2)) - (TC3 - (frac TC3))) + (- 1) is complex real ext-real set

- (frac TC2) is complex real ext-real Element of REAL

(- (frac TC2)) + (frac TC3) is complex real ext-real Element of REAL

((- (frac TC2)) + (frac TC3)) - 1 is complex real ext-real Element of REAL

((- (frac TC2)) + (frac TC3)) + (- 1) is complex real ext-real set

(TC2 - TC3) + (((- (frac TC2)) + (frac TC3)) - 1) is complex real ext-real Element of REAL

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

1 + (- 1) is complex real integer ext-real set

(frac TC3) - 1 is complex real ext-real Element of REAL

(frac TC3) + (- 1) is complex real ext-real set

((frac TC3) - 1) - (frac TC2) is complex real ext-real Element of REAL

((frac TC3) - 1) + (- (frac TC2)) is complex real ext-real set

(frac TC2) - (frac TC2) is complex real ext-real Element of REAL

(frac TC2) + (- (frac TC2)) is complex real ext-real set

(TC2 - TC3) + Q is complex real ext-real set

(TC2 - TC3) - 1 is complex real ext-real Element of REAL

(TC2 - TC3) + (- 1) is complex real ext-real set

((TC2 - TC3) - 1) - ((frac TC2) - (frac TC3)) is complex real ext-real Element of REAL

- ((frac TC2) - (frac TC3)) is complex real ext-real set

((TC2 - TC3) - 1) + (- ((frac TC2) - (frac TC3))) is complex real ext-real set

((TC2 - TC3) - 1) - Q is complex real ext-real Element of REAL

- Q is complex real integer ext-real non positive set

((TC2 - TC3) - 1) + (- Q) is complex real ext-real set

TC2 is complex real ext-real set

frac TC2 is complex real ext-real Element of REAL

[\TC2/] is complex real integer ext-real set

TC2 - [\TC2/] is complex real ext-real set

- [\TC2/] is complex real integer ext-real set

TC2 + (- [\TC2/]) is complex real ext-real set

TC3 is complex real ext-real set

TC2 - TC3 is complex real ext-real set

- TC3 is complex real ext-real set

TC2 + (- TC3) is complex real ext-real set

frac (TC2 - TC3) is complex real ext-real Element of REAL

[\(TC2 - TC3)/] is complex real integer ext-real set

(TC2 - TC3) - [\(TC2 - TC3)/] is complex real ext-real set

- [\(TC2 - TC3)/] is complex real integer ext-real set

(TC2 - TC3) + (- [\(TC2 - TC3)/]) is complex real ext-real set

frac TC3 is complex real ext-real Element of REAL

[\TC3/] is complex real integer ext-real set

TC3 - [\TC3/] is complex real ext-real set

- [\TC3/] is complex real integer ext-real set

TC3 + (- [\TC3/]) is complex real ext-real set

(frac TC2) - (frac TC3) is complex real ext-real Element of REAL

- (frac TC3) is complex real ext-real set

(frac TC2) + (- (frac TC3)) is complex real ext-real set

((frac TC2) - (frac TC3)) + Q is complex real ext-real Element of REAL

((frac TC2) - (frac TC3)) + 1 is complex real ext-real Element of REAL

TC2 is complex real ext-real set

sin TC2 is complex real ext-real set

TC2 / (2 * PI) is complex real ext-real Element of COMPLEX

(2 * PI) " is non empty complex real ext-real positive non negative set

TC2 * ((2 * PI) ") is complex real ext-real set

[\(TC2 / (2 * PI))/] is complex real integer ext-real set

(2 * PI) * [\(TC2 / (2 * PI))/] is complex real ext-real Element of REAL

PI + ((2 * PI) * [\(TC2 / (2 * PI))/]) is complex real ext-real Element of REAL

- [\(TC2 / (2 * PI))/] is complex real integer ext-real set

(2 * PI) * (- [\(TC2 / (2 * PI))/]) is complex real ext-real Element of REAL

((2 * PI) * (- [\(TC2 / (2 * PI))/])) + TC2 is complex real ext-real Element of REAL

QQ is complex real ext-real set

sin QQ is complex real ext-real set

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

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

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

(3 * PI) * (2 ") is non empty complex real ext-real positive non negative set

TC2 is complex real ext-real set

cos TC2 is complex real ext-real set

TC2 / (2 * PI) is complex real ext-real Element of COMPLEX

(2 * PI) " is non empty complex real ext-real positive non negative set

TC2 * ((2 * PI) ") is complex real ext-real set

[\(TC2 / (2 * PI))/] is complex real integer ext-real set

(2 * PI) * [\(TC2 / (2 * PI))/] is complex real ext-real Element of REAL

(PI / 2) + ((2 * PI) * [\(TC2 / (2 * PI))/]) is complex real ext-real Element of REAL

((3 * PI) / 2) + ((2 * PI) * [\(TC2 / (2 * PI))/]) is complex real ext-real Element of REAL

- [\(TC2 / (2 * PI))/] is complex real integer ext-real set

(2 * PI) * (- [\(TC2 / (2 * PI))/]) is complex real ext-real Element of REAL

((2 * PI) * (- [\(TC2 / (2 * PI))/])) + TC2 is complex real ext-real Element of REAL

QQ is complex real ext-real set

cos QQ is complex real ext-real set

TC2 is complex real ext-real set

sin TC2 is complex real ext-real set

TC2 / (2 * PI) is complex real ext-real Element of COMPLEX

(2 * PI) " is non empty complex real ext-real positive non negative set

TC2 * ((2 * PI) ") is complex real ext-real set

[\(TC2 / (2 * PI))/] is complex real integer ext-real set

(2 * PI) * [\(TC2 / (2 * PI))/] is complex real ext-real Element of REAL

PI + ((2 * PI) * [\(TC2 / (2 * PI))/]) is complex real ext-real Element of REAL

2 * [\(TC2 / (2 * PI))/] is complex real integer ext-real even Element of REAL

PI * (2 * [\(TC2 / (2 * PI))/]) is complex real ext-real Element of REAL

1 + (2 * [\(TC2 / (2 * PI))/]) is non empty complex real integer ext-real non even Element of REAL

PI * (1 + (2 * [\(TC2 / (2 * PI))/])) is non empty complex real ext-real Element of REAL

TC2 is complex real ext-real set

cos TC2 is complex real ext-real set

TC2 / (2 * PI) is complex real ext-real Element of COMPLEX

(2 * PI) " is non empty complex real ext-real positive non negative set

TC2 * ((2 * PI) ") is complex real ext-real set

[\(TC2 / (2 * PI))/] is complex real integer ext-real set

(2 * PI) * [\(TC2 / (2 * PI))/] is complex real ext-real Element of REAL

(PI / 2) + ((2 * PI) * [\(TC2 / (2 * PI))/]) is complex real ext-real Element of REAL

((3 * PI) / 2) + ((2 * PI) * [\(TC2 / (2 * PI))/]) is complex real ext-real Element of REAL

2 * [\(TC2 / (2 * PI))/] is complex real integer ext-real even Element of REAL

PI * (2 * [\(TC2 / (2 * PI))/]) is complex real ext-real Element of REAL

(PI / 2) + (PI * (2 * [\(TC2 / (2 * PI))/])) is complex real ext-real Element of REAL

1 + (2 * [\(TC2 / (2 * PI))/]) is non empty complex real integer ext-real non even Element of REAL

PI * (1 + (2 * [\(TC2 / (2 * PI))/])) is non empty complex real ext-real Element of REAL

(PI / 2) + (PI * (1 + (2 * [\(TC2 / (2 * PI))/]))) is complex real ext-real Element of REAL

TC2 is complex real ext-real set

TC3 is complex real ext-real set

TC2 - TC3 is complex real ext-real set

- TC3 is complex real ext-real set

TC2 + (- TC3) is complex real ext-real set

(TC2 - TC3) / 2 is complex real ext-real Element of COMPLEX

(TC2 - TC3) * (2 ") is complex real ext-real set

sin ((TC2 - TC3) / 2) is complex real ext-real set

QQ is complex real integer ext-real set

PI * QQ is complex real ext-real Element of REAL

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

TC3 + ((2 * PI) * QQ) is complex real ext-real Element of REAL

TC2 is complex real ext-real set

sin TC2 is complex real ext-real set

TC3 is complex real ext-real set

sin TC3 is complex real ext-real set

PI - TC3 is complex real ext-real Element of REAL

- TC3 is complex real ext-real set

PI + (- TC3) is complex real ext-real set

(sin TC2) - (sin TC3) is complex real ext-real set

- (sin TC3) is complex real ext-real set

(sin TC2) + (- (sin TC3)) is complex real ext-real set

TC2 + TC3 is complex real ext-real set

(TC2 + TC3) / 2 is complex real ext-real Element of COMPLEX

(TC2 + TC3) * (2 ") is complex real ext-real set

cos ((TC2 + TC3) / 2) is complex real ext-real set

TC2 - TC3 is complex real ext-real set

TC2 + (- TC3) is complex real ext-real set

(TC2 - TC3) / 2 is complex real ext-real Element of COMPLEX

(TC2 - TC3) * (2 ") is complex real ext-real set

sin ((TC2 - TC3) / 2) is complex real ext-real set

(cos ((TC2 + TC3) / 2)) * (sin ((TC2 - TC3) / 2)) is complex real ext-real set

2 * ((cos ((TC2 + TC3) / 2)) * (sin ((TC2 - TC3) / 2))) is complex real ext-real Element of REAL

QQ is complex real integer ext-real set

PI * QQ is complex real ext-real Element of REAL

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

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

(PI - TC3) + ((2 * PI) * QQ) is complex real ext-real Element of REAL

TC2 is complex real ext-real set

cos TC2 is complex real ext-real set

TC3 is complex real ext-real set

cos TC3 is complex real ext-real set

- TC3 is complex real ext-real set

(cos TC2) - (cos TC3) is complex real ext-real set

- (cos TC3) is complex real ext-real set

(cos TC2) + (- (cos TC3)) is complex real ext-real set

TC2 + TC3 is complex real ext-real set

(TC2 + TC3) / 2 is complex real ext-real Element of COMPLEX

(TC2 + TC3) * (2 ") is complex real ext-real set

sin ((TC2 + TC3) / 2) is complex real ext-real set

TC2 - TC3 is complex real ext-real set

TC2 + (- TC3) is complex real ext-real set

(TC2 - TC3) / 2 is complex real ext-real Element of COMPLEX

(TC2 - TC3) * (2 ") is complex real ext-real set

sin ((TC2 - TC3) / 2) is complex real ext-real set

(sin ((TC2 + TC3) / 2)) * (sin ((TC2 - TC3) / 2)) is complex real ext-real set

2 * ((sin ((TC2 + TC3) / 2)) * (sin ((TC2 - TC3) / 2))) is complex real ext-real Element of REAL

- (2 * ((sin ((TC2 + TC3) / 2)) * (sin ((TC2 - TC3) / 2)))) is complex real ext-real Element of REAL

QQ is complex real integer ext-real set

PI * QQ is complex real ext-real Element of REAL

(TC2 + TC3) - TC3 is complex real ext-real set

(TC2 + TC3) + (- TC3) is complex real ext-real set

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

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

((2 * PI) * QQ) + (- TC3) is complex real ext-real set

TC2 is complex real ext-real set

sin TC2 is complex real ext-real set

cos TC2 is complex real ext-real set

TC3 is complex real ext-real set

sin TC3 is complex real ext-real set

cos TC3 is complex real ext-real set

PI - TC3 is complex real ext-real Element of REAL

- TC3 is complex real ext-real set

PI + (- TC3) is complex real ext-real set

QQ is complex real integer ext-real set

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

TC3 + ((2 * PI) * QQ) is complex real ext-real Element of REAL

(PI - TC3) + ((2 * PI) * QQ) is complex real ext-real Element of REAL

RR is complex real integer ext-real set

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

TC3 + ((2 * PI) * RR) is complex real ext-real Element of REAL

(- TC3) + ((2 * PI) * RR) is complex real ext-real Element of REAL

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

PI " is non empty complex real ext-real positive non negative set

PI * (PI ") is non empty complex real ext-real positive non negative set

RR - QQ is complex real integer ext-real set

- QQ is complex real integer ext-real set

RR + (- QQ) is complex real integer ext-real set

2 * (RR - QQ) is complex real integer ext-real even Element of REAL

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

(PI * (2 * (RR - QQ))) / PI is complex real ext-real Element of COMPLEX

(PI * (2 * (RR - QQ))) * (PI ") is complex real ext-real set

TC2 is complex real integer ext-real set

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

TC3 is complex set

|.TC3.| is complex real ext-real Element of REAL

Re TC3 is complex real ext-real Element of REAL

(Re TC3) ^2 is complex real ext-real non negative Element of REAL

(Re TC3) * (Re TC3) is complex real ext-real non negative set

Im TC3 is complex real ext-real Element of REAL

(Im TC3) ^2 is complex real ext-real non negative Element of REAL

(Im TC3) * (Im TC3) is complex real ext-real non negative set

((Re TC3) ^2) + ((Im TC3) ^2) is complex real ext-real non negative Element of REAL

sqrt (((Re TC3) ^2) + ((Im TC3) ^2)) is complex real ext-real non negative Element of REAL

Arg TC3 is complex real ext-real Element of REAL

QQ is complex set

|.QQ.| is complex real ext-real Element of REAL

Re QQ is complex real ext-real Element of REAL

(Re QQ) ^2 is complex real ext-real non negative Element of REAL

(Re QQ) * (Re QQ) is complex real ext-real non negative set

Im QQ is complex real ext-real Element of REAL

(Im QQ) ^2 is complex real ext-real non negative Element of REAL

(Im QQ) * (Im QQ) is complex real ext-real non negative set

((Re QQ) ^2) + ((Im QQ) ^2) is complex real ext-real non negative Element of REAL

sqrt (((Re QQ) ^2) + ((Im QQ) ^2)) is complex real ext-real non negative Element of REAL

Arg QQ is complex real ext-real Element of REAL

(Arg QQ) + ((2 * PI) * TC2) is complex real ext-real Element of REAL

cos (Arg QQ) is complex real ext-real Element of REAL

cos ((Arg QQ) + ((2 * PI) * TC2)) is complex real ext-real Element of REAL

sin (Arg QQ) is complex real ext-real Element of REAL

sin ((Arg QQ) + ((2 * PI) * TC2)) is complex real ext-real Element of REAL

cos (Arg TC3) is complex real ext-real Element of REAL

|.TC3.| * (cos (Arg TC3)) is complex real ext-real Element of REAL

sin (Arg TC3) is complex real ext-real Element of REAL

|.TC3.| * (sin (Arg TC3)) is complex real ext-real Element of REAL

(|.TC3.| * (sin (Arg TC3))) * <i> is complex set

(|.TC3.| * (cos (Arg TC3))) + ((|.TC3.| * (sin (Arg TC3))) * <i>) is complex set

|.QQ.| * (cos (Arg QQ)) is complex real ext-real Element of REAL

|.QQ.| * (sin (Arg QQ)) is complex real ext-real Element of REAL

(|.QQ.| * (sin (Arg QQ))) * <i> is complex set

(|.QQ.| * (cos (Arg QQ))) + ((|.QQ.| * (sin (Arg QQ))) * <i>) is complex set

TC2 is Relation-like Function-like one-to-one complex-yielding set

TC3 is complex set

TC3 + TC2 is Relation-like Function-like complex-yielding set

QQ is set

dom (TC3 + TC2) is set

(TC3 + TC2) . QQ is complex set

RR is set

(TC3 + TC2) . RR is complex set

dom TC2 is set

TC2 . QQ is complex set

(TC2 . QQ) + TC3 is complex set

TC2 . RR is complex set

(TC2 . RR) + TC3 is complex set

TC2 is Relation-like Function-like one-to-one complex-yielding set

TC3 is complex set

TC2 - TC3 is Relation-like Function-like complex-yielding set

- TC3 is complex set

(- TC3) + TC2 is Relation-like Function-like one-to-one complex-yielding set

TC2 is Relation-like NAT -defined Function-like V32() FinSequence-like FinSubsequence-like complex-yielding set

- TC2 is Relation-like NAT -defined Function-like V32() FinSequence-like FinSubsequence-like complex-yielding set

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

(- 1) * TC2 is Relation-like NAT -defined Function-like V32() FinSequence-like FinSubsequence-like complex-yielding set

len (- TC2) is complex ordinal natural real integer non irrational ext-real non negative V195() V196() V197() V198() V199() V200() Element of NAT

len TC2 is complex ordinal natural real integer non irrational ext-real non negative V195() V196() V197() V198() V199() V200() Element of NAT

Seg (len (- TC2)) is V32() V39( len (- TC2)) V195() V196() V197() V198() V199() V200() Element of bool NAT

{ b

dom (- TC2) is V195() V196() V197() V198() V199() V200() Element of bool NAT

dom TC2 is V195() V196() V197() V198() V199() V200() Element of bool NAT

Seg (len TC2) is V32() V39( len TC2) V195() V196() V197() V198() V199() V200() Element of bool NAT

{ b

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

0* TC2 is Relation-like NAT -defined REAL -valued Function-like V32() V39(TC2) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of REAL TC2

REAL TC2 is functional non empty FinSequence-membered complex-functions-membered ext-real-functions-membered real-functions-membered M29( REAL )

K513(TC2,REAL) is functional non empty FinSequence-membered M29( REAL )

K514(REAL,TC2,0) is Relation-like empty-yielding NAT -defined REAL -valued Function-like V32() V39(TC2) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of K513(TC2,REAL)

- (0* TC2) is Relation-like NAT -defined REAL -valued Function-like V32() V39(TC2) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of REAL TC2

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

(- 1) * (0* TC2) is Relation-like NAT -defined Function-like V32() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued set

(- 1) multreal is Relation-like REAL -defined REAL -valued Function-like non empty total quasi_total complex-yielding ext-real-valued real-valued Element of bool [:REAL,REAL:]

K145() is Relation-like [:REAL,REAL:] -defined REAL -valued Function-like total quasi_total complex-yielding ext-real-valued real-valued Element of bool [:[:REAL,REAL:],REAL:]

K145() [;] ((- 1),(id REAL)) is Relation-like Function-like set

dom (id REAL) is non empty set

(dom (id REAL)) --> (- 1) is Relation-like non-empty dom (id REAL) -defined INT -valued Function-like constant non empty total complex-yielding ext-real-valued real-valued set

{(- 1)} is non empty V195() V196() V197() V198() V199() set

[:(dom (id REAL)),{(- 1)}:] is Relation-like RAT -valued INT -valued complex-yielding ext-real-valued real-valued set

K254(((dom (id REAL)) --> (- 1)),(id REAL)) is Relation-like Function-like set

K254(((dom (id REAL)) --> (- 1)),(id REAL)) (#) K145() is Relation-like REAL -valued Function-like complex-yielding ext-real-valued real-valued set

(0* TC2) (#) ((- 1) multreal) is Relation-like NAT -defined REAL -valued Function-like V32() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued set

(0* TC2) (#) K141() is Relation-like NAT -defined REAL -valued Function-like V32() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued set

len (0* TC2) is complex ordinal natural real integer non irrational ext-real non negative V195() V196() V197() V198() V199() V200() Element of NAT

len (- (0* TC2)) is complex ordinal natural real integer non irrational ext-real non negative V195() V196() V197() V198() V199() V200() Element of NAT

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

(- (0* TC2)) . RR is complex real ext-real set

(0* TC2) . RR is complex real ext-real set

- Q is complex real integer ext-real non positive set

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

0* TC2 is Relation-like NAT -defined REAL -valued Function-like V32() V39(TC2) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of REAL TC2

REAL TC2 is functional non empty FinSequence-membered complex-functions-membered ext-real-functions-membered real-functions-membered M29( REAL )

K513(TC2,REAL) is functional non empty FinSequence-membered M29( REAL )

K514(REAL,TC2,0) is Relation-like empty-yielding NAT -defined REAL -valued Function-like V32() V39(TC2) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of K513(TC2,REAL)

TC3 is Relation-like Function-like complex-yielding set

- TC3 is Relation-like Function-like complex-yielding set

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

(- 1) * TC3 is Relation-like Function-like complex-yielding set

- (- TC3) is Relation-like Function-like complex-yielding set

(- 1) * (- TC3) is Relation-like Function-like complex-yielding set

- (0* TC2) is Relation-like NAT -defined REAL -valued Function-like V32() V39(TC2) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of REAL TC2

(- 1) * (0* TC2) is Relation-like NAT -defined Function-like V32() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued set

(- 1) multreal is Relation-like REAL -defined REAL -valued Function-like non empty total quasi_total complex-yielding ext-real-valued real-valued Element of bool [:REAL,REAL:]

K145() is Relation-like [:REAL,REAL:] -defined REAL -valued Function-like total quasi_total complex-yielding ext-real-valued real-valued Element of bool [:[:REAL,REAL:],REAL:]

K145() [;] ((- 1),(id REAL)) is Relation-like Function-like set

dom (id REAL) is non empty set

(dom (id REAL)) --> (- 1) is Relation-like non-empty dom (id REAL) -defined INT -valued Function-like constant non empty total complex-yielding ext-real-valued real-valued set

{(- 1)} is non empty V195() V196() V197() V198() V199() set

[:(dom (id REAL)),{(- 1)}:] is Relation-like RAT -valued INT -valued complex-yielding ext-real-valued real-valued set

K254(((dom (id REAL)) --> (- 1)),(id REAL)) is Relation-like Function-like set

K254(((dom (id REAL)) --> (- 1)),(id REAL)) (#) K145() is Relation-like REAL -valued Function-like complex-yielding ext-real-valued real-valued set

(0* TC2) (#) ((- 1) multreal) is Relation-like NAT -defined REAL -valued Function-like V32() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued set

(0* TC2) (#) K141() is Relation-like NAT -defined REAL -valued Function-like V32() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued set

TC2 is complex real ext-real set

TC2 ^2 is complex real ext-real non negative set

TC2 * TC2 is complex real ext-real non negative set

TC3 is complex real ext-real set

TC3 ^2 is complex real ext-real non negative set

TC3 * TC3 is complex real ext-real non negative set

QQ is complex real ext-real set

<*TC2,TC3,QQ*> is Relation-like NAT -defined Function-like non empty V32() V39(3) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued set

<*TC2*> is Relation-like NAT -defined Function-like non empty V32() V39(1) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued set

[1,TC2] is set

{1,TC2} is non empty V195() V196() V197() set

{{1,TC2},{1}} is non empty set

{[1,TC2]} is Relation-like Function-like non empty set

<*TC3*> is Relation-like NAT -defined Function-like non empty V32() V39(1) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued set

[1,TC3] is set

{1,TC3} is non empty V195() V196() V197() set

{{1,TC3},{1}} is non empty set

{[1,TC3]} is Relation-like Function-like non empty set

<*TC2*> ^ <*TC3*> is Relation-like NAT -defined Function-like non empty V32() V39(1 + 1) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued set

<*QQ*> is Relation-like NAT -defined Function-like non empty V32() V39(1) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued set

[1,QQ] is set

{1,QQ} is non empty V195() V196() V197() set

{{1,QQ},{1}} is non empty set

{[1,QQ]} is Relation-like Function-like non empty set

(<*TC2*> ^ <*TC3*>) ^ <*QQ*> is Relation-like NAT -defined Function-like non empty V32() V39((1 + 1) + 1) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued set

sqr <*TC2,TC3,QQ*> is Relation-like NAT -defined REAL -valued Function-like V32() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL

mlt (<*TC2,TC3,QQ*>,<*TC2,TC3,QQ*>) is Relation-like NAT -defined Function-like V32() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued set

K145() is Relation-like [:REAL,REAL:] -defined REAL -valued Function-like total quasi_total complex-yielding ext-real-valued real-valued Element of bool [:[:REAL,REAL:],REAL:]

K145() .: (<*TC2,TC3,QQ*>,<*TC2,TC3,QQ*>) is Relation-like Function-like set

K254(<*TC2,TC3,QQ*>,<*TC2,TC3,QQ*>) is Relation-like Function-like set

K254(<*TC2,TC3,QQ*>,<*TC2,TC3,QQ*>) (#) K145() is Relation-like REAL -valued Function-like complex-yielding ext-real-valued real-valued set

<*TC2,TC3,QQ*> (#) sqrreal is Relation-like NAT -defined REAL -valued Function-like V32() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued set

QQ ^2 is complex real ext-real non negative set

QQ * QQ is complex real ext-real non negative set

<*(TC2 ^2),(TC3 ^2),(QQ ^2)*> is Relation-like NAT -defined Function-like non empty V32() V39(3) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued set

<*(TC2 ^2)*> is Relation-like NAT -defined Function-like non empty V32() V39(1) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued set

[1,(TC2 ^2)] is set

{1,(TC2 ^2)} is non empty V195() V196() V197() set

{{1,(TC2 ^2)},{1}} is non empty set

{[1,(TC2 ^2)]} is Relation-like Function-like non empty set

<*(TC3 ^2)*> is Relation-like NAT -defined Function-like non empty V32() V39(1) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued set

[1,(TC3 ^2)] is set

{1,(TC3 ^2)} is non empty V195() V196() V197() set

{{1,(TC3 ^2)},{1}} is non