:: TOPREALC semantic presentation

bool REAL is non trivial non finite set

bool omega is non trivial non finite set
bool NAT is non trivial non finite set
COMPLEX is non empty non trivial non finite complex-membered V132() set

bool is non trivial non finite set
K282() is non empty strict multMagma
the carrier of K282() is non empty set
K287() is non empty strict V107() V108() V109() V111() V148() V149() V150() V151() V152() V153() multMagma
K288() is non empty strict V109() V111() V151() V152() V153() M13(K287())
K289() is non empty strict V107() V109() V111() V151() V152() V153() V154() M16(K287(),K288())
K291() is non empty strict V107() V109() V111() multMagma
K292() is non empty strict V107() V109() V111() V154() M13(K291())

bool [:1,1:] is finite V49() set

bool [:[:1,1:],1:] is finite V49() set

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

bool is non trivial non finite set

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

the carrier of () is non empty set

Family_open_set RealSpace is Element of bool (bool the carrier of RealSpace)
bool the carrier of RealSpace is set
bool (bool the carrier of RealSpace) is set
TopStruct(# the carrier of RealSpace, #) is strict TopStruct
K603() is non empty strict TopSpace-like real-membered SubSpace of R^1
[:K603(),K603():] is non empty strict TopSpace-like TopStruct
the carrier of [:K603(),K603():] is non empty set
K605() is non empty strict TopSpace-like real-membered V244() SubSpace of R^1

bool the carrier of K605() is set
bool (bool the carrier of K605()) is set
Tunit_circle 2 is non empty TopSpace-like V245() SubSpace of TOP-REAL 2

Tcircle ((0. ()),1) is non empty strict TopSpace-like V245() SubSpace of TOP-REAL 2
Sphere ((0. ()),1) is non empty closed V215( TOP-REAL 2) Element of bool the carrier of ()
bool the carrier of () is set
() | (Sphere ((0. ()),1)) is non empty strict TopSpace-like SubSpace of TOP-REAL 2
the carrier of () is non empty set
[: the carrier of K605(), the carrier of ():] is Relation-like set
bool [: the carrier of K605(), the carrier of ():] is set
CircleMap is Relation-like the carrier of K605() -defined the carrier of K605() -defined the carrier of () -valued the carrier of () -valued Function-like non empty total total V18( the carrier of K605(), the carrier of ()) V18( the carrier of K605(), the carrier of ()) V19( the carrier of ()) continuous Element of bool [: the carrier of K605(), the carrier of ():]
c[10] is Element of the carrier of ()

[1,1] is set

{{1,1},{1}} is non empty finite V49() set

[1,0] is set

{{1,0},{1}} is non empty finite V49() set

the carrier of is non empty set

K605() | (R^1 ].0,1.[) is non empty strict TopSpace-like real-membered SubSpace of K605()
the carrier of (K605() | (R^1 ].0,1.[)) is non empty complex-membered ext-real-membered real-membered set
[: the carrier of , the carrier of (K605() | (R^1 ].0,1.[)):] is Relation-like complex-valued ext-real-valued real-valued set
bool [: the carrier of , the carrier of (K605() | (R^1 ].0,1.[)):] is set
c[-10] is Element of the carrier of ()
K504(1) is non empty ext-real non positive negative complex real Element of REAL

[1,K504(1)] is set

{{1,K504(1)},{1}} is non empty finite V49() set

the carrier of is non empty set
K513(1,2) is non empty ext-real positive non negative complex real Element of REAL
2 " is non empty ext-real positive non negative complex real set
1 * (2 ") is non empty ext-real positive non negative complex real set

K513(3,2) is non empty ext-real positive non negative complex real Element of REAL
3 * (2 ") is non empty ext-real positive non negative complex real set
].K513(1,2),K513(3,2).[ is non empty complex-membered ext-real-membered real-membered open Element of bool REAL
R^1 ].K513(1,2),K513(3,2).[ is non empty complex-membered ext-real-membered real-membered open Element of bool the carrier of K605()
K605() | (R^1 ].K513(1,2),K513(3,2).[) is non empty strict TopSpace-like real-membered SubSpace of K605()
the carrier of (K605() | (R^1 ].K513(1,2),K513(3,2).[)) is non empty complex-membered ext-real-membered real-membered set
[: the carrier of , the carrier of (K605() | (R^1 ].K513(1,2),K513(3,2).[)):] is Relation-like complex-valued ext-real-valued real-valued set
bool [: the carrier of , the carrier of (K605() | (R^1 ].K513(1,2),K513(3,2).[)):] is set
K759() is set

bool [:(),:] is set

bool is non trivial non finite set

bool is non trivial non finite set

bool is non trivial non finite set

bool is non trivial non finite set

bool is non trivial non finite set

bool is non trivial non finite set

{ } is set

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

bool [:[:(),():],REAL:] is set
MetrStruct(# (),() #) is strict MetrStruct

the carrier of () is non empty set
Family_open_set () is Element of bool (bool the carrier of ())
bool the carrier of () is set
bool (bool the carrier of ()) is set
TopStruct(# the carrier of (),() #) is non empty strict TopStruct

the carrier of () is non empty set

r is set

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

m * m is non empty ext-real positive non negative complex real set

K857() .: (m,m) is Relation-like Function-like set

sqrt (Sum (sqr m)) is ext-real complex real Element of REAL
m is complex set
r is complex set
m + r is complex set

(m (#) T) + (r (#) T) is Relation-like Function-like complex-valued set
dom ((m + r) (#) T) is set
dom T is set
dom (m (#) T) is set
dom (r (#) T) is set
dom ((m (#) T) + (r (#) T)) is set
(dom (m (#) T)) /\ (dom (r (#) T)) is set
f is set
((m + r) (#) T) . f is complex set
((m (#) T) + (r (#) T)) . f is complex set
T . f is complex set
(T . f) * (m + r) is complex set
(T . f) * m is complex set
(T . f) * r is complex set
((T . f) * m) + ((T . f) * r) is complex set
(m (#) T) . f is complex set
((m (#) T) . f) + ((T . f) * r) is complex set
(r (#) T) . f is complex set
((m (#) T) . f) + ((r (#) T) . f) is complex set
m is complex set
r is complex set
m - r is complex set
- r is complex set
m + (- r) is complex set

(m (#) T) - (r (#) T) is Relation-like Function-like complex-valued set

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

(m (#) T) + (- (r (#) T)) is Relation-like Function-like complex-valued set

(m (#) T) + ((- r) (#) T) is Relation-like Function-like complex-valued set
m is complex set

1 / m is complex set
m " is complex set
1 * (m ") is complex set

(r (/) m) + (T (/) m) is Relation-like Function-like complex-valued set

(1 / m) (#) (r + T) is Relation-like Function-like complex-valued set
dom ((r (/) m) + (T (/) m)) is set
dom (r (/) m) is set
dom (T (/) m) is set
(dom (r (/) m)) /\ (dom (T (/) m)) is set
dom r is set
dom T is set
dom ((r + T) (/) m) is set
dom (r + T) is set
(dom r) /\ (dom T) is set
f is set
((r (/) m) + (T (/) m)) . f is complex set
((r + T) (/) m) . f is complex set
(r + T) . f is complex set
((r + T) . f) / m is complex Element of COMPLEX
((r + T) . f) * (m ") is complex set
r . f is complex set
T . f is complex set
(r . f) + (T . f) is complex set
((r . f) + (T . f)) / m is complex Element of COMPLEX
((r . f) + (T . f)) * (m ") is complex set
(r . f) / m is complex Element of COMPLEX
(r . f) * (m ") is complex set
(T . f) / m is complex Element of COMPLEX
(T . f) * (m ") is complex set
((r . f) / m) + ((T . f) / m) is complex Element of COMPLEX
(T (/) m) . f is complex set
((r . f) / m) + ((T (/) m) . f) is complex set
(r (/) m) . f is complex set
((r (/) m) . f) + ((T (/) m) . f) is complex set
m is complex set

1 / m is complex set
m " is complex set
1 * (m ") is complex set

(r (/) m) - (T (/) m) is Relation-like Function-like complex-valued set

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

(r (/) m) + (- (T (/) m)) is Relation-like Function-like complex-valued set

(1 / m) (#) (r - T) is Relation-like Function-like complex-valued set

(1 / m) (#) (- T) is Relation-like Function-like complex-valued set
(r (/) m) + ((- T) (/) m) is Relation-like Function-like complex-valued set
m is complex set
r is complex set
m * r is complex set

1 / m is complex set
m " is complex set
1 * (m ") is complex set

1 / r is complex set
r " is complex set
1 * (r ") is complex set

(T (/) m) - (f (/) r) is Relation-like Function-like complex-valued set

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

(T (/) m) + (- (f (/) r)) is Relation-like Function-like complex-valued set

(r (#) T) - (m (#) f) is Relation-like Function-like complex-valued set

(r (#) T) + (- (m (#) f)) is Relation-like Function-like complex-valued set
((r (#) T) - (m (#) f)) (/) (m * r) is Relation-like Function-like complex-valued set
1 / (m * r) is complex set
(m * r) " is complex set
1 * ((m * r) ") is complex set
(1 / (m * r)) (#) ((r (#) T) - (m (#) f)) is Relation-like Function-like complex-valued set
dom (T (/) m) is set
dom T is set
dom (f (/) r) is set
dom f is set
dom (r (#) T) is set
dom (m (#) f) is set
dom ((T (/) m) - (f (/) r)) is set
(dom (T (/) m)) /\ (dom (f (/) r)) is set
dom ((r (#) T) - (m (#) f)) is set
(dom (r (#) T)) /\ (dom (m (#) f)) is set
dom (((r (#) T) - (m (#) f)) (/) (m * r)) is set
g is set
((T (/) m) - (f (/) r)) . g is complex set
(((r (#) T) - (m (#) f)) (/) (m * r)) . g is complex set
(T (/) m) . g is complex set
(f (/) r) . g is complex set
((T (/) m) . g) - ((f (/) r) . g) is complex set
- ((f (/) r) . g) is complex set
((T (/) m) . g) + (- ((f (/) r) . g)) is complex set
T . g is complex set
(T . g) / m is complex Element of COMPLEX
(T . g) * (m ") is complex set
((T . g) / m) - ((f (/) r) . g) is complex set
((T . g) / m) + (- ((f (/) r) . g)) is complex set
f . g is complex set
(f . g) / r is complex Element of COMPLEX
(f . g) * (r ") is complex set
((T . g) / m) - ((f . g) / r) is complex Element of COMPLEX
- ((f . g) / r) is complex set
((T . g) / m) + (- ((f . g) / r)) is complex set
(T . g) * r is complex set
(f . g) * m is complex set
((T . g) * r) - ((f . g) * m) is complex set
- ((f . g) * m) is complex set
((T . g) * r) + (- ((f . g) * m)) is complex set
(((T . g) * r) - ((f . g) * m)) / (m * r) is complex Element of COMPLEX
(((T . g) * r) - ((f . g) * m)) * ((m * r) ") is complex set
(m (#) f) . g is complex set
((T . g) * r) - ((m (#) f) . g) is complex set
- ((m (#) f) . g) is complex set
((T . g) * r) + (- ((m (#) f) . g)) is complex set
(((T . g) * r) - ((m (#) f) . g)) / (m * r) is complex Element of COMPLEX
(((T . g) * r) - ((m (#) f) . g)) * ((m * r) ") is complex set
(r (#) T) . g is complex set
((r (#) T) . g) - ((m (#) f) . g) is complex set
((r (#) T) . g) + (- ((m (#) f) . g)) is complex set
(((r (#) T) . g) - ((m (#) f) . g)) / (m * r) is complex Element of COMPLEX
(((r (#) T) . g) - ((m (#) f) . g)) * ((m * r) ") is complex set
((r (#) T) - (m (#) f)) . g is complex set
(((r (#) T) - (m (#) f)) . g) / (m * r) is complex Element of COMPLEX
(((r (#) T) - (m (#) f)) . g) * ((m * r) ") is complex set
m is complex set

1 / m is complex set
m " is complex set
1 * (m ") is complex set

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

(r (/) m) + (- T) is Relation-like Function-like complex-valued set

r + (- (m (#) T)) is Relation-like Function-like complex-valued set
(r - (m (#) T)) (/) m is Relation-like Function-like complex-valued set
(1 / m) (#) (r - (m (#) T)) is Relation-like Function-like complex-valued set
dom ((r (/) m) - T) is set
dom (r (/) m) is set
dom T is set
(dom (r (/) m)) /\ (dom T) is set
dom r is set
(dom r) /\ (dom T) is set
dom (r - (m (#) T)) is set
dom (m (#) T) is set
(dom r) /\ (dom (m (#) T)) is set
dom ((r - (m (#) T)) (/) m) is set
f is set
((r (/) m) - T) . f is complex set
((r - (m (#) T)) (/) m) . f is complex set
(r (/) m) . f is complex set
T . f is complex set
((r (/) m) . f) - (T . f) is complex set
- (T . f) is complex set
((r (/) m) . f) + (- (T . f)) is complex set
r . f is complex set
(r . f) / m is complex Element of COMPLEX
(r . f) * (m ") is complex set
((r . f) / m) - (T . f) is complex set
((r . f) / m) + (- (T . f)) is complex set
m * (T . f) is complex set
(m * (T . f)) / m is complex Element of COMPLEX
(m * (T . f)) * (m ") is complex set
((r . f) / m) - ((m * (T . f)) / m) is complex Element of COMPLEX
- ((m * (T . f)) / m) is complex set
((r . f) / m) + (- ((m * (T . f)) / m)) is complex set
(m (#) T) . f is complex set
((m (#) T) . f) / m is complex Element of COMPLEX
((m (#) T) . f) * (m ") is complex set
((r . f) / m) - (((m (#) T) . f) / m) is complex Element of COMPLEX
- (((m (#) T) . f) / m) is complex set
((r . f) / m) + (- (((m (#) T) . f) / m)) is complex set
(r . f) - ((m (#) T) . f) is complex set
- ((m (#) T) . f) is complex set
(r . f) + (- ((m (#) T) . f)) is complex set
((r . f) - ((m (#) T) . f)) / m is complex Element of COMPLEX
((r . f) - ((m (#) T) . f)) * (m ") is complex set
(r - (m (#) T)) . f is complex set
((r - (m (#) T)) . f) / m is complex Element of COMPLEX
((r - (m (#) T)) . f) * (m ") is complex set
m is complex set
r is complex set
m - r is complex set
- r is complex set
m + (- r) is complex set

(m (#) T) - (r (#) T) is Relation-like Function-like complex-valued set

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

(m (#) T) + (- (r (#) T)) is Relation-like Function-like complex-valued set
dom ((m (#) T) - (r (#) T)) is set
dom (m (#) T) is set
dom (r (#) T) is set
(dom (m (#) T)) /\ (dom (r (#) T)) is set
dom T is set
(dom T) /\ (dom (r (#) T)) is set
(dom T) /\ (dom T) is set
dom ((m - r) (#) T) is set
f is set
((m - r) (#) T) . f is complex set
((m (#) T) - (r (#) T)) . f is complex set
T . f is complex set
(m - r) * (T . f) is complex set
m * (T . f) is complex set
r * (T . f) is complex set
(m * (T . f)) - (r * (T . f)) is complex set
- (r * (T . f)) is complex set
(m * (T . f)) + (- (r * (T . f))) is complex set
(r (#) T) . f is complex set
(m * (T . f)) - ((r (#) T) . f) is complex set
- ((r (#) T) . f) is complex set
(m * (T . f)) + (- ((r (#) T) . f)) is complex set
(m (#) T) . f is complex set
((m (#) T) . f) - ((r (#) T) . f) is complex set
((m (#) T) . f) + (- ((r (#) T) . f)) is complex set

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

(m - r) (#) (m - r) is Relation-like Function-like complex-valued set

(r - m) (#) (r - m) is Relation-like Function-like complex-valued set
dom (m - r) is set
dom m is set
dom r is set
(dom m) /\ (dom r) is set
dom (r - m) is set
(dom r) /\ (dom m) is set
dom ((m - r) ^2) is set
dom ((r - m) ^2) is set
T is set
((m - r) ^2) . T is complex set
((r - m) ^2) . T is complex set
(m - r) . T is complex set
m . T is complex set
r . T is complex set
(m . T) - (r . T) is complex set
- (r . T) is complex set
(m . T) + (- (r . T)) is complex set
(r - m) . T is complex set
(r . T) - (m . T) is complex set
- (m . T) is complex set
(r . T) + (- (m . T)) is complex set
((m - r) . T) * ((m - r) . T) is complex set
((r - m) . T) * ((r - m) . T) is complex set
m is complex set
m ^2 is complex set
m * m is complex set

1 / m is complex set
m " is complex set
1 * (m ") is complex set

(r (/) m) (#) (r (/) m) is Relation-like Function-like complex-valued set

1 / (m ^2) is complex set
(m ^2) " is complex set
1 * ((m ^2) ") is complex set
(1 / (m ^2)) (#) (r ^2) is Relation-like Function-like complex-valued set
dom ((r (/) m) ^2) is set
dom (r (/) m) is set
dom r is set
dom (r ^2) is set
dom ((r ^2) (/) (m ^2)) is set
T is set
((r (/) m) ^2) . T is complex set
((r ^2) (/) (m ^2)) . T is complex set
(r (/) m) . T is complex set
((r (/) m) . T) ^2 is complex set
((r (/) m) . T) * ((r (/) m) . T) is complex set
r . T is complex set
(r . T) / m is complex Element of COMPLEX
(r . T) * (m ") is complex set
((r . T) / m) ^2 is complex Element of COMPLEX
((r . T) / m) * ((r . T) / m) is complex set
(r . T) ^2 is complex set
(r . T) * (r . T) is complex set
((r . T) ^2) / (m ^2) is complex Element of COMPLEX
((r . T) ^2) * ((m ^2) ") is complex set
(r ^2) . T is complex set
((r ^2) . T) / (m ^2) is complex Element of COMPLEX
((r ^2) . T) * ((m ^2) ") is complex set

{ } is set

bool [:(Seg m),{r}:] is finite V49() set

bool [:(Seg m),{T}:] is finite V49() set

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

K857() [;] ((- 1),()) is Relation-like Function-like set
dom () is non empty set

<:((dom ()) --> (- 1)),():> is Relation-like Function-like set

K855() .: ((m |-> r),(- (m |-> T))) is Relation-like Function-like set
<:(m |-> r),(- (m |-> T)):> is Relation-like Function-like set

K856() .: ((m |-> r),(m |-> T)) is Relation-like Function-like set
<:(m |-> r),(m |-> T):> is Relation-like Function-like set

|.((m |-> r) - (m |-> T)).| is ext-real non negative complex real Element of REAL

((m |-> r) - (m |-> T)) (#) ((m |-> r) - (m |-> T)) is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued finite m -element FinSequence-like FinSubsequence-like V268() V317() set
K857() .: (((m |-> r) - (m |-> T)),((m |-> r) - (m |-> T))) is Relation-like Function-like set
<:((m |-> r) - (m |-> T)),((m |-> r) - (m |-> T)):> is Relation-like Function-like set
<:((m |-> r) - (m |-> T)),((m |-> r) - (m |-> T)):> (#) K857() is Relation-like REAL -valued Function-like complex-valued ext-real-valued real-valued set

Sum (sqr ((m |-> r) - (m |-> T))) is ext-real complex real Element of REAL
sqrt (Sum (sqr ((m |-> r) - (m |-> T)))) is ext-real complex real Element of REAL

r + (- T) is ext-real complex real set
abs (r - T) is ext-real complex real Element of REAL
(sqrt m) * (abs (r - T)) is ext-real complex real set

bool [:(Seg m),{(r - T)}:] is finite V49() set

K857() .: ((m |-> (r - T)),(m |-> (r - T))) is Relation-like Function-like set
<:(m |-> (r - T)),(m |-> (r - T)):> is Relation-like Function-like set
<:(m |-> (r - T)),(m |-> (r - T)):> (#) K857() is Relation-like REAL -valued Function-like complex-valued ext-real-valued real-valued set

Sum (sqr (m |-> (r - T))) is ext-real complex real Element of REAL
sqrt (Sum (sqr (m |-> (r - T)))) is ext-real complex real Element of REAL
(r - T) ^2 is ext-real non negative complex real set
(r - T) * (r - T) is ext-real non negative complex real set

(Seg m) --> ((r - T) ^2) is Relation-like Seg m -defined Seg m -defined {((r - T) ^2)} -valued Function-like constant total total V18( Seg m,{((r - T) ^2)}) complex-valued ext-real-valued real-valued finite FinSequence-like FinSubsequence-like V268() V317() Element of bool [:(Seg m),{((r - T) ^2)}:]

bool [:(Seg m),{((r - T) ^2)}:] is finite V49() set
Sum (m |-> ((r - T) ^2)) is ext-real complex real set
sqrt (Sum (m |-> ((r - T) ^2))) is ext-real complex real set
m * ((r - T) ^2) is ext-real non negative complex real set
sqrt (m * ((r - T) ^2)) is ext-real non negative complex real set
sqrt ((r - T) ^2) is ext-real non negative complex real set
(sqrt m) * (sqrt ((r - T) ^2)) is ext-real non negative complex real set

r is set
T is complex set
m +* (r,T) is Relation-like Function-like set
g is set
dom (m +* (r,T)) is set
(m +* (r,T)) . g is set
dom m is set
dom m is set
m . g is complex set
dom m is set
m . g is complex set
dom m is set
m is set

{ } is set

{ } is set

bool [:(Seg r),:] is finite V49() set
T is complex set

((0* r) +* (m,T)) (#) ((0* r) +* (m,T)) is Relation-like NAT -defined Function-like complex-valued finite r -element FinSequence-like FinSubsequence-like V268() set
T ^2 is complex set
T * T is complex set

p is set
(((0* r) +* (m,T)) ^2) . p is complex set
((0* r) +* (m,(T ^2))) . p is complex set
((0* r) +* (m,T)) . p is complex set
(((0* r) +* (m,T)) . p) ^2 is complex set
(((0* r) +* (m,T)) . p) * (((0* r) +* (m,T)) . p) is complex set

m is set

{ } is set

{ } is set

bool [:(Seg r),:] is finite V49() set

|.((0* r) +* (m,T)).| is ext-real non negative complex real Element of REAL

K857() .: (((0* r) +* (m,T)),((0* r) +* (m,T))) is Relation-like Function-like set
<:((0* r) +* (m,T)),((0* r) +* (m,T)):> is Relation-like Function-like set
<:((0* r) +* (m,T)),((0* r) +* (m,T)):> (#) K857() is Relation-like REAL -valued Function-like complex-valued ext-real-valued real-valued set

Sum (sqr ((0* r) +* (m,T))) is ext-real complex real Element of REAL
sqrt (Sum (sqr ((0* r) +* (m,T)))) is ext-real complex real Element of REAL

Sum (((0* r) +* (m,T)) ^2) is ext-real complex real set
m is set

the carrier of () is non empty set

{ } is set

{ } is set

bool [:(Seg r),:] is finite V49() set

f is set
(() +* (m,0)) . f is ext-real complex real set

(() +* (m,0)) . f is ext-real complex real set

m is set

the carrier of () is non empty set

{ } is set

{ } is set

bool [:(Seg r),:] is finite V49() set

K857() .: (f,(() +* (m,T))) is Relation-like Function-like set
<:f,(() +* (m,T)):> is Relation-like Function-like set
<:f,(()