:: 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)))) *