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
{ b1 where b1 is complex ordinal natural real integer non irrational ext-real non negative V195() V196() V197() V198() V199() V200() Element of NAT : ( 1 <= b1 & b1 <= 3 ) } is set
{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
{ b1 where b1 is complex ordinal natural real integer non irrational ext-real non negative V195() V196() V197() V198() V199() V200() Element of NAT : ( 1 <= b1 & b1 <= len (- TC2) ) } is set
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
{ b1 where b1 is complex ordinal natural real integer non irrational ext-real non negative V195() V196() V197() V198() V199() V200() Element of NAT : ( 1 <= b1 & b1 <= len TC2 ) } is 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)
- (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