:: JORDAN24 semantic presentation

REAL is V149() V150() V151() V155() set

NAT is V149() V150() V151() V152() V153() V154() V155() Element of K6(REAL)

K6(REAL) is set

COMPLEX is V149() V155() set

K7(NAT,REAL) is V16() set

K6(K7(NAT,REAL)) is set

K7(NAT,COMPLEX) is V16() set

K6(K7(NAT,COMPLEX)) is set

K7(COMPLEX,COMPLEX) is V16() set

K6(K7(COMPLEX,COMPLEX)) is set

K7(REAL,REAL) is V16() set

K6(K7(REAL,REAL)) is set

omega is V149() V150() V151() V152() V153() V154() V155() set

K6(omega) is set

1 is non empty natural complex real ext-real positive non negative integer V102() V149() V150() V151() V152() V153() V154() Element of NAT

K7(1,1) is V16() set

K6(K7(1,1)) is set

K7(K7(1,1),1) is V16() set

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

K7(K7(1,1),REAL) is V16() set

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

K7(K7(REAL,REAL),REAL) is V16() set

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

2 is non empty natural complex real ext-real positive non negative integer V102() V149() V150() V151() V152() V153() V154() Element of NAT

K7(2,2) is V16() set

K7(K7(2,2),REAL) is V16() set

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

K6(NAT) is set

RAT is V149() V150() V151() V152() V155() set

INT is V149() V150() V151() V152() V153() V155() set

TOP-REAL 2 is non empty TopSpace-like V115() V161() V162() V163() V164() V165() V166() V167() V173() L15()

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

K453() is TopStruct

the carrier of K453() is set

RealSpace is strict MetrStruct

K458() is TopSpace-like TopStruct

the carrier of K458() is set

NonZero (TOP-REAL 2) is Element of K6( the carrier of (TOP-REAL 2))

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

[#] (TOP-REAL 2) is non empty non proper closed Element of K6( the carrier of (TOP-REAL 2))

K172((TOP-REAL 2)) is V40(2) zero V98() V141() Element of the carrier of (TOP-REAL 2)

the ZeroF of (TOP-REAL 2) is V40(2) V98() V141() Element of the carrier of (TOP-REAL 2)

{K172((TOP-REAL 2))} is non empty set

([#] (TOP-REAL 2)) \ {K172((TOP-REAL 2))} is Element of K6( the carrier of (TOP-REAL 2))

K7((NonZero (TOP-REAL 2)),(NonZero (TOP-REAL 2))) is V16() set

K6(K7((NonZero (TOP-REAL 2)),(NonZero (TOP-REAL 2)))) is set

K7( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)) is V16() set

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

{} is empty V16() non-empty empty-yielding V149() V150() V151() V152() V153() V154() V155() set

the empty V16() non-empty empty-yielding V149() V150() V151() V152() V153() V154() V155() set is empty V16() non-empty empty-yielding V149() V150() V151() V152() V153() V154() V155() set

0 is empty natural complex real ext-real non positive non negative V16() non-empty empty-yielding integer V102() V149() V150() V151() V152() V153() V154() V155() Element of NAT

Euclid 2 is non empty strict Reflexive discerning symmetric triangle MetrStruct

the carrier of (Euclid 2) is non empty set

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

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

<i> is complex Element of COMPLEX

Re 0 is complex real ext-real Element of REAL

Im 0 is complex real ext-real Element of REAL

rl is natural complex real ext-real integer V102() V149() V150() V151() V152() V153() V154() Element of NAT

TOP-REAL rl is non empty TopSpace-like V115() V161() V162() V163() V164() V165() V166() V167() V173() L15()

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

K6( the carrier of (TOP-REAL rl)) is set

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

|[(- 1),0]| is V40(2) V98() V141() Element of the carrier of (TOP-REAL 2)

|[1,0]| is V40(2) V98() V141() Element of the carrier of (TOP-REAL 2)

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

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

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

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

Family_open_set (Euclid 2) is Element of K6(K6( the carrier of (Euclid 2)))

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

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

TopStruct(# the carrier of (Euclid 2),(Family_open_set (Euclid 2)) #) is non empty strict TopStruct

S is non empty compact Element of K6( the carrier of (TOP-REAL 2))

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

K6( the carrier of (TopSpaceMetr (Euclid 2))) is set

f is Element of K6( the carrier of (TopSpaceMetr (Euclid 2)))

max_dist_max (f,f) is complex real ext-real Element of REAL

s is Element of the carrier of (Euclid 2)

s is Element of the carrier of (Euclid 2)

dist (s,s) is complex real ext-real Element of REAL

A1 is V40(2) V98() V141() Element of the carrier of (TOP-REAL 2)

A2 is V40(2) V98() V141() Element of the carrier of (TOP-REAL 2)

dist (A1,A2) is complex real ext-real Element of REAL

B1 is V40(2) V98() V141() Element of the carrier of (TOP-REAL 2)

B2 is V40(2) V98() V141() Element of the carrier of (TOP-REAL 2)

dist (B1,B2) is complex real ext-real Element of REAL

S2 is Element of the carrier of (Euclid 2)

fB is Element of the carrier of (Euclid 2)

dist (S2,fB) is complex real ext-real Element of REAL

S is non empty MetrStruct

TopSpaceMetr S is non empty strict TopSpace-like TopStruct

the carrier of S is non empty set

Family_open_set S is Element of K6(K6( the carrier of S))

K6( the carrier of S) is set

K6(K6( the carrier of S)) is set

TopStruct(# the carrier of S,(Family_open_set S) #) is non empty strict TopStruct

the carrier of (TopSpaceMetr S) is non empty set

K7( the carrier of (TopSpaceMetr S), the carrier of (TopSpaceMetr S)) is V16() set

K6(K7( the carrier of (TopSpaceMetr S), the carrier of (TopSpaceMetr S))) is set

S is non empty MetrStruct

TopSpaceMetr S is non empty strict TopSpace-like TopStruct

the carrier of S is non empty set

Family_open_set S is Element of K6(K6( the carrier of S))

K6( the carrier of S) is set

K6(K6( the carrier of S)) is set

TopStruct(# the carrier of S,(Family_open_set S) #) is non empty strict TopStruct

the carrier of (TopSpaceMetr S) is non empty set

K7( the carrier of (TopSpaceMetr S), the carrier of (TopSpaceMetr S)) is V16() set

K6(K7( the carrier of (TopSpaceMetr S), the carrier of (TopSpaceMetr S))) is set

K7( the carrier of S, the carrier of S) is V16() set

K6(K7( the carrier of S, the carrier of S)) is set

the non empty V16() V19( the carrier of S) V20( the carrier of S) Function-like V26( the carrier of S) quasi_total onto isometric Element of K6(K7( the carrier of S, the carrier of S)) is non empty V16() V19( the carrier of S) V20( the carrier of S) Function-like V26( the carrier of S) quasi_total onto isometric Element of K6(K7( the carrier of S, the carrier of S))

s is non empty V16() V19( the carrier of (TopSpaceMetr S)) V20( the carrier of (TopSpaceMetr S)) Function-like V26( the carrier of (TopSpaceMetr S)) quasi_total Element of K6(K7( the carrier of (TopSpaceMetr S), the carrier of (TopSpaceMetr S)))

S is non empty Reflexive discerning symmetric triangle MetrStruct

TopSpaceMetr S is non empty strict TopSpace-like TopStruct

the carrier of S is non empty set

Family_open_set S is Element of K6(K6( the carrier of S))

K6( the carrier of S) is set

K6(K6( the carrier of S)) is set

TopStruct(# the carrier of S,(Family_open_set S) #) is non empty strict TopStruct

the carrier of (TopSpaceMetr S) is non empty set

K7( the carrier of (TopSpaceMetr S), the carrier of (TopSpaceMetr S)) is V16() set

K6(K7( the carrier of (TopSpaceMetr S), the carrier of (TopSpaceMetr S))) is set

f is non empty V16() V19( the carrier of (TopSpaceMetr S)) V20( the carrier of (TopSpaceMetr S)) Function-like V26( the carrier of (TopSpaceMetr S)) quasi_total Element of K6(K7( the carrier of (TopSpaceMetr S), the carrier of (TopSpaceMetr S)))

K7( the carrier of S, the carrier of S) is V16() set

K6(K7( the carrier of S, the carrier of S)) is set

s is non empty V16() V19( the carrier of S) V20( the carrier of S) Function-like one-to-one V26( the carrier of S) quasi_total isometric Element of K6(K7( the carrier of S, the carrier of S))

s is Element of the carrier of (TopSpaceMetr S)

f . s is Element of the carrier of (TopSpaceMetr S)

A1 is non empty a_neighborhood of f . s

Int A1 is Element of K6( the carrier of (TopSpaceMetr S))

K6( the carrier of (TopSpaceMetr S)) is set

A2 is Element of the carrier of S

B2 is complex real ext-real set

Ball (A2,B2) is Element of K6( the carrier of S)

B1 is Element of the carrier of S

Ball (B1,B2) is Element of K6( the carrier of S)

S2 is non empty a_neighborhood of s

f .: S2 is Element of K6( the carrier of (TopSpaceMetr S))

fB is set

dom f is non empty Element of K6( the carrier of (TopSpaceMetr S))

arg is set

f . arg is set

qq is Element of the carrier of (TopSpaceMetr S)

h is Element of the carrier of S

dist (h,B1) is complex real ext-real Element of REAL

s . h is Element of the carrier of S

dist ((s . h),A2) is complex real ext-real Element of REAL

S is non empty Reflexive discerning symmetric triangle MetrStruct

TopSpaceMetr S is non empty strict TopSpace-like TopStruct

the carrier of S is non empty set

Family_open_set S is Element of K6(K6( the carrier of S))

K6( the carrier of S) is set

K6(K6( the carrier of S)) is set

TopStruct(# the carrier of S,(Family_open_set S) #) is non empty strict TopStruct

the carrier of (TopSpaceMetr S) is non empty set

K7( the carrier of (TopSpaceMetr S), the carrier of (TopSpaceMetr S)) is V16() set

K6(K7( the carrier of (TopSpaceMetr S), the carrier of (TopSpaceMetr S))) is set

f is non empty V16() V19( the carrier of (TopSpaceMetr S)) V20( the carrier of (TopSpaceMetr S)) Function-like V26( the carrier of (TopSpaceMetr S)) quasi_total Element of K6(K7( the carrier of (TopSpaceMetr S), the carrier of (TopSpaceMetr S)))

dom f is non empty Element of K6( the carrier of (TopSpaceMetr S))

K6( the carrier of (TopSpaceMetr S)) is set

[#] (TopSpaceMetr S) is non empty non proper closed Element of K6( the carrier of (TopSpaceMetr S))

rng f is non empty Element of K6( the carrier of (TopSpaceMetr S))

f " is non empty V16() V19( the carrier of (TopSpaceMetr S)) V20( the carrier of (TopSpaceMetr S)) Function-like V26( the carrier of (TopSpaceMetr S)) quasi_total Element of K6(K7( the carrier of (TopSpaceMetr S), the carrier of (TopSpaceMetr S)))

K7( the carrier of S, the carrier of S) is V16() set

K6(K7( the carrier of S, the carrier of S)) is set

s is non empty V16() V19( the carrier of S) V20( the carrier of S) Function-like one-to-one V26( the carrier of S) quasi_total isometric Element of K6(K7( the carrier of S, the carrier of S))

s is non empty V16() V19( the carrier of (TopSpaceMetr S)) V20( the carrier of (TopSpaceMetr S)) Function-like V26( the carrier of (TopSpaceMetr S)) quasi_total onto continuous (S) Element of K6(K7( the carrier of (TopSpaceMetr S), the carrier of (TopSpaceMetr S)))

<i> is complex set

S is complex real ext-real Element of REAL

f is non empty V16() V19( the carrier of (TOP-REAL 2)) V20( the carrier of (TOP-REAL 2)) Function-like V26( the carrier of (TOP-REAL 2)) quasi_total Element of K6(K7( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)))

s is V40(2) V98() V141() Element of the carrier of (TOP-REAL 2)

f . s is V40(2) V98() V141() Element of the carrier of (TOP-REAL 2)

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

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

(s `2) * <i> is complex set

(s `1) + ((s `2) * <i>) is complex set

Rotate (((s `1) + ((s `2) * <i>)),S) is complex Element of COMPLEX

|.((s `1) + ((s `2) * <i>)).| is complex real ext-real Element of REAL

Arg ((s `1) + ((s `2) * <i>)) is complex real ext-real Element of REAL

S + (Arg ((s `1) + ((s `2) * <i>))) is complex real ext-real Element of REAL

cos (S + (Arg ((s `1) + ((s `2) * <i>)))) is complex real ext-real Element of REAL

|.((s `1) + ((s `2) * <i>)).| * (cos (S + (Arg ((s `1) + ((s `2) * <i>))))) is complex real ext-real Element of REAL

sin (S + (Arg ((s `1) + ((s `2) * <i>)))) is complex real ext-real Element of REAL

|.((s `1) + ((s `2) * <i>)).| * (sin (S + (Arg ((s `1) + ((s `2) * <i>))))) is complex real ext-real Element of REAL

(|.((s `1) + ((s `2) * <i>)).| * (sin (S + (Arg ((s `1) + ((s `2) * <i>)))))) * <i> is complex set

(|.((s `1) + ((s `2) * <i>)).| * (cos (S + (Arg ((s `1) + ((s `2) * <i>)))))) + ((|.((s `1) + ((s `2) * <i>)).| * (sin (S + (Arg ((s `1) + ((s `2) * <i>)))))) * <i>) is complex set

Re (Rotate (((s `1) + ((s `2) * <i>)),S)) is complex real ext-real Element of REAL

Im (Rotate (((s `1) + ((s `2) * <i>)),S)) is complex real ext-real Element of REAL

|[(Re (Rotate (((s `1) + ((s `2) * <i>)),S))),(Im (Rotate (((s `1) + ((s `2) * <i>)),S)))]| is V40(2) V98() V141() Element of the carrier of (TOP-REAL 2)

f is non empty V16() V19( the carrier of (TOP-REAL 2)) V20( the carrier of (TOP-REAL 2)) Function-like V26( the carrier of (TOP-REAL 2)) quasi_total Element of K6(K7( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)))

s is non empty V16() V19( the carrier of (TOP-REAL 2)) V20( the carrier of (TOP-REAL 2)) Function-like V26( the carrier of (TOP-REAL 2)) quasi_total Element of K6(K7( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)))

s is V40(2) V98() V141() Element of the carrier of (TOP-REAL 2)

f . s is V40(2) V98() V141() Element of the carrier of (TOP-REAL 2)

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

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

(s `2) * <i> is complex set

(s `1) + ((s `2) * <i>) is complex set

Rotate (((s `1) + ((s `2) * <i>)),S) is complex Element of COMPLEX

|.((s `1) + ((s `2) * <i>)).| is complex real ext-real Element of REAL

Arg ((s `1) + ((s `2) * <i>)) is complex real ext-real Element of REAL

S + (Arg ((s `1) + ((s `2) * <i>))) is complex real ext-real Element of REAL

cos (S + (Arg ((s `1) + ((s `2) * <i>)))) is complex real ext-real Element of REAL

|.((s `1) + ((s `2) * <i>)).| * (cos (S + (Arg ((s `1) + ((s `2) * <i>))))) is complex real ext-real Element of REAL

sin (S + (Arg ((s `1) + ((s `2) * <i>)))) is complex real ext-real Element of REAL

|.((s `1) + ((s `2) * <i>)).| * (sin (S + (Arg ((s `1) + ((s `2) * <i>))))) is complex real ext-real Element of REAL

(|.((s `1) + ((s `2) * <i>)).| * (sin (S + (Arg ((s `1) + ((s `2) * <i>)))))) * <i> is complex set

(|.((s `1) + ((s `2) * <i>)).| * (cos (S + (Arg ((s `1) + ((s `2) * <i>)))))) + ((|.((s `1) + ((s `2) * <i>)).| * (sin (S + (Arg ((s `1) + ((s `2) * <i>)))))) * <i>) is complex set

Re (Rotate (((s `1) + ((s `2) * <i>)),S)) is complex real ext-real Element of REAL

Im (Rotate (((s `1) + ((s `2) * <i>)),S)) is complex real ext-real Element of REAL

|[(Re (Rotate (((s `1) + ((s `2) * <i>)),S))),(Im (Rotate (((s `1) + ((s `2) * <i>)),S)))]| is V40(2) V98() V141() Element of the carrier of (TOP-REAL 2)

s . s is V40(2) V98() V141() Element of the carrier of (TOP-REAL 2)

S is complex real ext-real Element of REAL

f is complex set

Arg f is complex real ext-real Element of REAL

S + (Arg f) is complex real ext-real Element of REAL

cos (S + (Arg f)) is complex real ext-real Element of REAL

s is complex real ext-real integer set

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

(S + (Arg f)) + ((2 * PI) * s) is complex real ext-real Element of REAL

cos ((S + (Arg f)) + ((2 * PI) * s)) is complex real ext-real Element of REAL

Rotate (f,S) is complex Element of COMPLEX

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

|.f.| * (cos (S + (Arg f))) is complex real ext-real Element of REAL

sin (S + (Arg f)) is complex real ext-real Element of REAL

|.f.| * (sin (S + (Arg f))) is complex real ext-real Element of REAL

(|.f.| * (sin (S + (Arg f)))) * <i> is complex set

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

S + ((2 * PI) * s) is complex real ext-real Element of REAL

Rotate (f,(S + ((2 * PI) * s))) is complex Element of COMPLEX

(S + ((2 * PI) * s)) + (Arg f) is complex real ext-real Element of REAL

cos ((S + ((2 * PI) * s)) + (Arg f)) is complex real ext-real Element of REAL

|.f.| * (cos ((S + ((2 * PI) * s)) + (Arg f))) is complex real ext-real Element of REAL

sin ((S + ((2 * PI) * s)) + (Arg f)) is complex real ext-real Element of REAL

|.f.| * (sin ((S + ((2 * PI) * s)) + (Arg f))) is complex real ext-real Element of REAL

(|.f.| * (sin ((S + ((2 * PI) * s)) + (Arg f)))) * <i> is complex set

(|.f.| * (cos ((S + ((2 * PI) * s)) + (Arg f)))) + ((|.f.| * (sin ((S + ((2 * PI) * s)) + (Arg f)))) * <i>) is complex set

S is complex real ext-real Element of REAL

(S) is non empty V16() V19( the carrier of (TOP-REAL 2)) V20( the carrier of (TOP-REAL 2)) Function-like V26( the carrier of (TOP-REAL 2)) quasi_total Element of K6(K7( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)))

f is complex real ext-real integer set

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

S + ((2 * PI) * f) is complex real ext-real Element of REAL

((S + ((2 * PI) * f))) is non empty V16() V19( the carrier of (TOP-REAL 2)) V20( the carrier of (TOP-REAL 2)) Function-like V26( the carrier of (TOP-REAL 2)) quasi_total Element of K6(K7( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)))

s is V40(2) V98() V141() Element of the carrier of (TOP-REAL 2)

(S) . s is set

((S + ((2 * PI) * f))) . s is set

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

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

(s `2) * <i> is complex set

(s `1) + ((s `2) * <i>) is complex set

Rotate (((s `1) + ((s `2) * <i>)),S) is complex Element of COMPLEX

|.((s `1) + ((s `2) * <i>)).| is complex real ext-real Element of REAL

Arg ((s `1) + ((s `2) * <i>)) is complex real ext-real Element of REAL

S + (Arg ((s `1) + ((s `2) * <i>))) is complex real ext-real Element of REAL

cos (S + (Arg ((s `1) + ((s `2) * <i>)))) is complex real ext-real Element of REAL

|.((s `1) + ((s `2) * <i>)).| * (cos (S + (Arg ((s `1) + ((s `2) * <i>))))) is complex real ext-real Element of REAL

sin (S + (Arg ((s `1) + ((s `2) * <i>)))) is complex real ext-real Element of REAL

|.((s `1) + ((s `2) * <i>)).| * (sin (S + (Arg ((s `1) + ((s `2) * <i>))))) is complex real ext-real Element of REAL

(|.((s `1) + ((s `2) * <i>)).| * (sin (S + (Arg ((s `1) + ((s `2) * <i>)))))) * <i> is complex set

(|.((s `1) + ((s `2) * <i>)).| * (cos (S + (Arg ((s `1) + ((s `2) * <i>)))))) + ((|.((s `1) + ((s `2) * <i>)).| * (sin (S + (Arg ((s `1) + ((s `2) * <i>)))))) * <i>) is complex set

Rotate (((s `1) + ((s `2) * <i>)),(S + ((2 * PI) * f))) is complex Element of COMPLEX

(S + ((2 * PI) * f)) + (Arg ((s `1) + ((s `2) * <i>))) is complex real ext-real Element of REAL

cos ((S + ((2 * PI) * f)) + (Arg ((s `1) + ((s `2) * <i>)))) is complex real ext-real Element of REAL

|.((s `1) + ((s `2) * <i>)).| * (cos ((S + ((2 * PI) * f)) + (Arg ((s `1) + ((s `2) * <i>))))) is complex real ext-real Element of REAL

sin ((S + ((2 * PI) * f)) + (Arg ((s `1) + ((s `2) * <i>)))) is complex real ext-real Element of REAL

|.((s `1) + ((s `2) * <i>)).| * (sin ((S + ((2 * PI) * f)) + (Arg ((s `1) + ((s `2) * <i>))))) is complex real ext-real Element of REAL

(|.((s `1) + ((s `2) * <i>)).| * (sin ((S + ((2 * PI) * f)) + (Arg ((s `1) + ((s `2) * <i>)))))) * <i> is complex set

(|.((s `1) + ((s `2) * <i>)).| * (cos ((S + ((2 * PI) * f)) + (Arg ((s `1) + ((s `2) * <i>)))))) + ((|.((s `1) + ((s `2) * <i>)).| * (sin ((S + ((2 * PI) * f)) + (Arg ((s `1) + ((s `2) * <i>)))))) * <i>) is complex set

(S) . s is V40(2) V98() V141() Element of the carrier of (TOP-REAL 2)

Re (Rotate (((s `1) + ((s `2) * <i>)),S)) is complex real ext-real Element of REAL

Im (Rotate (((s `1) + ((s `2) * <i>)),S)) is complex real ext-real Element of REAL

|[(Re (Rotate (((s `1) + ((s `2) * <i>)),S))),(Im (Rotate (((s `1) + ((s `2) * <i>)),S)))]| is V40(2) V98() V141() Element of the carrier of (TOP-REAL 2)

((S + ((2 * PI) * f))) . s is V40(2) V98() V141() Element of the carrier of (TOP-REAL 2)

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

K7( the carrier of (TopSpaceMetr (Euclid 2)), the carrier of (TopSpaceMetr (Euclid 2))) is V16() set

K6(K7( the carrier of (TopSpaceMetr (Euclid 2)), the carrier of (TopSpaceMetr (Euclid 2)))) is set

S is complex real ext-real Element of REAL

(S) is non empty V16() V19( the carrier of (TOP-REAL 2)) V20( the carrier of (TOP-REAL 2)) Function-like V26( the carrier of (TOP-REAL 2)) quasi_total Element of K6(K7( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)))

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

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

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

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

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

f is complex real ext-real set

s is non empty V16() V19( the carrier of (TopSpaceMetr (Euclid 2))) V20( the carrier of (TopSpaceMetr (Euclid 2))) Function-like V26( the carrier of (TopSpaceMetr (Euclid 2))) quasi_total Element of K6(K7( the carrier of (TopSpaceMetr (Euclid 2)), the carrier of (TopSpaceMetr (Euclid 2))))

K7( the carrier of (Euclid 2), the carrier of (Euclid 2)) is V16() set

K6(K7( the carrier of (Euclid 2), the carrier of (Euclid 2))) is set

s is complex real ext-real Element of REAL

(s) is non empty V16() V19( the carrier of (TOP-REAL 2)) V20( the carrier of (TOP-REAL 2)) Function-like V26( the carrier of (TOP-REAL 2)) quasi_total Element of K6(K7( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)))

A1 is non empty V16() V19( the carrier of (Euclid 2)) V20( the carrier of (Euclid 2)) Function-like V26( the carrier of (Euclid 2)) quasi_total Element of K6(K7( the carrier of (Euclid 2), the carrier of (Euclid 2)))

rng A1 is non empty Element of K6( the carrier of (Euclid 2))

A2 is set

B1 is V40(2) V98() V141() Element of the carrier of (TOP-REAL 2)

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

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

(B1 `2) * <i> is complex set

(B1 `1) + ((B1 `2) * <i>) is complex set

S2 is complex Element of COMPLEX

Arg S2 is complex real ext-real Element of REAL

(Arg S2) - s is complex real ext-real Element of REAL

- s is complex real ext-real Element of REAL

Rotate (S2,(- s)) is complex Element of COMPLEX

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

(- s) + (Arg S2) is complex real ext-real Element of REAL

cos ((- s) + (Arg S2)) is complex real ext-real Element of REAL

|.S2.| * (cos ((- s) + (Arg S2))) is complex real ext-real Element of REAL

sin ((- s) + (Arg S2)) is complex real ext-real Element of REAL

|.S2.| * (sin ((- s) + (Arg S2))) is complex real ext-real Element of REAL

(|.S2.| * (sin ((- s) + (Arg S2)))) * <i> is complex set

(|.S2.| * (cos ((- s) + (Arg S2)))) + ((|.S2.| * (sin ((- s) + (Arg S2)))) * <i>) is complex set

|.(Rotate (S2,(- s))).| is complex real ext-real Element of REAL

Arg (Rotate (S2,(- s))) is complex real ext-real Element of REAL

Rotate ((Rotate (S2,(- s))),s) is complex Element of COMPLEX

s + (Arg (Rotate (S2,(- s)))) is complex real ext-real Element of REAL

cos (s + (Arg (Rotate (S2,(- s))))) is complex real ext-real Element of REAL

|.(Rotate (S2,(- s))).| * (cos (s + (Arg (Rotate (S2,(- s)))))) is complex real ext-real Element of REAL

sin (s + (Arg (Rotate (S2,(- s))))) is complex real ext-real Element of REAL

|.(Rotate (S2,(- s))).| * (sin (s + (Arg (Rotate (S2,(- s)))))) is complex real ext-real Element of REAL

(|.(Rotate (S2,(- s))).| * (sin (s + (Arg (Rotate (S2,(- s))))))) * <i> is complex set

(|.(Rotate (S2,(- s))).| * (cos (s + (Arg (Rotate (S2,(- s))))))) + ((|.(Rotate (S2,(- s))).| * (sin (s + (Arg (Rotate (S2,(- s))))))) * <i>) is complex set

Re (Rotate (S2,(- s))) is complex real ext-real Element of REAL

Im (Rotate (S2,(- s))) is complex real ext-real Element of REAL

|[(Re (Rotate (S2,(- s)))),(Im (Rotate (S2,(- s))))]| is V40(2) V98() V141() Element of the carrier of (TOP-REAL 2)

dom A1 is non empty Element of K6( the carrier of (Euclid 2))

A1 . |[(Re (Rotate (S2,(- s)))),(Im (Rotate (S2,(- s))))]| is set

|[(Re (Rotate (S2,(- s)))),(Im (Rotate (S2,(- s))))]| `1 is complex real ext-real Element of REAL

|[(Re (Rotate (S2,(- s)))),(Im (Rotate (S2,(- s))))]| `2 is complex real ext-real Element of REAL

(|[(Re (Rotate (S2,(- s)))),(Im (Rotate (S2,(- s))))]| `2) * <i> is complex set

(|[(Re (Rotate (S2,(- s)))),(Im (Rotate (S2,(- s))))]| `1) + ((|[(Re (Rotate (S2,(- s)))),(Im (Rotate (S2,(- s))))]| `2) * <i>) is complex set

Rotate (((|[(Re (Rotate (S2,(- s)))),(Im (Rotate (S2,(- s))))]| `1) + ((|[(Re (Rotate (S2,(- s)))),(Im (Rotate (S2,(- s))))]| `2) * <i>)),s) is complex Element of COMPLEX

|.((|[(Re (Rotate (S2,(- s)))),(Im (Rotate (S2,(- s))))]| `1) + ((|[(Re (Rotate (S2,(- s)))),(Im (Rotate (S2,(- s))))]| `2) * <i>)).| is complex real ext-real Element of REAL

Arg ((|[(Re (Rotate (S2,(- s)))),(Im (Rotate (S2,(- s))))]| `1) + ((|[(Re (Rotate (S2,(- s)))),(Im (Rotate (S2,(- s))))]| `2) * <i>)) is complex real ext-real Element of REAL

s + (Arg ((|[(Re (Rotate (S2,(- s)))),(Im (Rotate (S2,(- s))))]| `1) + ((|[(Re (Rotate (S2,(- s)))),(Im (Rotate (S2,(- s))))]| `2) * <i>))) is complex real ext-real Element of REAL

cos (s + (Arg ((|[(Re (Rotate (S2,(- s)))),(Im (Rotate (S2,(- s))))]| `1) + ((|[(Re (Rotate (S2,(- s)))),(Im (Rotate (S2,(- s))))]| `2) * <i>)))) is complex real ext-real Element of REAL

|.((|[(Re (Rotate (S2,(- s)))),(Im (Rotate (S2,(- s))))]| `1) + ((|[(Re (Rotate (S2,(- s)))),(Im (Rotate (S2,(- s))))]| `2) * <i>)).| * (cos (s + (Arg ((|[(Re (Rotate (S2,(- s)))),(Im (Rotate (S2,(- s))))]| `1) + ((|[(Re (Rotate (S2,(- s)))),(Im (Rotate (S2,(- s))))]| `2) * <i>))))) is complex real ext-real Element of REAL

sin (s + (Arg ((|[(Re (Rotate (S2,(- s)))),(Im (Rotate (S2,(- s))))]| `1) + ((|[(Re (Rotate (S2,(- s)))),(Im (Rotate (S2,(- s))))]| `2) * <i>)))) is complex real ext-real Element of REAL

|.((|[(Re (Rotate (S2,(- s)))),(Im (Rotate (S2,(- s))))]| `1) + ((|[(Re (Rotate (S2,(- s)))),(Im (Rotate (S2,(- s))))]| `2) * <i>)).| * (sin (s + (Arg ((|[(Re (Rotate (S2,(- s)))),(Im (Rotate (S2,(- s))))]| `1) + ((|[(Re (Rotate (S2,(- s)))),(Im (Rotate (S2,(- s))))]| `2) * <i>))))) is complex real ext-real Element of REAL

(|.((|[(Re (Rotate (S2,(- s)))),(Im (Rotate (S2,(- s))))]| `1) + ((|[(Re (Rotate (S2,(- s)))),(Im (Rotate (S2,(- s))))]| `2) * <i>)).| * (sin (s + (Arg ((|[(Re (Rotate (S2,(- s)))),(Im (Rotate (S2,(- s))))]| `1) + ((|[(Re (Rotate (S2,(- s)))),(Im (Rotate (S2,(- s))))]| `2) * <i>)))))) * <i> is complex set

(|.((|[(Re (Rotate (S2,(- s)))),(Im (Rotate (S2,(- s))))]| `1) + ((|[(Re (Rotate (S2,(- s)))),(Im (Rotate (S2,(- s))))]| `2) * <i>)).| * (cos (s + (Arg ((|[(Re (Rotate (S2,(- s)))),(Im (Rotate (S2,(- s))))]| `1) + ((|[(Re (Rotate (S2,(- s)))),(Im (Rotate (S2,(- s))))]| `2) * <i>)))))) + ((|.((|[(Re (Rotate (S2,(- s)))),(Im (Rotate (S2,(- s))))]| `1) + ((|[(Re (Rotate (S2,(- s)))),(Im (Rotate (S2,(- s))))]| `2) * <i>)).| * (sin (s + (Arg ((|[(Re (Rotate (S2,(- s)))),(Im (Rotate (S2,(- s))))]| `1) + ((|[(Re (Rotate (S2,(- s)))),(Im (Rotate (S2,(- s))))]| `2) * <i>)))))) * <i>) is complex set

Re (Rotate (((|[(Re (Rotate (S2,(- s)))),(Im (Rotate (S2,(- s))))]| `1) + ((|[(Re (Rotate (S2,(- s)))),(Im (Rotate (S2,(- s))))]| `2) * <i>)),s)) is complex real ext-real Element of REAL

Im (Rotate (((|[(Re (Rotate (S2,(- s)))),(Im (Rotate (S2,(- s))))]| `1) + ((|[(Re (Rotate (S2,(- s)))),(Im (Rotate (S2,(- s))))]| `2) * <i>)),s)) is complex real ext-real Element of REAL

|[(Re (Rotate (((|[(Re (Rotate (S2,(- s)))),(Im (Rotate (S2,(- s))))]| `1) + ((|[(Re (Rotate (S2,(- s)))),(Im (Rotate (S2,(- s))))]| `2) * <i>)),s))),(Im (Rotate (((|[(Re (Rotate (S2,(- s)))),(Im (Rotate (S2,(- s))))]| `1) + ((|[(Re (Rotate (S2,(- s)))),(Im (Rotate (S2,(- s))))]| `2) * <i>)),s)))]| is V40(2) V98() V141() Element of the carrier of (TOP-REAL 2)

(Re (Rotate (S2,(- s)))) + ((|[(Re (Rotate (S2,(- s)))),(Im (Rotate (S2,(- s))))]| `2) * <i>) is complex set

Rotate (((Re (Rotate (S2,(- s)))) + ((|[(Re (Rotate (S2,(- s)))),(Im (Rotate (S2,(- s))))]| `2) * <i>)),s) is complex Element of COMPLEX

|.((Re (Rotate (S2,(- s)))) + ((|[(Re (Rotate (S2,(- s)))),(Im (Rotate (S2,(- s))))]| `2) * <i>)).| is complex real ext-real Element of REAL

Arg ((Re (Rotate (S2,(- s)))) + ((|[(Re (Rotate (S2,(- s)))),(Im (Rotate (S2,(- s))))]| `2) * <i>)) is complex real ext-real Element of REAL

s + (Arg ((Re (Rotate (S2,(- s)))) + ((|[(Re (Rotate (S2,(- s)))),(Im (Rotate (S2,(- s))))]| `2) * <i>))) is complex real ext-real Element of REAL

cos (s + (Arg ((Re (Rotate (S2,(- s)))) + ((|[(Re (Rotate (S2,(- s)))),(Im (Rotate (S2,(- s))))]| `2) * <i>)))) is complex real ext-real Element of REAL

|.((Re (Rotate (S2,(- s)))) + ((|[(Re (Rotate (S2,(- s)))),(Im (Rotate (S2,(- s))))]| `2) * <i>)).| * (cos (s + (Arg ((Re (Rotate (S2,(- s)))) + ((|[(Re (Rotate (S2,(- s)))),(Im (Rotate (S2,(- s))))]| `2) * <i>))))) is complex real ext-real Element of REAL

sin (s + (Arg ((Re (Rotate (S2,(- s)))) + ((|[(Re (Rotate (S2,(- s)))),(Im (Rotate (S2,(- s))))]| `2) * <i>)))) is complex real ext-real Element of REAL

|.((Re (Rotate (S2,(- s)))) + ((|[(Re (Rotate (S2,(- s)))),(Im (Rotate (S2,(- s))))]| `2) * <i>)).| * (sin (s + (Arg ((Re (Rotate (S2,(- s)))) + ((|[(Re (Rotate (S2,(- s)))),(Im (Rotate (S2,(- s))))]| `2) * <i>))))) is complex real ext-real Element of REAL

(|.((Re (Rotate (S2,(- s)))) + ((|[(Re (Rotate (S2,(- s)))),(Im (Rotate (S2,(- s))))]| `2) * <i>)).| * (sin (s + (Arg ((Re (Rotate (S2,(- s)))) + ((|[(Re (Rotate (S2,(- s)))),(Im (Rotate (S2,(- s))))]| `2) * <i>)))))) * <i> is complex set

(|.((Re (Rotate (S2,(- s)))) + ((|[(Re (Rotate (S2,(- s)))),(Im (Rotate (S2,(- s))))]| `2) * <i>)).| * (cos (s + (Arg ((Re (Rotate (S2,(- s)))) + ((|[(Re (Rotate (S2,(- s)))),(Im (Rotate (S2,(- s))))]| `2) * <i>)))))) + ((|.((Re (Rotate (S2,(- s)))) + ((|[(Re (Rotate (S2,(- s)))),(Im (Rotate (S2,(- s))))]| `2) * <i>)).| * (sin (s + (Arg ((Re (Rotate (S2,(- s)))) + ((|[(Re (Rotate (S2,(- s)))),(Im (Rotate (S2,(- s))))]| `2) * <i>)))))) * <i>) is complex set

Re (Rotate (((Re (Rotate (S2,(- s)))) + ((|[(Re (Rotate (S2,(- s)))),(Im (Rotate (S2,(- s))))]| `2) * <i>)),s)) is complex real ext-real Element of REAL

|[(Re (Rotate (((Re (Rotate (S2,(- s)))) + ((|[(Re (Rotate (S2,(- s)))),(Im (Rotate (S2,(- s))))]| `2) * <i>)),s))),(Im (Rotate (((|[(Re (Rotate (S2,(- s)))),(Im (Rotate (S2,(- s))))]| `1) + ((|[(Re (Rotate (S2,(- s)))),(Im (Rotate (S2,(- s))))]| `2) * <i>)),s)))]| is V40(2) V98() V141() Element of the carrier of (TOP-REAL 2)

(Im (Rotate (S2,(- s)))) * <i> is complex set

(Re (Rotate (S2,(- s)))) + ((Im (Rotate (S2,(- s)))) * <i>) is complex set

Rotate (((Re (Rotate (S2,(- s)))) + ((Im (Rotate (S2,(- s)))) * <i>)),s) is complex Element of COMPLEX

|.((Re (Rotate (S2,(- s)))) + ((Im (Rotate (S2,(- s)))) * <i>)).| is complex real ext-real Element of REAL

Arg ((Re (Rotate (S2,(- s)))) + ((Im (Rotate (S2,(- s)))) * <i>)) is complex real ext-real Element of REAL

s + (Arg ((Re (Rotate (S2,(- s)))) + ((Im (Rotate (S2,(- s)))) * <i>))) is complex real ext-real Element of REAL

cos (s + (Arg ((Re (Rotate (S2,(- s)))) + ((Im (Rotate (S2,(- s)))) * <i>)))) is complex real ext-real Element of REAL

|.((Re (Rotate (S2,(- s)))) + ((Im (Rotate (S2,(- s)))) * <i>)).| * (cos (s + (Arg ((Re (Rotate (S2,(- s)))) + ((Im (Rotate (S2,(- s)))) * <i>))))) is complex real ext-real Element of REAL

sin (s + (Arg ((Re (Rotate (S2,(- s)))) + ((Im (Rotate (S2,(- s)))) * <i>)))) is complex real ext-real Element of REAL

|.((Re (Rotate (S2,(- s)))) + ((Im (Rotate (S2,(- s)))) * <i>)).| * (sin (s + (Arg ((Re (Rotate (S2,(- s)))) + ((Im (Rotate (S2,(- s)))) * <i>))))) is complex real ext-real Element of REAL

(|.((Re (Rotate (S2,(- s)))) + ((Im (Rotate (S2,(- s)))) * <i>)).| * (sin (s + (Arg ((Re (Rotate (S2,(- s)))) + ((Im (Rotate (S2,(- s)))) * <i>)))))) * <i> is complex set

(|.((Re (Rotate (S2,(- s)))) + ((Im (Rotate (S2,(- s)))) * <i>)).| * (cos (s + (Arg ((Re (Rotate (S2,(- s)))) + ((Im (Rotate (S2,(- s)))) * <i>)))))) + ((|.((Re (Rotate (S2,(- s)))) + ((Im (Rotate (S2,(- s)))) * <i>)).| * (sin (s + (Arg ((Re (Rotate (S2,(- s)))) + ((Im (Rotate (S2,(- s)))) * <i>)))))) * <i>) is complex set

Re (Rotate (((Re (Rotate (S2,(- s)))) + ((Im (Rotate (S2,(- s)))) * <i>)),s)) is complex real ext-real Element of REAL

|[(Re (Rotate (((Re (Rotate (S2,(- s)))) + ((Im (Rotate (S2,(- s)))) * <i>)),s))),(Im (Rotate (((|[(Re (Rotate (S2,(- s)))),(Im (Rotate (S2,(- s))))]| `1) + ((|[(Re (Rotate (S2,(- s)))),(Im (Rotate (S2,(- s))))]| `2) * <i>)),s)))]| is V40(2) V98() V141() Element of the carrier of (TOP-REAL 2)

Im (Rotate (((Re (Rotate (S2,(- s)))) + ((|[(Re (Rotate (S2,(- s)))),(Im (Rotate (S2,(- s))))]| `2) * <i>)),s)) is complex real ext-real Element of REAL

|[(Re (Rotate (((Re (Rotate (S2,(- s)))) + ((Im (Rotate (S2,(- s)))) * <i>)),s))),(Im (Rotate (((Re (Rotate (S2,(- s)))) + ((|[(Re (Rotate (S2,(- s)))),(Im (Rotate (S2,(- s))))]| `2) * <i>)),s)))]| is V40(2) V98() V141() Element of the carrier of (TOP-REAL 2)

Im (Rotate (((Re (Rotate (S2,(- s)))) + ((Im (Rotate (S2,(- s)))) * <i>)),s)) is complex real ext-real Element of REAL

|[(Re (Rotate (((Re (Rotate (S2,(- s)))) + ((Im (Rotate (S2,(- s)))) * <i>)),s))),(Im (Rotate (((Re (Rotate (S2,(- s)))) + ((Im (Rotate (S2,(- s)))) * <i>)),s)))]| is V40(2) V98() V141() Element of the carrier of (TOP-REAL 2)

Re (Rotate ((Rotate (S2,(- s))),s)) is complex real ext-real Element of REAL

|[(Re (Rotate ((Rotate (S2,(- s))),s))),(Im (Rotate (((Re (Rotate (S2,(- s)))) + ((Im (Rotate (S2,(- s)))) * <i>)),s)))]| is V40(2) V98() V141() Element of the carrier of (TOP-REAL 2)

Re S2 is complex real ext-real Element of REAL

Im S2 is complex real ext-real Element of REAL

|[(Re S2),(Im S2)]| is V40(2) V98() V141() Element of the carrier of (TOP-REAL 2)

|[(B1 `1),(Im S2)]| is V40(2) V98() V141() Element of the carrier of (TOP-REAL 2)

|[(B1 `1),(B1 `2)]| is V40(2) V98() V141() Element of the carrier of (TOP-REAL 2)

(Arg S2) - s is complex real ext-real Element of REAL

(2 * PI) + ((Arg S2) - s) is complex real ext-real Element of REAL

- s is complex real ext-real Element of REAL

Rotate (S2,(- s)) is complex Element of COMPLEX

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

(- s) + (Arg S2) is complex real ext-real Element of REAL

cos ((- s) + (Arg S2)) is complex real ext-real Element of REAL

|.S2.| * (cos ((- s) + (Arg S2))) is complex real ext-real Element of REAL

sin ((- s) + (Arg S2)) is complex real ext-real Element of REAL

|.S2.| * (sin ((- s) + (Arg S2))) is complex real ext-real Element of REAL

(|.S2.| * (sin ((- s) + (Arg S2)))) * <i> is complex set

(|.S2.| * (cos ((- s) + (Arg S2)))) + ((|.S2.| * (sin ((- s) + (Arg S2)))) * <i>) is complex set

Re (Rotate (S2,(- s))) is complex real ext-real Element of REAL

Im (Rotate (S2,(- s))) is complex real ext-real Element of REAL

|[(Re (Rotate (S2,(- s)))),(Im (Rotate (S2,(- s))))]| is V40(2) V98() V141() Element of the carrier of (TOP-REAL 2)

dom A1 is non empty Element of K6( the carrier of (Euclid 2))

|.(Rotate (S2,(- s))).| is complex real ext-real Element of REAL

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

((2 * PI) * 1) + ((- s) + (Arg S2)) is complex real ext-real Element of REAL

cos (((2 * PI) * 1) + ((- s) + (Arg S2))) is complex real ext-real Element of REAL

|.(Rotate (S2,(- s))).| * (cos (((2 * PI) * 1) + ((- s) + (Arg S2)))) is complex real ext-real Element of REAL

|.(Rotate (S2,(- s))).| * (sin ((- s) + (Arg S2))) is complex real ext-real Element of REAL

(|.(Rotate (S2,(- s))).| * (sin ((- s) + (Arg S2)))) * <i> is complex set

(|.(Rotate (S2,(- s))).| * (cos (((2 * PI) * 1) + ((- s) + (Arg S2))))) + ((|.(Rotate (S2,(- s))).| * (sin ((- s) + (Arg S2)))) * <i>) is complex set

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

|.(Rotate (S2,(- s))).| * (cos ((2 * PI) + ((Arg S2) - s))) is complex real ext-real Element of REAL

sin (((2 * PI) * 1) + ((- s) + (Arg S2))) is complex real ext-real Element of REAL

|.(Rotate (S2,(- s))).| * (sin (((2 * PI) * 1) + ((- s) + (Arg S2)))) is complex real ext-real Element of REAL

(|.(Rotate (S2,(- s))).| * (sin (((2 * PI) * 1) + ((- s) + (Arg S2))))) * <i> is complex set

(|.(Rotate (S2,(- s))).| * (cos ((2 * PI) + ((Arg S2) - s)))) + ((|.(Rotate (S2,(- s))).| * (sin (((2 * PI) * 1) + ((- s) + (Arg S2))))) * <i>) is complex set

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

((2 * PI) - s) + (Arg S2) is complex real ext-real Element of REAL

Arg (Rotate (S2,(- s))) is complex real ext-real Element of REAL

Rotate ((Rotate (S2,(- s))),s) is complex Element of COMPLEX

s + (Arg (Rotate (S2,(- s)))) is complex real ext-real Element of REAL

cos (s + (Arg (Rotate (S2,(- s))))) is complex real ext-real Element of REAL

|.(Rotate (S2,(- s))).| * (cos (s + (Arg (Rotate (S2,(- s)))))) is complex real ext-real Element of REAL

sin (s + (Arg (Rotate (S2,(- s))))) is complex real ext-real Element of REAL

|.(Rotate (S2,(- s))).| * (sin (s + (Arg (Rotate (S2,(- s)))))) is complex real ext-real Element of REAL

(|.(Rotate (S2,(- s))).| * (sin (s + (Arg (Rotate (S2,(- s))))))) * <i> is complex set

(|.(Rotate (S2,(- s))).| * (cos (s + (Arg (Rotate (S2,(- s))))))) + ((|.(Rotate (S2,(- s))).| * (sin (s + (Arg (Rotate (S2,(- s))))))) * <i>) is complex set

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

|.(Rotate (S2,(- s))).| * (cos (Arg S2)) is complex real ext-real Element of REAL

((2 * PI) * 1) + (Arg S2) is complex real ext-real Element of REAL

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

|.(Rotate (S2,(- s))).| * (sin (((2 * PI) * 1) + (Arg S2))) is complex real ext-real Element of REAL

(|.(Rotate (S2,(- s))).| * (sin (((2 * PI) * 1) + (Arg S2)))) * <i> is complex set

(|.(Rotate (S2,(- s))).| * (cos (Arg S2))) + ((|.(Rotate (S2,(- s))).| * (sin (((2 * PI) * 1) + (Arg S2)))) * <i>) is complex set

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

|.(Rotate (S2,(- s))).| * (sin (Arg S2)) is complex real ext-real Element of REAL

(|.(Rotate (S2,(- s))).| * (sin (Arg S2))) * <i> is complex set

(|.(Rotate (S2,(- s))).| * (cos (Arg S2))) + ((|.(Rotate (S2,(- s))).| * (sin (Arg S2))) * <i>) is complex set

A1 . |[(Re (Rotate (S2,(- s)))),(Im (Rotate (S2,(- s))))]| is set

|[(Re (Rotate (S2,(- s)))),(Im (Rotate (S2,(- s))))]| `1 is complex real ext-real Element of REAL

|[(Re (Rotate (S2,(- s)))),(Im (Rotate (S2,(- s))))]| `2 is complex real ext-real Element of REAL

(|[(Re (Rotate (S2,(- s)))),(Im (Rotate (S2,(- s))))]| `2) * <i> is complex set

(|[(Re (Rotate (S2,(- s)))),(Im (Rotate (S2,(- s))))]| `1) + ((|[(Re (Rotate (S2,(- s)))),(Im (Rotate (S2,(- s))))]| `2) * <i>) is complex set

Rotate (((|[(Re (Rotate (S2,(- s)))),(Im (Rotate (S2,(- s))))]| `1) + ((|[(Re (Rotate (S2,(- s)))),(Im (Rotate (S2,(- s))))]| `2) * <i>)),s) is complex Element of COMPLEX

|.((|[(Re (Rotate (S2,(- s)))),(Im (Rotate (S2,(- s))))]| `1) + ((|[(Re (Rotate (S2,(- s)))),(Im (Rotate (S2,(- s))))]| `2) * <i>)).| is complex real ext-real Element of REAL

Arg ((|[(Re (Rotate (S2,(- s)))),(Im (Rotate (S2,(- s))))]| `1) + ((|[(Re (Rotate (S2,(- s)))),(Im (Rotate (S2,(- s))))]| `2) * <i>)) is complex real ext-real Element of REAL

s + (Arg ((|[(Re (Rotate (S2,(- s)))),(Im (Rotate (S2,(- s))))]| `1) + ((|[(Re (Rotate (S2,(- s)))),(Im (Rotate (S2,(- s))))]| `2) * <i>))) is complex real ext-real Element of REAL

cos (s + (Arg ((|[(Re (Rotate (S2,(- s)))),(Im (Rotate (S2,(- s))))]| `1) + ((|[(Re (Rotate (S2,(- s)))),(Im (Rotate (S2,(- s))))]| `2) * <i>)))) is complex real ext-real Element of REAL

|.((|[(Re (Rotate (S2,(- s)))),(Im (Rotate (S2,(- s))))]| `1) + ((|[(Re (Rotate (S2,(- s)))),(Im (Rotate (S2,(- s))))]| `2) * <i>)).| * (cos (s + (Arg ((|[(Re (Rotate (S2,(- s)))),(Im (Rotate (S2,(- s))))]| `1) + ((|[(Re (Rotate (S2,(- s)))),(Im (Rotate (S2,(- s))))]| `2) * <i>))))) is complex real ext-real Element of REAL

sin (s + (Arg ((|[(Re (Rotate (S2,(- s)))),(Im (Rotate (S2,(- s))))]| `1) + ((|[(Re (Rotate (S2,(- s)))),(Im (Rotate (S2,(- s))))]| `2) * <i>)))) is complex real ext-real Element of REAL

|.((|[(Re (Rotate (S2,(- s)))),(Im (Rotate (S2,(- s))))]| `1) + ((|[(Re (Rotate (S2,(- s)))),(Im (Rotate (S2,(- s))))]| `2) * <i>)).| * (sin (s + (Arg ((|[(Re (Rotate (S2,(- s)))),(Im (Rotate (S2,(- s))))]| `1) + ((|[(Re (Rotate (S2,(- s)))),(Im (Rotate (S2,(- s))))]| `2) * <i>))))) is complex real ext-real Element of REAL

(|.((|[(Re (Rotate (S2,(- s)))),(Im (Rotate (S2,(- s))))]| `1) + ((|[(Re (Rotate (S2,(- s)))),(Im (Rotate (S2,(- s))))]| `2) * <i>)).| * (sin (s + (Arg ((|[(Re (Rotate (S2,(- s)))),(Im (Rotate (S2,(- s))))]| `1) + ((|[(Re (Rotate (S2,(- s)))),(Im (Rotate (S2,(- s))))]| `2) * <i>)))))) * <i> is complex set

(|.((|[(Re (Rotate (S2,(- s)))),(Im (Rotate (S2,(- s))))]| `1) + ((|[(Re (Rotate (S2,(- s)))),(Im (Rotate (S2,(- s))))]| `2) * <i>)).| * (cos (s + (Arg ((|[(Re (Rotate (S2,(- s)))),(Im (Rotate (S2,(- s))))]| `1) + ((|[(Re (Rotate (S2,(- s)))),(Im (Rotate (S2,(- s))))]| `2) * <i>)))))) + ((|.((|[(Re (Rotate (S2,(- s)))),(Im (Rotate (S2,(- s))))]| `1) + ((|[(Re (Rotate (S2,(- s)))),(Im (Rotate (S2,(- s))))]| `2) * <i>)).| * (sin (s + (Arg ((|[(Re (Rotate (S2,(- s)))),(Im (Rotate (S2,(- s))))]| `1) + ((|[(Re (Rotate (S2,(- s)))),(Im (Rotate (S2,(- s))))]| `2) * <i>)))))) * <i>) is complex set

Re (Rotate (((|[(Re (Rotate (S2,(- s)))),(Im (Rotate (S2,(- s))))]| `1) + ((|[(Re (Rotate (S2,(- s)))),(Im (Rotate (S2,(- s))))]| `2) * <i>)),s)) is complex real ext-real Element of REAL

Im (Rotate (((|[(Re (Rotate (S2,(- s)))),(Im (Rotate (S2,(- s))))]| `1) + ((|[(Re (Rotate (S2,(- s)))),(Im (Rotate (S2,(- s))))]| `2) * <i>)),s)) is complex real ext-real Element of REAL

|[(Re (Rotate (((|[(Re (Rotate (S2,(- s)))),(Im (Rotate (S2,(- s))))]| `1) + ((|[(Re (Rotate (S2,(- s)))),(Im (Rotate (S2,(- s))))]| `2) * <i>)),s))),(Im (Rotate (((|[(Re (Rotate (S2,(- s)))),(Im (Rotate (S2,(- s))))]| `1) + ((|[(Re (Rotate (S2,(- s)))),(Im (Rotate (S2,(- s))))]| `2) * <i>)),s)))]| is V40(2) V98() V141() Element of the carrier of (TOP-REAL 2)

(Re (Rotate (S2,(- s)))) + ((|[(Re (Rotate (S2,(- s)))),(Im (Rotate (S2,(- s))))]| `2) * <i>) is complex set

Rotate (((Re (Rotate (S2,(- s)))) + ((|[(Re (Rotate (S2,(- s)))),(Im (Rotate (S2,(- s))))]| `2) * <i>)),s) is complex Element of COMPLEX

|.((Re (Rotate (S2,(- s)))) + ((|[(Re (Rotate (S2,(- s)))),(Im (Rotate (S2,(- s))))]| `2) * <i>)).| is complex real ext-real Element of REAL

Arg ((Re (Rotate (S2,(- s)))) + ((|[(Re (Rotate (S2,(- s)))),(Im (Rotate (S2,(- s))))]| `2) * <i>)) is complex real ext-real Element of REAL

s + (Arg ((Re (Rotate (S2,(- s)))) + ((|[(Re (Rotate (S2,(- s)))),(Im (Rotate (S2,(- s))))]| `2) * <i>))) is complex real ext-real Element of REAL

cos (s + (Arg ((Re (Rotate (S2,(- s)))) + ((|[(Re (Rotate (S2,(- s)))),(Im (Rotate (S2,(- s))))]| `2) * <i>)))) is complex real ext-real Element of REAL

|.((Re (Rotate (S2,(- s)))) + ((|[(Re (Rotate (S2,(- s)))),(Im (Rotate (S2,(- s))))]| `2) * <i>)).| * (cos (s + (Arg ((Re (Rotate (S2,(- s)))) + ((|[(Re (Rotate (S2,(- s)))),(Im (Rotate (S2,(- s))))]| `2) * <i>))))) is complex real ext-real Element of REAL

sin (s + (Arg ((Re (Rotate (S2,(- s)))) + ((|[(Re (Rotate (S2,(- s)))),(Im (Rotate (S2,(- s))))]| `2) * <i>)))) is complex real ext-real Element of REAL

|.((Re (Rotate (S2,(- s)))) + ((|[(Re (Rotate (S2,(- s)))),(Im (Rotate (S2,(- s))))]| `2) * <i>)).| * (sin (s + (Arg ((Re (Rotate (S2,(- s)))) + ((|[(Re (Rotate (S2,(- s)))),(Im (Rotate (S2,(- s))))]| `2) * <i>))))) is complex real ext-real Element of REAL

(|.((Re (Rotate (S2,(- s)))) + ((|[(Re (Rotate (S2,(- s)))),(Im (Rotate (S2,(- s))))]| `2) * <i>)).| * (sin (s + (Arg ((Re (Rotate (S2,(- s)))) + ((|[(Re (Rotate (S2,(- s)))),(Im (Rotate (S2,(- s))))]| `2) * <i>)))))) * <i> is complex set

(|.((Re (Rotate (S2,(- s)))) + ((|[(Re (Rotate (S2,(- s)))),(Im (Rotate (S2,(- s))))]| `2) * <i>)).| * (cos (s + (Arg ((Re (Rotate (S2,(- s)))) + ((|[(Re (Rotate (S2,(- s)))),(Im (Rotate (S2,(- s))))]| `2) * <i>)))))) + ((|.((Re (Rotate (S2,(- s)))) + ((|[(Re (Rotate (S2,(- s)))),(Im (Rotate (S2,(- s))))]| `2) * <i>)).| * (sin (s + (Arg ((Re (Rotate (S2,(- s)))) + ((|[(Re (Rotate (S2,(- s)))),(Im (Rotate (S2,(- s))))]| `2) * <i>)))))) * <i>) is complex set

Re (Rotate (((Re (Rotate (S2,(- s)))) + ((|[(Re (Rotate (S2,(- s)))),(Im (Rotate (S2,(- s))))]| `2) * <i>)),s)) is complex real ext-real Element of REAL

|[(Re (Rotate (((Re (Rotate (S2,(- s)))) + ((|[(Re (Rotate (S2,(- s)))),(Im (Rotate (S2,(- s))))]| `2) * <i>)),s))),(Im (Rotate (((|[(Re (Rotate (S2,(- s)))),(Im (Rotate (S2,(- s))))]| `1) + ((|[(Re (Rotate (S2,(- s)))),(Im (Rotate (S2,(- s))))]| `2) * <i>)),s)))]| is V40(2) V98() V141() Element of the carrier of (TOP-REAL 2)

(Im (Rotate (S2,(- s)))) * <i> is complex set

(Re (Rotate (S2,(- s)))) + ((Im (Rotate (S2,(- s)))) * <i>) is complex set

Rotate (((Re (Rotate (S2,(- s)))) + ((Im (Rotate (S2,(- s)))) * <i>)),s) is complex Element of COMPLEX

|.((Re (Rotate (S2,(- s)))) + ((Im (Rotate (S2,(- s)))) * <i>)).| is complex real ext-real Element of REAL

Arg ((Re (Rotate (S2,(- s)))) + ((Im (Rotate (S2,(- s)))) * <i>)) is complex real ext-real Element of REAL

s + (Arg ((Re (Rotate (S2,(- s)))) + ((Im (Rotate (S2,(- s)))) * <i>))) is complex real ext-real Element of REAL

cos (s + (Arg ((Re (Rotate (S2,(- s)))) + ((Im (Rotate (S2,(- s)))) * <i>)))) is complex real ext-real Element of REAL

|.((Re (Rotate (S2,(- s)))) + ((Im (Rotate (S2,(- s)))) * <i>)).| * (cos (s + (Arg ((Re (Rotate (S2,(- s)))) + ((Im (Rotate (S2,(- s)))) * <i>))))) is complex real ext-real Element of REAL

sin (s + (Arg ((Re (Rotate (S2,(- s)))) + ((Im (Rotate (S2,(- s)))) * <i>)))) is complex real ext-real Element of REAL

|.((Re (Rotate (S2,(- s)))) + ((Im (Rotate (S2,(- s)))) * <i>)).| * (sin (s + (Arg ((Re (Rotate (S2,(- s)))) + ((Im (Rotate (S2,(- s)))) * <i>))))) is complex real ext-real Element of REAL

(|.((Re (Rotate (S2,(- s)))) + ((Im (Rotate (S2,(- s)))) * <i>)).| * (sin (s + (Arg ((Re (Rotate (S2,(- s)))) + ((Im (Rotate (S2,(- s)))) * <i>)))))) * <i> is complex set

(|.((Re (Rotate (S2,(- s)))) + ((Im (Rotate (S2,(- s)))) * <i>)).| * (cos (s + (Arg ((Re (Rotate (S2,(- s)))) + ((Im (Rotate (S2,(- s)))) * <i>)))))) + ((|.((Re (Rotate (S2,(- s)))) + ((Im (Rotate (S2,(- s)))) * <i>)).| * (sin (s + (Arg ((Re (Rotate (S2,(- s)))) + ((Im (Rotate (S2,(- s)))) * <i>)))))) * <i>) is complex set

Re (Rotate (((Re (Rotate (S2,(- s)))) + ((Im (Rotate (S2,(- s)))) * <i>)),s)) is complex real ext-real Element of REAL

|[(Re (Rotate (((Re (Rotate (S2,(- s)))) + ((Im (Rotate (S2,(- s)))) * <i>)),s))),(Im (Rotate (((|[(Re (Rotate (S2,(- s)))),(Im (Rotate (S2,(- s))))]| `1) + ((|[(Re (Rotate (S2,(- s)))),(Im (Rotate (S2,(- s))))]| `2) * <i>)),s)))]| is V40(2) V98() V141() Element of the carrier of (TOP-REAL 2)

Im (Rotate (((Re (Rotate (S2,(- s)))) + ((|[(Re (Rotate (S2,(- s)))),(Im (Rotate (S2,(- s))))]| `2) * <i>)),s)) is complex real ext-real Element of REAL

|[(Re (Rotate (((Re (Rotate (S2,(- s)))) + ((Im (Rotate (S2,(- s)))) *