:: 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)))) * <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)
|[0,0]| 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 . |[0,0]| is set
|[0,0]| `1 is complex real ext-real Element of REAL
|[0,0]| `2 is complex real ext-real Element of REAL
(|[0,0]| `2) * <i> is complex set
(|[0,0]| `1) + ((|[0,0]| `2) * <i>) is complex set
Rotate (((|[0,0]| `1) + ((|[0,0]| `2) * <i>)),S) is complex Element of COMPLEX
|.((|[0,0]| `1) + ((|[0,0]| `2) * <i>)).| is complex real ext-real Element of REAL
Arg ((|[0,0]| `1) + ((|[0,0]| `2) * <i>)) is complex real ext-real Element of REAL
S + (Arg ((|[0,0]| `1) + ((|[0,0]| `2) * <i>))) is complex real ext-real Element of REAL
cos (S + (Arg ((|[0,0]| `1) + ((|[0,0]| `2) * <i>)))) is complex real ext-real Element of REAL
|.((|[0,0]| `1) + ((|[0,0]| `2) * <i>)).| * (cos (S + (Arg ((|[0,0]| `1) + ((|[0,0]| `2) * <i>))))) is complex real ext-real Element of REAL
sin (S + (Arg ((|[0,0]| `1) + ((|[0,0]| `2) * <i>)))) is complex real ext-real Element of REAL
|.((|[0,0]| `1) + ((|[0,0]| `2) * <i>)).| * (sin (S + (Arg ((|[0,0]| `1) + ((|[0,0]| `2) * <i>))))) is complex real ext-real Element of REAL
(|.((|[0,0]| `1) + ((|[0,0]| `2) * <i>)).| * (sin (S + (Arg ((|[0,0]| `1) + ((|[0,0]| `2) * <i>)))))) * <i> is complex set
(|.((|[0,0]| `1) + ((|[0,0]| `2) * <i>)).| * (cos (S + (Arg ((|[0,0]| `1) + ((|[0,0]| `2) * <i>)))))) + ((|.((|[0,0]| `1) + ((|[0,0]| `2) * <i>)).| * (sin (S + (Arg ((|[0,0]| `1) + ((|[0,0]| `2) * <i>)))))) * <i>) is complex set
Re (Rotate (((|[0,0]| `1) + ((|[0,0]| `2) * <i>)),S)) is complex real ext-real Element of REAL
Im (Rotate (((|[0,0]| `1) + ((|[0,0]| `2) * <i>)),S)) is complex real ext-real Element of REAL
|[(Re (Rotate (((|[0,0]| `1) + ((|[0,0]| `2) * <i>)),S))),(Im (Rotate (((|[0,0]| `1) + ((|[0,0]| `2) * <i>)),S)))]| is V40(2) V98() V141() Element of the carrier of (TOP-REAL 2)
arg is complex Element of COMPLEX
arg + ((|[0,0]| `2) * <i>) is complex set
Rotate ((arg + ((|[0,0]| `2) * <i>)),S) is complex Element of COMPLEX
|.(arg + ((|[0,0]| `2) * <i>)).| is complex real ext-real Element of REAL
Arg (arg + ((|[0,0]| `2) * <i>)) is complex real ext-real Element of REAL
S + (Arg (arg + ((|[0,0]| `2) * <i>))) is complex real ext-real Element of REAL
cos (S + (Arg (arg + ((|[0,0]| `2) * <i>)))) is complex real ext-real Element of REAL
|.(arg + ((|[0,0]| `2) * <i>)).| * (cos (S + (Arg (arg + ((|[0,0]| `2) * <i>))))) is complex real ext-real Element of REAL
sin (S + (Arg (arg + ((|[0,0]| `2) * <i>)))) is complex real ext-real Element of REAL
|.(arg + ((|[0,0]| `2) * <i>)).| * (sin (S + (Arg (arg + ((|[0,0]| `2) * <i>))))) is complex real ext-real Element of REAL
(|.(arg + ((|[0,0]| `2) * <i>)).| * (sin (S + (Arg (arg + ((|[0,0]| `2) * <i>)))))) * <i> is complex set
(|.(arg + ((|[0,0]| `2) * <i>)).| * (cos (S + (Arg (arg + ((|[0,0]| `2) * <i>)))))) + ((|.(arg + ((|[0,0]| `2) * <i>)).| * (sin (S + (Arg (arg + ((|[0,0]| `2) * <i>)))))) * <i>) is complex set
Re (Rotate ((arg + ((|[0,0]| `2) * <i>)),S)) is complex real ext-real Element of REAL
|[(Re (Rotate ((arg + ((|[0,0]| `2) * <i>)),S))),(Im (Rotate (((|[0,0]| `1) + ((|[0,0]| `2) * <i>)),S)))]| is V40(2) V98() V141() Element of the carrier of (TOP-REAL 2)
arg * <i> is complex set
arg + (arg * <i>) is complex set
Rotate ((arg + (arg * <i>)),S) is complex Element of COMPLEX
|.(arg + (arg * <i>)).| is complex real ext-real Element of REAL
Arg (arg + (arg * <i>)) is complex real ext-real Element of REAL
S + (Arg (arg + (arg * <i>))) is complex real ext-real Element of REAL
cos (S + (Arg (arg + (arg * <i>)))) is complex real ext-real Element of REAL
|.(arg + (arg * <i>)).| * (cos (S + (Arg (arg + (arg * <i>))))) is complex real ext-real Element of REAL
sin (S + (Arg (arg + (arg * <i>)))) is complex real ext-real Element of REAL
|.(arg + (arg * <i>)).| * (sin (S + (Arg (arg + (arg * <i>))))) is complex real ext-real Element of REAL
(|.(arg + (arg * <i>)).| * (sin (S + (Arg (arg + (arg * <i>)))))) * <i> is complex set
(|.(arg + (arg * <i>)).| * (cos (S + (Arg (arg + (arg * <i>)))))) + ((|.(arg + (arg * <i>)).| * (sin (S + (Arg (arg + (arg * <i>)))))) * <i>) is complex set
Re (Rotate ((arg + (arg * <i>)),S)) is complex real ext-real Element of REAL
|[(Re (Rotate ((arg + (arg * <i>)),S))),(Im (Rotate (((|[0,0]| `1) + ((|[0,0]| `2) * <i>)),S)))]| is V40(2) V98() V141() Element of the carrier of (TOP-REAL 2)
Im (Rotate ((arg + ((|[0,0]| `2) * <i>)),S)) is complex real ext-real Element of REAL
|[(Re (Rotate ((arg + (arg * <i>)),S))),(Im (Rotate ((arg + ((|[0,0]| `2) * <i>)),S)))]| is V40(2) V98() V141() Element of the carrier of (TOP-REAL 2)
Rotate (arg,S) is complex Element of COMPLEX
|.arg.| is complex real ext-real Element of REAL
Arg arg is complex real ext-real Element of REAL
S + (Arg arg) is complex real ext-real Element of REAL
cos (S + (Arg arg)) is complex real ext-real Element of REAL
|.arg.| * (cos (S + (Arg arg))) is complex real ext-real Element of REAL
sin (S + (Arg arg)) is complex real ext-real Element of REAL
|.arg.| * (sin (S + (Arg arg))) is complex real ext-real Element of REAL
(|.arg.| * (sin (S + (Arg arg)))) * <i> is complex set
(|.arg.| * (cos (S + (Arg arg)))) + ((|.arg.| * (sin (S + (Arg arg)))) * <i>) is complex set
Re (Rotate (arg,S)) is complex real ext-real Element of REAL
Im (Rotate (arg,S)) is complex real ext-real Element of REAL
|[(Re (Rotate (arg,S))),(Im (Rotate (arg,S)))]| is V40(2) V98() V141() Element of the carrier of (TOP-REAL 2)
Re arg is complex real ext-real Element of REAL
|[(Re arg),(Im (Rotate (arg,S)))]| is V40(2) V98() V141() Element of the carrier of (TOP-REAL 2)
Im arg is complex real ext-real Element of REAL
|[(Re arg),(Im arg)]| is V40(2) V98() V141() Element of the carrier of (TOP-REAL 2)
A2 is Element of the carrier of (Euclid 2)
B1 is Element of the carrier of (Euclid 2)
dist (A2,B1) is complex real ext-real Element of REAL
A1 . A2 is Element of the carrier of (Euclid 2)
A1 . B1 is Element of the carrier of (Euclid 2)
dist ((A1 . A2),(A1 . B1)) is complex real ext-real Element of REAL
B2 is V40(2) V98() V141() Element of the carrier of (TOP-REAL 2)
B2 `1 is complex real ext-real Element of REAL
B2 `2 is complex real ext-real Element of REAL
(B2 `2) * <i> is complex set
(B2 `1) + ((B2 `2) * <i>) is complex set
Rotate (((B2 `1) + ((B2 `2) * <i>)),S) is complex Element of COMPLEX
|.((B2 `1) + ((B2 `2) * <i>)).| is complex real ext-real Element of REAL
Arg ((B2 `1) + ((B2 `2) * <i>)) is complex real ext-real Element of REAL
S + (Arg ((B2 `1) + ((B2 `2) * <i>))) is complex real ext-real Element of REAL
cos (S + (Arg ((B2 `1) + ((B2 `2) * <i>)))) is complex real ext-real Element of REAL
|.((B2 `1) + ((B2 `2) * <i>)).| * (cos (S + (Arg ((B2 `1) + ((B2 `2) * <i>))))) is complex real ext-real Element of REAL
sin (S + (Arg ((B2 `1) + ((B2 `2) * <i>)))) is complex real ext-real Element of REAL
|.((B2 `1) + ((B2 `2) * <i>)).| * (sin (S + (Arg ((B2 `1) + ((B2 `2) * <i>))))) is complex real ext-real Element of REAL
(|.((B2 `1) + ((B2 `2) * <i>)).| * (sin (S + (Arg ((B2 `1) + ((B2 `2) * <i>)))))) * <i> is complex set
(|.((B2 `1) + ((B2 `2) * <i>)).| * (cos (S + (Arg ((B2 `1) + ((B2 `2) * <i>)))))) + ((|.((B2 `1) + ((B2 `2) * <i>)).| * (sin (S + (Arg ((B2 `1) + ((B2 `2) * <i>)))))) * <i>) is complex set
Re (Rotate (((B2 `1) + ((B2 `2) * <i>)),S)) is complex real ext-real Element of REAL
Im (Rotate (((B2 `1) + ((B2 `2) * <i>)),S)) is complex real ext-real Element of REAL
|[(Re (Rotate (((B2 `1) + ((B2 `2) * <i>)),S))),(Im (Rotate (((B2 `1) + ((B2 `2) * <i>)),S)))]| is V40(2) V98() V141() Element of the carrier of (TOP-REAL 2)
|[(Re (Rotate (((B2 `1) + ((B2 `2) * <i>)),S))),(Im (Rotate (((B2 `1) + ((B2 `2) * <i>)),S)))]| `1 is complex real ext-real Element of REAL
|[(Re (Rotate (((B2 `1) + ((B2 `2) * <i>)),S))),(Im (Rotate (((B2 `1) + ((B2 `2) * <i>)),S)))]| `2 is complex real ext-real Element of REAL
S2 is V40(2) V98() V141() Element of the carrier of (TOP-REAL 2)
S2 `1 is complex real ext-real Element of REAL
S2 `2 is complex real ext-real Element of REAL
(S2 `2) * <i> is complex set
(S2 `1) + ((S2 `2) * <i>) is complex set
Rotate (((S2 `1) + ((S2 `2) * <i>)),S) is complex Element of COMPLEX
|.((S2 `1) + ((S2 `2) * <i>)).| is complex real ext-real Element of REAL
Arg ((S2 `1) + ((S2 `2) * <i>)) is complex real ext-real Element of REAL
S + (Arg ((S2 `1) + ((S2 `2) * <i>))) is complex real ext-real Element of REAL
cos (S + (Arg ((S2 `1) + ((S2 `2) * <i>)))) is complex real ext-real Element of REAL
|.((S2 `1) + ((S2 `2) * <i>)).| * (cos (S + (Arg ((S2 `1) + ((S2 `2) * <i>))))) is complex real ext-real Element of REAL
sin (S + (Arg ((S2 `1) + ((S2 `2) * <i>)))) is complex real ext-real Element of REAL
|.((S2 `1) + ((S2 `2) * <i>)).| * (sin (S + (Arg ((S2 `1) + ((S2 `2) * <i>))))) is complex real ext-real Element of REAL
(|.((S2 `1) + ((S2 `2) * <i>)).| * (sin (S + (Arg ((S2 `1) + ((S2 `2) * <i>)))))) * <i> is complex set
(|.((S2 `1) + ((S2 `2) * <i>)).| * (cos (S + (Arg ((S2 `1) + ((S2 `2) * <i>)))))) + ((|.((S2 `1) + ((S2 `2) * <i>)).| * (sin (S + (Arg ((S2 `1) + ((S2 `2) * <i>)))))) * <i>) is complex set
Re (Rotate (((S2 `1) + ((S2 `2) * <i>)),S)) is complex real ext-real Element of REAL
Im (Rotate (((S2 `1) + ((S2 `2) * <i>)),S)) is complex real ext-real Element of REAL
|[(Re (Rotate (((S2 `1) + ((S2 `2) * <i>)),S))),(Im (Rotate (((S2 `1) + ((S2 `2) * <i>)),S)))]| is V40(2) V98() V141() Element of the carrier of (TOP-REAL 2)
|[(Re (Rotate (((S2 `1) + ((S2 `2) * <i>)),S))),(Im (Rotate (((S2 `1) + ((S2 `2) * <i>)),S)))]| `1 is complex real ext-real Element of REAL
|[(Re (Rotate (((S2 `1) + ((S2 `2) * <i>)),S))),(Im (Rotate (((S2 `1) + ((S2 `2) * <i>)),S)))]| `2 is complex real ext-real Element of REAL
Re ((S2 `1) + ((S2 `2) * <i>)) is complex real ext-real Element of REAL
Im ((S2 `1) + ((S2 `2) * <i>)) is complex real ext-real Element of REAL
sin S is complex real ext-real Element of REAL
(sin S) ^2 is complex real ext-real Element of REAL
(sin S) * (sin S) is complex real ext-real set
cos S is complex real ext-real Element of REAL
(cos S) ^2 is complex real ext-real Element of REAL
(cos S) * (cos S) is complex real ext-real set
((sin S) ^2) + ((cos S) ^2) is complex real ext-real Element of REAL
Re ((B2 `1) + ((B2 `2) * <i>)) is complex real ext-real Element of REAL
Im ((B2 `1) + ((B2 `2) * <i>)) is complex real ext-real Element of REAL
|[(B2 `1),(B2 `2)]| is V40(2) V98() V141() Element of the carrier of (TOP-REAL 2)
|[(S2 `1),(S2 `2)]| is V40(2) V98() V141() Element of the carrier of (TOP-REAL 2)
dist (A2,B1) is complex real ext-real Element of REAL
(B2 `1) - (S2 `1) is complex real ext-real Element of REAL
((B2 `1) - (S2 `1)) ^2 is complex real ext-real Element of REAL
((B2 `1) - (S2 `1)) * ((B2 `1) - (S2 `1)) is complex real ext-real set
(B2 `2) - (S2 `2) is complex real ext-real Element of REAL
((B2 `2) - (S2 `2)) ^2 is complex real ext-real Element of REAL
((B2 `2) - (S2 `2)) * ((B2 `2) - (S2 `2)) is complex real ext-real set
(((B2 `1) - (S2 `1)) ^2) + (((B2 `2) - (S2 `2)) ^2) is complex real ext-real Element of REAL
sqrt ((((B2 `1) - (S2 `1)) ^2) + (((B2 `2) - (S2 `2)) ^2)) is complex real ext-real Element of REAL
(B2 `1) * (B2 `1) is complex real ext-real Element of REAL
2 * (B2 `1) is complex real ext-real Element of REAL
(2 * (B2 `1)) * (S2 `1) is complex real ext-real Element of REAL
((B2 `1) * (B2 `1)) - ((2 * (B2 `1)) * (S2 `1)) is complex real ext-real Element of REAL
(S2 `1) * (S2 `1) is complex real ext-real Element of REAL
(((B2 `1) * (B2 `1)) - ((2 * (B2 `1)) * (S2 `1))) + ((S2 `1) * (S2 `1)) is complex real ext-real Element of REAL
(sin S) * (sin S) is complex real ext-real Element of REAL
(cos S) * (cos S) is complex real ext-real Element of REAL
((sin S) * (sin S)) + ((cos S) * (cos S)) is complex real ext-real Element of REAL
((((B2 `1) * (B2 `1)) - ((2 * (B2 `1)) * (S2 `1))) + ((S2 `1) * (S2 `1))) * (((sin S) * (sin S)) + ((cos S) * (cos S))) is complex real ext-real Element of REAL
(B2 `2) * (B2 `2) is complex real ext-real Element of REAL
2 * (B2 `2) is complex real ext-real Element of REAL
(2 * (B2 `2)) * (S2 `2) is complex real ext-real Element of REAL
((B2 `2) * (B2 `2)) - ((2 * (B2 `2)) * (S2 `2)) is complex real ext-real Element of REAL
(S2 `2) * (S2 `2) is complex real ext-real Element of REAL
(((B2 `2) * (B2 `2)) - ((2 * (B2 `2)) * (S2 `2))) + ((S2 `2) * (S2 `2)) is complex real ext-real Element of REAL
((((B2 `2) * (B2 `2)) - ((2 * (B2 `2)) * (S2 `2))) + ((S2 `2) * (S2 `2))) * (((sin S) ^2) + ((cos S) ^2)) is complex real ext-real Element of REAL
(((((B2 `1) * (B2 `1)) - ((2 * (B2 `1)) * (S2 `1))) + ((S2 `1) * (S2 `1))) * (((sin S) * (sin S)) + ((cos S) * (cos S)))) + (((((B2 `2) * (B2 `2)) - ((2 * (B2 `2)) * (S2 `2))) + ((S2 `2) * (S2 `2))) * (((sin S) ^2) + ((cos S) ^2))) is complex real ext-real Element of REAL
sqrt ((((((B2 `1) * (B2 `1)) - ((2 * (B2 `1)) * (S2 `1))) + ((S2 `1) * (S2 `1))) * (((sin S) * (sin S)) + ((cos S) * (cos S)))) + (((((B2 `2) * (B2 `2)) - ((2 * (B2 `2)) * (S2 `2))) + ((S2 `2) * (S2 `2))) * (((sin S) ^2) + ((cos S) ^2)))) is complex real ext-real Element of REAL
(B2 `1) * (cos S) is complex real ext-real Element of REAL
(B2 `2) * (sin S) is complex real ext-real Element of REAL
((B2 `1) * (cos S)) - ((B2 `2) * (sin S)) is complex real ext-real Element of REAL
(S2 `1) * (cos S) is complex real ext-real Element of REAL
(S2 `2) * (sin S) is complex real ext-real Element of REAL
((S2 `1) * (cos S)) - ((S2 `2) * (sin S)) is complex real ext-real Element of REAL
(((B2 `1) * (cos S)) - ((B2 `2) * (sin S))) - (((S2 `1) * (cos S)) - ((S2 `2) * (sin S))) is complex real ext-real Element of REAL
((((B2 `1) * (cos S)) - ((B2 `2) * (sin S))) - (((S2 `1) * (cos S)) - ((S2 `2) * (sin S)))) ^2 is complex real ext-real Element of REAL
((((B2 `1) * (cos S)) - ((B2 `2) * (sin S))) - (((S2 `1) * (cos S)) - ((S2 `2) * (sin S)))) * ((((B2 `1) * (cos S)) - ((B2 `2) * (sin S))) - (((S2 `1) * (cos S)) - ((S2 `2) * (sin S)))) is complex real ext-real set
(B2 `1) * (sin S) is complex real ext-real Element of REAL
(B2 `2) * (cos S) is complex real ext-real Element of REAL
((B2 `1) * (sin S)) + ((B2 `2) * (cos S)) is complex real ext-real Element of REAL
(((B2 `1) * (sin S)) + ((B2 `2) * (cos S))) ^2 is complex real ext-real Element of REAL
(((B2 `1) * (sin S)) + ((B2 `2) * (cos S))) * (((B2 `1) * (sin S)) + ((B2 `2) * (cos S))) is complex real ext-real set
2 * (((B2 `1) * (sin S)) + ((B2 `2) * (cos S))) is complex real ext-real Element of REAL
(S2 `1) * (sin S) is complex real ext-real Element of REAL
(S2 `2) * (cos S) is complex real ext-real Element of REAL
((S2 `1) * (sin S)) + ((S2 `2) * (cos S)) is complex real ext-real Element of REAL
(2 * (((B2 `1) * (sin S)) + ((B2 `2) * (cos S)))) * (((S2 `1) * (sin S)) + ((S2 `2) * (cos S))) is complex real ext-real Element of REAL
((((B2 `1) * (sin S)) + ((B2 `2) * (cos S))) ^2) - ((2 * (((B2 `1) * (sin S)) + ((B2 `2) * (cos S)))) * (((S2 `1) * (sin S)) + ((S2 `2) * (cos S)))) is complex real ext-real Element of REAL
(((S2 `1) * (sin S)) + ((S2 `2) * (cos S))) ^2 is complex real ext-real Element of REAL
(((S2 `1) * (sin S)) + ((S2 `2) * (cos S))) * (((S2 `1) * (sin S)) + ((S2 `2) * (cos S))) is complex real ext-real set
(((((B2 `1) * (sin S)) + ((B2 `2) * (cos S))) ^2) - ((2 * (((B2 `1) * (sin S)) + ((B2 `2) * (cos S)))) * (((S2 `1) * (sin S)) + ((S2 `2) * (cos S))))) + ((((S2 `1) * (sin S)) + ((S2 `2) * (cos S))) ^2) is complex real ext-real Element of REAL
(((((B2 `1) * (cos S)) - ((B2 `2) * (sin S))) - (((S2 `1) * (cos S)) - ((S2 `2) * (sin S)))) ^2) + ((((((B2 `1) * (sin S)) + ((B2 `2) * (cos S))) ^2) - ((2 * (((B2 `1) * (sin S)) + ((B2 `2) * (cos S)))) * (((S2 `1) * (sin S)) + ((S2 `2) * (cos S))))) + ((((S2 `1) * (sin S)) + ((S2 `2) * (cos S))) ^2)) is complex real ext-real Element of REAL
sqrt ((((((B2 `1) * (cos S)) - ((B2 `2) * (sin S))) - (((S2 `1) * (cos S)) - ((S2 `2) * (sin S)))) ^2) + ((((((B2 `1) * (sin S)) + ((B2 `2) * (cos S))) ^2) - ((2 * (((B2 `1) * (sin S)) + ((B2 `2) * (cos S)))) * (((S2 `1) * (sin S)) + ((S2 `2) * (cos S))))) + ((((S2 `1) * (sin S)) + ((S2 `2) * (cos S))) ^2))) is complex real ext-real Element of REAL
qq is complex Element of COMPLEX
Rotate (qq,S) is complex Element of COMPLEX
|.qq.| is complex real ext-real Element of REAL
Arg qq is complex real ext-real Element of REAL
S + (Arg qq) is complex real ext-real Element of REAL
cos (S + (Arg qq)) is complex real ext-real Element of REAL
|.qq.| * (cos (S + (Arg qq))) is complex real ext-real Element of REAL
sin (S + (Arg qq)) is complex real ext-real Element of REAL
|.qq.| * (sin (S + (Arg qq))) is complex real ext-real Element of REAL
(|.qq.| * (sin (S + (Arg qq)))) * <i> is complex set
(|.qq.| * (cos (S + (Arg qq)))) + ((|.qq.| * (sin (S + (Arg qq)))) * <i>) is complex set
Re (Rotate (qq,S)) is complex real ext-real Element of REAL
(Re (Rotate (qq,S))) - (((S2 `1) * (cos S)) - ((S2 `2) * (sin S))) is complex real ext-real Element of REAL
((Re (Rotate (qq,S))) - (((S2 `1) * (cos S)) - ((S2 `2) * (sin S)))) ^2 is complex real ext-real Element of REAL
((Re (Rotate (qq,S))) - (((S2 `1) * (cos S)) - ((S2 `2) * (sin S)))) * ((Re (Rotate (qq,S))) - (((S2 `1) * (cos S)) - ((S2 `2) * (sin S)))) is complex real ext-real set
(((B2 `1) * (sin S)) + ((B2 `2) * (cos S))) - (((S2 `1) * (sin S)) + ((S2 `2) * (cos S))) is complex real ext-real Element of REAL
((((B2 `1) * (sin S)) + ((B2 `2) * (cos S))) - (((S2 `1) * (sin S)) + ((S2 `2) * (cos S)))) ^2 is complex real ext-real Element of REAL
((((B2 `1) * (sin S)) + ((B2 `2) * (cos S))) - (((S2 `1) * (sin S)) + ((S2 `2) * (cos S)))) * ((((B2 `1) * (sin S)) + ((B2 `2) * (cos S))) - (((S2 `1) * (sin S)) + ((S2 `2) * (cos S)))) is complex real ext-real set
(((Re (Rotate (qq,S))) - (((S2 `1) * (cos S)) - ((S2 `2) * (sin S)))) ^2) + (((((B2 `1) * (sin S)) + ((B2 `2) * (cos S))) - (((S2 `1) * (sin S)) + ((S2 `2) * (cos S)))) ^2) is complex real ext-real Element of REAL
sqrt ((((Re (Rotate (qq,S))) - (((S2 `1) * (cos S)) - ((S2 `2) * (sin S)))) ^2) + (((((B2 `1) * (sin S)) + ((B2 `2) * (cos S))) - (((S2 `1) * (sin S)) + ((S2 `2) * (cos S)))) ^2)) is complex real ext-real Element of REAL
Im (Rotate (qq,S)) is complex real ext-real Element of REAL
(Im (Rotate (qq,S))) - (((S2 `1) * (sin S)) + ((S2 `2) * (cos S))) is complex real ext-real Element of REAL
((Im (Rotate (qq,S))) - (((S2 `1) * (sin S)) + ((S2 `2) * (cos S)))) ^2 is complex real ext-real Element of REAL
((Im (Rotate (qq,S))) - (((S2 `1) * (sin S)) + ((S2 `2) * (cos S)))) * ((Im (Rotate (qq,S))) - (((S2 `1) * (sin S)) + ((S2 `2) * (cos S)))) is complex real ext-real set
(((Re (Rotate (qq,S))) - (((S2 `1) * (cos S)) - ((S2 `2) * (sin S)))) ^2) + (((Im (Rotate (qq,S))) - (((S2 `1) * (sin S)) + ((S2 `2) * (cos S)))) ^2) is complex real ext-real Element of REAL
sqrt ((((Re (Rotate (qq,S))) - (((S2 `1) * (cos S)) - ((S2 `2) * (sin S)))) ^2) + (((Im (Rotate (qq,S))) - (((S2 `1) * (sin S)) + ((S2 `2) * (cos S)))) ^2)) is complex real ext-real Element of REAL
h is complex Element of COMPLEX
Rotate (h,S) is complex Element of COMPLEX
|.h.| is complex real ext-real Element of REAL
Arg h is complex real ext-real Element of REAL
S + (Arg h) is complex real ext-real Element of REAL
cos (S + (Arg h)) is complex real ext-real Element of REAL
|.h.| * (cos (S + (Arg h))) is complex real ext-real Element of REAL
sin (S + (Arg h)) is complex real ext-real Element of REAL
|.h.| * (sin (S + (Arg h))) is complex real ext-real Element of REAL
(|.h.| * (sin (S + (Arg h)))) * <i> is complex set
(|.h.| * (cos (S + (Arg h)))) + ((|.h.| * (sin (S + (Arg h)))) * <i>) is complex set
Re (Rotate (h,S)) is complex real ext-real Element of REAL
(Re (Rotate (qq,S))) - (Re (Rotate (h,S))) is complex real ext-real Element of REAL
((Re (Rotate (qq,S))) - (Re (Rotate (h,S)))) ^2 is complex real ext-real Element of REAL
((Re (Rotate (qq,S))) - (Re (Rotate (h,S)))) * ((Re (Rotate (qq,S))) - (Re (Rotate (h,S)))) is complex real ext-real set
(((Re (Rotate (qq,S))) - (Re (Rotate (h,S)))) ^2) + (((Im (Rotate (qq,S))) - (((S2 `1) * (sin S)) + ((S2 `2) * (cos S)))) ^2) is complex real ext-real Element of REAL
sqrt ((((Re (Rotate (qq,S))) - (Re (Rotate (h,S)))) ^2) + (((Im (Rotate (qq,S))) - (((S2 `1) * (sin S)) + ((S2 `2) * (cos S)))) ^2)) is complex real ext-real Element of REAL
Im (Rotate (h,S)) is complex real ext-real Element of REAL
(Im (Rotate (qq,S))) - (Im (Rotate (h,S))) is complex real ext-real Element of REAL
((Im (Rotate (qq,S))) - (Im (Rotate (h,S)))) ^2 is complex real ext-real Element of REAL
((Im (Rotate (qq,S))) - (Im (Rotate (h,S)))) * ((Im (Rotate (qq,S))) - (Im (Rotate (h,S)))) is complex real ext-real set
(((Re (Rotate (qq,S))) - (Re (Rotate (h,S)))) ^2) + (((Im (Rotate (qq,S))) - (Im (Rotate (h,S)))) ^2) is complex real ext-real Element of REAL
sqrt ((((Re (Rotate (qq,S))) - (Re (Rotate (h,S)))) ^2) + (((Im (Rotate (qq,S))) - (Im (Rotate (h,S)))) ^2)) is complex real ext-real Element of REAL
dist (|[(Re (Rotate (((B2 `1) + ((B2 `2) * <i>)),S))),(Im (Rotate (((B2 `1) + ((B2 `2) * <i>)),S)))]|,|[(Re (Rotate (((S2 `1) + ((S2 `2) * <i>)),S))),(Im (Rotate (((S2 `1) + ((S2 `2) * <i>)),S)))]|) is complex real ext-real Element of REAL
arg is V40(2) V98() V141() Element of the carrier of (TOP-REAL 2)
dist (|[(Re (Rotate (((B2 `1) + ((B2 `2) * <i>)),S))),(Im (Rotate (((B2 `1) + ((B2 `2) * <i>)),S)))]|,arg) is complex real ext-real Element of REAL
fB is V40(2) V98() V141() Element of the carrier of (TOP-REAL 2)
dist (fB,arg) is complex real ext-real Element of REAL
dist ((A1 . A2),(A1 . B1)) is complex real ext-real Element of REAL
S is V40(2) V98() V141() Element of the carrier of (TOP-REAL 2)
f is V40(2) V98() V141() Element of the carrier of (TOP-REAL 2)
s is Element of K6( the carrier of (TOP-REAL 2))
s is complex real ext-real set
A1 is complex real ext-real set
A2 is complex real ext-real set
AffineMap (s,A1,s,A2) 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)))
(AffineMap (s,A1,s,A2)) .: s is Element of K6( the carrier of (TOP-REAL 2))
(AffineMap (s,A1,s,A2)) . S is V40(2) V98() V141() Element of the carrier of (TOP-REAL 2)
(AffineMap (s,A1,s,A2)) . f is V40(2) V98() V141() Element of the carrier of (TOP-REAL 2)
dom (AffineMap (s,A1,s,A2)) is non empty Element of K6( the carrier of (TOP-REAL 2))
dist (((AffineMap (s,A1,s,A2)) . S),((AffineMap (s,A1,s,A2)) . f)) is complex real ext-real Element of REAL
fB is V40(2) V98() V141() Element of the carrier of (TOP-REAL 2)
arg is V40(2) V98() V141() Element of the carrier of (TOP-REAL 2)
dist (fB,arg) is complex real ext-real Element of REAL
qq is set
(AffineMap (s,A1,s,A2)) . qq is set
h0 is set
(AffineMap (s,A1,s,A2)) . h0 is set
h is V40(2) V98() V141() Element of the carrier of (TOP-REAL 2)
h `1 is complex real ext-real Element of REAL
h is V40(2) V98() V141() Element of the carrier of (TOP-REAL 2)
h `1 is complex real ext-real Element of REAL
(h `1) - (h `1) is complex real ext-real Element of REAL
((h `1) - (h `1)) ^2 is complex real ext-real Element of REAL
((h `1) - (h `1)) * ((h `1) - (h `1)) is complex real ext-real set
h `2 is complex real ext-real Element of REAL
h `2 is complex real ext-real Element of REAL
(h `2) - (h `2) is complex real ext-real Element of REAL
((h `2) - (h `2)) ^2 is complex real ext-real Element of REAL
((h `2) - (h `2)) * ((h `2) - (h `2)) is complex real ext-real set
S `1 is complex real ext-real Element of REAL
f `1 is complex real ext-real Element of REAL
(S `1) - (f `1) is complex real ext-real Element of REAL
((S `1) - (f `1)) ^2 is complex real ext-real Element of REAL
((S `1) - (f `1)) * ((S `1) - (f `1)) is complex real ext-real set
S `2 is complex real ext-real Element of REAL
f `2 is complex real ext-real Element of REAL
(S `2) - (f `2) is complex real ext-real Element of REAL
((S `2) - (f `2)) ^2 is complex real ext-real Element of REAL
((S `2) - (f `2)) * ((S `2) - (f `2)) is complex real ext-real set
s ^2 is complex real ext-real set
s * s is complex real ext-real set
sqrt (s ^2) is complex real ext-real set
s * (S `1) is complex real ext-real Element of REAL
(s * (S `1)) + A1 is complex real ext-real Element of REAL
s * (S `2) is complex real ext-real Element of REAL
(s * (S `2)) + A2 is complex real ext-real Element of REAL
|[((s * (S `1)) + A1),((s * (S `2)) + A2)]| is V40(2) V98() V141() Element of the carrier of (TOP-REAL 2)
dist (|[((s * (S `1)) + A1),((s * (S `2)) + A2)]|,((AffineMap (s,A1,s,A2)) . f)) is complex real ext-real Element of REAL
s * (f `1) is complex real ext-real Element of REAL
(s * (f `1)) + A1 is complex real ext-real Element of REAL
s * (f `2) is complex real ext-real Element of REAL
(s * (f `2)) + A2 is complex real ext-real Element of REAL
|[((s * (f `1)) + A1),((s * (f `2)) + A2)]| is V40(2) V98() V141() Element of the carrier of (TOP-REAL 2)
dist (|[((s * (S `1)) + A1),((s * (S `2)) + A2)]|,|[((s * (f `1)) + A1),((s * (f `2)) + A2)]|) is complex real ext-real Element of REAL
|[((s * (S `1)) + A1),((s * (S `2)) + A2)]| `1 is complex real ext-real Element of REAL
|[((s * (f `1)) + A1),((s * (f `2)) + A2)]| `1 is complex real ext-real Element of REAL
(|[((s * (S `1)) + A1),((s * (S `2)) + A2)]| `1) - (|[((s * (f `1)) + A1),((s * (f `2)) + A2)]| `1) is complex real ext-real Element of REAL
((|[((s * (S `1)) + A1),((s * (S `2)) + A2)]| `1) - (|[((s * (f `1)) + A1),((s * (f `2)) + A2)]| `1)) ^2 is complex real ext-real Element of REAL
((|[((s * (S `1)) + A1),((s * (S `2)) + A2)]| `1) - (|[((s * (f `1)) + A1),((s * (f `2)) + A2)]| `1)) * ((|[((s * (S `1)) + A1),((s * (S `2)) + A2)]| `1) - (|[((s * (f `1)) + A1),((s * (f `2)) + A2)]| `1)) is complex real ext-real set
|[((s * (S `1)) + A1),((s * (S `2)) + A2)]| `2 is complex real ext-real Element of REAL
|[((s * (f `1)) + A1),((s * (f `2)) + A2)]| `2 is complex real ext-real Element of REAL
(|[((s * (S `1)) + A1),((s * (S `2)) + A2)]| `2) - (|[((s * (f `1)) + A1),((s * (f `2)) + A2)]| `2) is complex real ext-real Element of REAL
((|[((s * (S `1)) + A1),((s * (S `2)) + A2)]| `2) - (|[((s * (f `1)) + A1),((s * (f `2)) + A2)]| `2)) ^2 is complex real ext-real Element of REAL
((|[((s * (S `1)) + A1),((s * (S `2)) + A2)]| `2) - (|[((s * (f `1)) + A1),((s * (f `2)) + A2)]| `2)) * ((|[((s * (S `1)) + A1),((s * (S `2)) + A2)]| `2) - (|[((s * (f `1)) + A1),((s * (f `2)) + A2)]| `2)) is complex real ext-real set
(((|[((s * (S `1)) + A1),((s * (S `2)) + A2)]| `1) - (|[((s * (f `1)) + A1),((s * (f `2)) + A2)]| `1)) ^2) + (((|[((s * (S `1)) + A1),((s * (S `2)) + A2)]| `2) - (|[((s * (f `1)) + A1),((s * (f `2)) + A2)]| `2)) ^2) is complex real ext-real Element of REAL
sqrt ((((|[((s * (S `1)) + A1),((s * (S `2)) + A2)]| `1) - (|[((s * (f `1)) + A1),((s * (f `2)) + A2)]| `1)) ^2) + (((|[((s * (S `1)) + A1),((s * (S `2)) + A2)]| `2) - (|[((s * (f `1)) + A1),((s * (f `2)) + A2)]| `2)) ^2)) is complex real ext-real Element of REAL
((s * (S `1)) + A1) - (|[((s * (f `1)) + A1),((s * (f `2)) + A2)]| `1) is complex real ext-real Element of REAL
(((s * (S `1)) + A1) - (|[((s * (f `1)) + A1),((s * (f `2)) + A2)]| `1)) ^2 is complex real ext-real Element of REAL
(((s * (S `1)) + A1) - (|[((s * (f `1)) + A1),((s * (f `2)) + A2)]| `1)) * (((s * (S `1)) + A1) - (|[((s * (f `1)) + A1),((s * (f `2)) + A2)]| `1)) is complex real ext-real set
((((s * (S `1)) + A1) - (|[((s * (f `1)) + A1),((s * (f `2)) + A2)]| `1)) ^2) + (((|[((s * (S `1)) + A1),((s * (S `2)) + A2)]| `2) - (|[((s * (f `1)) + A1),((s * (f `2)) + A2)]| `2)) ^2) is complex real ext-real Element of REAL
sqrt (((((s * (S `1)) + A1) - (|[((s * (f `1)) + A1),((s * (f `2)) + A2)]| `1)) ^2) + (((|[((s * (S `1)) + A1),((s * (S `2)) + A2)]| `2) - (|[((s * (f `1)) + A1),((s * (f `2)) + A2)]| `2)) ^2)) is complex real ext-real Element of REAL
((s * (S `1)) + A1) - ((s * (f `1)) + A1) is complex real ext-real Element of REAL
(((s * (S `1)) + A1) - ((s * (f `1)) + A1)) ^2 is complex real ext-real Element of REAL
(((s * (S `1)) + A1) - ((s * (f `1)) + A1)) * (((s * (S `1)) + A1) - ((s * (f `1)) + A1)) is complex real ext-real set
((((s * (S `1)) + A1) - ((s * (f `1)) + A1)) ^2) + (((|[((s * (S `1)) + A1),((s * (S `2)) + A2)]| `2) - (|[((s * (f `1)) + A1),((s * (f `2)) + A2)]| `2)) ^2) is complex real ext-real Element of REAL
sqrt (((((s * (S `1)) + A1) - ((s * (f `1)) + A1)) ^2) + (((|[((s * (S `1)) + A1),((s * (S `2)) + A2)]| `2) - (|[((s * (f `1)) + A1),((s * (f `2)) + A2)]| `2)) ^2)) is complex real ext-real Element of REAL
((s * (S `2)) + A2) - (|[((s * (f `1)) + A1),((s * (f `2)) + A2)]| `2) is complex real ext-real Element of REAL
(((s * (S `2)) + A2) - (|[((s * (f `1)) + A1),((s * (f `2)) + A2)]| `2)) ^2 is complex real ext-real Element of REAL
(((s * (S `2)) + A2) - (|[((s * (f `1)) + A1),((s * (f `2)) + A2)]| `2)) * (((s * (S `2)) + A2) - (|[((s * (f `1)) + A1),((s * (f `2)) + A2)]| `2)) is complex real ext-real set
((((s * (S `1)) + A1) - ((s * (f `1)) + A1)) ^2) + ((((s * (S `2)) + A2) - (|[((s * (f `1)) + A1),((s * (f `2)) + A2)]| `2)) ^2) is complex real ext-real Element of REAL
sqrt (((((s * (S `1)) + A1) - ((s * (f `1)) + A1)) ^2) + ((((s * (S `2)) + A2) - (|[((s * (f `1)) + A1),((s * (f `2)) + A2)]| `2)) ^2)) is complex real ext-real Element of REAL
((s * (S `2)) + A2) - ((s * (f `2)) + A2) is complex real ext-real Element of REAL
(((s * (S `2)) + A2) - ((s * (f `2)) + A2)) ^2 is complex real ext-real Element of REAL
(((s * (S `2)) + A2) - ((s * (f `2)) + A2)) * (((s * (S `2)) + A2) - ((s * (f `2)) + A2)) is complex real ext-real set
((((s * (S `1)) + A1) - ((s * (f `1)) + A1)) ^2) + ((((s * (S `2)) + A2) - ((s * (f `2)) + A2)) ^2) is complex real ext-real Element of REAL
sqrt (((((s * (S `1)) + A1) - ((s * (f `1)) + A1)) ^2) + ((((s * (S `2)) + A2) - ((s * (f `2)) + A2)) ^2)) is complex real ext-real Element of REAL
(((S `1) - (f `1)) ^2) + (((S `2) - (f `2)) ^2) is complex real ext-real Element of REAL
(s ^2) * ((((S `1) - (f `1)) ^2) + (((S `2) - (f `2)) ^2)) is complex real ext-real Element of REAL
sqrt ((s ^2) * ((((S `1) - (f `1)) ^2) + (((S `2) - (f `2)) ^2))) is complex real ext-real Element of REAL
sqrt ((((S `1) - (f `1)) ^2) + (((S `2) - (f `2)) ^2)) is complex real ext-real Element of REAL
(sqrt (s ^2)) * (sqrt ((((S `1) - (f `1)) ^2) + (((S `2) - (f `2)) ^2))) is complex real ext-real Element of REAL
dist (S,f) is complex real ext-real Element of REAL
(sqrt (s ^2)) * (dist (S,f)) is complex real ext-real Element of REAL
s * (h `1) is complex real ext-real Element of REAL
(s * (h `1)) + A1 is complex real ext-real Element of REAL
s * (h `2) is complex real ext-real Element of REAL
(s * (h `2)) + A2 is complex real ext-real Element of REAL
|[((s * (h `1)) + A1),((s * (h `2)) + A2)]| is V40(2) V98() V141() Element of the carrier of (TOP-REAL 2)
(AffineMap (s,A1,s,A2)) . h is V40(2) V98() V141() Element of the carrier of (TOP-REAL 2)
dist (|[((s * (h `1)) + A1),((s * (h `2)) + A2)]|,((AffineMap (s,A1,s,A2)) . h)) is complex real ext-real Element of REAL
s * (h `1) is complex real ext-real Element of REAL
(s * (h `1)) + A1 is complex real ext-real Element of REAL
s * (h `2) is complex real ext-real Element of REAL
(s * (h `2)) + A2 is complex real ext-real Element of REAL
|[((s * (h `1)) + A1),((s * (h `2)) + A2)]| is V40(2) V98() V141() Element of the carrier of (TOP-REAL 2)
dist (|[((s * (h `1)) + A1),((s * (h `2)) + A2)]|,|[((s * (h `1)) + A1),((s * (h `2)) + A2)]|) is complex real ext-real Element of REAL
|[((s * (h `1)) + A1),((s * (h `2)) + A2)]| `1 is complex real ext-real Element of REAL
|[((s * (h `1)) + A1),((s * (h `2)) + A2)]| `1 is complex real ext-real Element of REAL
(|[((s * (h `1)) + A1),((s * (h `2)) + A2)]| `1) - (|[((s * (h `1)) + A1),((s * (h `2)) + A2)]| `1) is complex real ext-real Element of REAL
((|[((s * (h `1)) + A1),((s * (h `2)) + A2)]| `1) - (|[((s * (h `1)) + A1),((s * (h `2)) + A2)]| `1)) ^2 is complex real ext-real Element of REAL
((|[((s * (h `1)) + A1),((s * (h `2)) + A2)]| `1) - (|[((s * (h `1)) + A1),((s * (h `2)) + A2)]| `1)) * ((|[((s * (h `1)) + A1),((s * (h `2)) + A2)]| `1) - (|[((s * (h `1)) + A1),((s * (h `2)) + A2)]| `1)) is complex real ext-real set
|[((s * (h `1)) + A1),((s * (h `2)) + A2)]| `2 is complex real ext-real Element of REAL
|[((s * (h `1)) + A1),((s * (h `2)) + A2)]| `2 is complex real ext-real Element of REAL
(|[((s * (h `1)) + A1),((s * (h `2)) + A2)]| `2) - (|[((s * (h `1)) + A1),((s * (h `2)) + A2)]| `2) is complex real ext-real Element of REAL
((|[((s * (h `1)) + A1),((s * (h `2)) + A2)]| `2) - (|[((s * (h `1)) + A1),((s * (h `2)) + A2)]| `2)) ^2 is complex real ext-real Element of REAL
((|[((s * (h `1)) + A1),((s * (h `2)) + A2)]| `2) - (|[((s * (h `1)) + A1),((s * (h `2)) + A2)]| `2)) * ((|[((s * (h `1)) + A1),((s * (h `2)) + A2)]| `2) - (|[((s * (h `1)) + A1),((s * (h `2)) + A2)]| `2)) is complex real ext-real set
(((|[((s * (h `1)) + A1),((s * (h `2)) + A2)]| `1) - (|[((s * (h `1)) + A1),((s * (h `2)) + A2)]| `1)) ^2) + (((|[((s * (h `1)) + A1),((s * (h `2)) + A2)]| `2) - (|[((s * (h `1)) + A1),((s * (h `2)) + A2)]| `2)) ^2) is complex real ext-real Element of REAL
sqrt ((((|[((s * (h `1)) + A1),((s * (h `2)) + A2)]| `1) - (|[((s * (h `1)) + A1),((s * (h `2)) + A2)]| `1)) ^2) + (((|[((s * (h `1)) + A1),((s * (h `2)) + A2)]| `2) - (|[((s * (h `1)) + A1),((s * (h `2)) + A2)]| `2)) ^2)) is complex real ext-real Element of REAL
((s * (h `1)) + A1) - (|[((s * (h `1)) + A1),((s * (h `2)) + A2)]| `1) is complex real ext-real Element of REAL
(((s * (h `1)) + A1) - (|[((s * (h `1)) + A1),((s * (h `2)) + A2)]| `1)) ^2 is complex real ext-real Element of REAL
(((s * (h `1)) + A1) - (|[((s * (h `1)) + A1),((s * (h `2)) + A2)]| `1)) * (((s * (h `1)) + A1) - (|[((s * (h `1)) + A1),((s * (h `2)) + A2)]| `1)) is complex real ext-real set
((((s * (h `1)) + A1) - (|[((s * (h `1)) + A1),((s * (h `2)) + A2)]| `1)) ^2) + (((|[((s * (h `1)) + A1),((s * (h `2)) + A2)]| `2) - (|[((s * (h `1)) + A1),((s * (h `2)) + A2)]| `2)) ^2) is complex real ext-real Element of REAL
sqrt (((((s * (h `1)) + A1) - (|[((s * (h `1)) + A1),((s * (h `2)) + A2)]| `1)) ^2) + (((|[((s * (h `1)) + A1),((s * (h `2)) + A2)]| `2) - (|[((s * (h `1)) + A1),((s * (h `2)) + A2)]| `2)) ^2)) is complex real ext-real Element of REAL
((s * (h `1)) + A1) - ((s * (h `1)) + A1) is complex real ext-real Element of REAL
(((s * (h `1)) + A1) - ((s * (h `1)) + A1)) ^2 is complex real ext-real Element of REAL
(((s * (h `1)) + A1) - ((s * (h `1)) + A1)) * (((s * (h `1)) + A1) - ((s * (h `1)) + A1)) is complex real ext-real set
((((s * (h `1)) + A1) - ((s * (h `1)) + A1)) ^2) + (((|[((s * (h `1)) + A1),((s * (h `2)) + A2)]| `2) - (|[((s * (h `1)) + A1),((s * (h `2)) + A2)]| `2)) ^2) is complex real ext-real Element of REAL
sqrt (((((s * (h `1)) + A1) - ((s * (h `1)) + A1)) ^2) + (((|[((s * (h `1)) + A1),((s * (h `2)) + A2)]| `2) - (|[((s * (h `1)) + A1),((s * (h `2)) + A2)]| `2)) ^2)) is complex real ext-real Element of REAL
((s * (h `2)) + A2) - (|[((s * (h `1)) + A1),((s * (h `2)) + A2)]| `2) is complex real ext-real Element of REAL
(((s * (h `2)) + A2) - (|[((s * (h `1)) + A1),((s * (h `2)) + A2)]| `2)) ^2 is complex real ext-real Element of REAL
(((s * (h `2)) + A2) - (|[((s * (h `1)) + A1),((s * (h `2)) + A2)]| `2)) * (((s * (h `2)) + A2) - (|[((s * (h `1)) + A1),((s * (h `2)) + A2)]| `2)) is complex real ext-real set
((((s * (h `1)) + A1) - ((s * (h `1)) + A1)) ^2) + ((((s * (h `2)) + A2) - (|[((s * (h `1)) + A1),((s * (h `2)) + A2)]| `2)) ^2) is complex real ext-real Element of REAL
sqrt (((((s * (h `1)) + A1) - ((s * (h `1)) + A1)) ^2) + ((((s * (h `2)) + A2) - (|[((s * (h `1)) + A1),((s * (h `2)) + A2)]| `2)) ^2)) is complex real ext-real Element of REAL
((s * (h `2)) + A2) - ((s * (h `2)) + A2) is complex real ext-real Element of REAL
(((s * (h `2)) + A2) - ((s * (h `2)) + A2)) ^2 is complex real ext-real Element of REAL
(((s * (h `2)) + A2) - ((s * (h `2)) + A2)) * (((s * (h `2)) + A2) - ((s * (h `2)) + A2)) is complex real ext-real set
((((s * (h `1)) + A1) - ((s * (h `1)) + A1)) ^2) + ((((s * (h `2)) + A2) - ((s * (h `2)) + A2)) ^2) is complex real ext-real Element of REAL
sqrt (((((s * (h `1)) + A1) - ((s * (h `1)) + A1)) ^2) + ((((s * (h `2)) + A2) - ((s * (h `2)) + A2)) ^2)) is complex real ext-real Element of REAL
(((h `1) - (h `1)) ^2) + (((h `2) - (h `2)) ^2) is complex real ext-real Element of REAL
(s ^2) * ((((h `1) - (h `1)) ^2) + (((h `2) - (h `2)) ^2)) is complex real ext-real Element of REAL
sqrt ((s ^2) * ((((h `1) - (h `1)) ^2) + (((h `2) - (h `2)) ^2))) is complex real ext-real Element of REAL
sqrt ((((h `1) - (h `1)) ^2) + (((h `2) - (h `2)) ^2)) is complex real ext-real Element of REAL
(sqrt (s ^2)) * (sqrt ((((h `1) - (h `1)) ^2) + (((h `2) - (h `2)) ^2))) is complex real ext-real Element of REAL
dist (h,h) is complex real ext-real Element of REAL
(sqrt (s ^2)) * (dist (h,h)) is complex real ext-real Element of REAL
S is V40(2) V98() V141() Element of the carrier of (TOP-REAL 2)
f is V40(2) V98() V141() Element of the carrier of (TOP-REAL 2)
s is Element of K6( the carrier of (TOP-REAL 2))
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) .: s is Element of K6( the carrier of (TOP-REAL 2))
(s) . S is V40(2) V98() V141() Element of the carrier of (TOP-REAL 2)
(s) . f is V40(2) V98() V141() Element of the carrier of (TOP-REAL 2)
dom (s) is non empty Element of K6( the carrier of (TOP-REAL 2))
dist (((s) . S),((s) . f)) 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
A1 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
S2 is non empty V16() V19( the carrier of (Euclid 2)) V20( the carrier of (Euclid 2)) Function-like one-to-one V26( the carrier of (Euclid 2)) quasi_total isometric Element of K6(K7( the carrier of (Euclid 2), the carrier of (Euclid 2)))
fB is set
(s) . fB is set
qq is set
(s) . qq is set
h is V40(2) V98() V141() Element of the carrier of (TOP-REAL 2)
arg is V40(2) V98() V141() Element of the carrier of (TOP-REAL 2)
dist (h,arg) is complex real ext-real Element of REAL
dist (S,f) is complex real ext-real Element of REAL
h0 is Element of the carrier of (Euclid 2)
h is Element of the carrier of (Euclid 2)
dist (h0,h) is complex real ext-real Element of REAL
F is Element of the carrier of (Euclid 2)
s1 is Element of the carrier of (Euclid 2)
dist (F,s1) is complex real ext-real Element of REAL
S2 . h0 is Element of the carrier of (Euclid 2)
S2 . h is Element of the carrier of (Euclid 2)
dist ((S2 . h0),(S2 . h)) is complex real ext-real Element of REAL
S2 . F is Element of the carrier of (Euclid 2)
S2 . s1 is Element of the carrier of (Euclid 2)
dist ((S2 . F),(S2 . s1)) is complex real ext-real Element of REAL
S is complex set
f is complex real ext-real Element of REAL
- f is complex real ext-real Element of REAL
Rotate (S,(- f)) is complex Element of COMPLEX
|.S.| is complex real ext-real Element of REAL
Arg S is complex real ext-real Element of REAL
(- f) + (Arg S) is complex real ext-real Element of REAL
cos ((- f) + (Arg S)) is complex real ext-real Element of REAL
|.S.| * (cos ((- f) + (Arg S))) is complex real ext-real Element of REAL
sin ((- f) + (Arg S)) is complex real ext-real Element of REAL
|.S.| * (sin ((- f) + (Arg S))) is complex real ext-real Element of REAL
(|.S.| * (sin ((- f) + (Arg S)))) * <i> is complex set
(|.S.| * (cos ((- f) + (Arg S)))) + ((|.S.| * (sin ((- f) + (Arg S)))) * <i>) is complex set
(2 * PI) - f is complex real ext-real Element of REAL
Rotate (S,((2 * PI) - f)) is complex Element of COMPLEX
((2 * PI) - f) + (Arg S) is complex real ext-real Element of REAL
cos (((2 * PI) - f) + (Arg S)) is complex real ext-real Element of REAL
|.S.| * (cos (((2 * PI) - f) + (Arg S))) is complex real ext-real Element of REAL
sin (((2 * PI) - f) + (Arg S)) is complex real ext-real Element of REAL
|.S.| * (sin (((2 * PI) - f) + (Arg S))) is complex real ext-real Element of REAL
(|.S.| * (sin (((2 * PI) - f) + (Arg S)))) * <i> is complex set
(|.S.| * (cos (((2 * PI) - f) + (Arg S)))) + ((|.S.| * (sin (((2 * PI) - f) + (Arg S)))) * <i>) is complex set
(2 * PI) * 1 is non empty complex real ext-real positive non negative Element of REAL
((2 * PI) * 1) + ((- f) + (Arg S)) is complex real ext-real Element of REAL
cos (((2 * PI) * 1) + ((- f) + (Arg S))) is complex real ext-real Element of REAL
|.S.| * (cos (((2 * PI) * 1) + ((- f) + (Arg S)))) is complex real ext-real Element of REAL
(|.S.| * (sin ((- f) + (Arg S)))) * <i> is complex set
(|.S.| * (cos (((2 * PI) * 1) + ((- f) + (Arg S))))) + ((|.S.| * (sin ((- f) + (Arg S)))) * <i>) is complex set
S is complex real ext-real Element of REAL
- 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)))
(2 * PI) - S is complex real ext-real Element of REAL
(((2 * PI) - 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 V40(2) V98() V141() Element of the carrier of (TOP-REAL 2)
(((2 * PI) - S)) . f is V40(2) V98() V141() Element of the carrier of (TOP-REAL 2)
f `1 is complex real ext-real Element of REAL
f `2 is complex real ext-real Element of REAL
(f `2) * <i> is complex set
(f `1) + ((f `2) * <i>) is complex set
Rotate (((f `1) + ((f `2) * <i>)),((2 * PI) - S)) is complex Element of COMPLEX
|.((f `1) + ((f `2) * <i>)).| is complex real ext-real Element of REAL
Arg ((f `1) + ((f `2) * <i>)) is complex real ext-real Element of REAL
((2 * PI) - S) + (Arg ((f `1) + ((f `2) * <i>))) is complex real ext-real Element of REAL
cos (((2 * PI) - S) + (Arg ((f `1) + ((f `2) * <i>)))) is complex real ext-real Element of REAL
|.((f `1) + ((f `2) * <i>)).| * (cos (((2 * PI) - S) + (Arg ((f `1) + ((f `2) * <i>))))) is complex real ext-real Element of REAL
sin (((2 * PI) - S) + (Arg ((f `1) + ((f `2) * <i>)))) is complex real ext-real Element of REAL
|.((f `1) + ((f `2) * <i>)).| * (sin (((2 * PI) - S) + (Arg ((f `1) + ((f `2) * <i>))))) is complex real ext-real Element of REAL
(|.((f `1) + ((f `2) * <i>)).| * (sin (((2 * PI) - S) + (Arg ((f `1) + ((f `2) * <i>)))))) * <i> is complex set
(|.((f `1) + ((f `2) * <i>)).| * (cos (((2 * PI) - S) + (Arg ((f `1) + ((f `2) * <i>)))))) + ((|.((f `1) + ((f `2) * <i>)).| * (sin (((2 * PI) - S) + (Arg ((f `1) + ((f `2) * <i>)))))) * <i>) is complex set
Re (Rotate (((f `1) + ((f `2) * <i>)),((2 * PI) - S))) is complex real ext-real Element of REAL
Im (Rotate (((f `1) + ((f `2) * <i>)),((2 * PI) - S))) is complex real ext-real Element of REAL
|[(Re (Rotate (((f `1) + ((f `2) * <i>)),((2 * PI) - S)))),(Im (Rotate (((f `1) + ((f `2) * <i>)),((2 * PI) - S))))]| is V40(2) V98() V141() Element of the carrier of (TOP-REAL 2)
Rotate (((f `1) + ((f `2) * <i>)),(- S)) is complex Element of COMPLEX
(- S) + (Arg ((f `1) + ((f `2) * <i>))) is complex real ext-real Element of REAL
cos ((- S) + (Arg ((f `1) + ((f `2) * <i>)))) is complex real ext-real Element of REAL
|.((f `1) + ((f `2) * <i>)).| * (cos ((- S) + (Arg ((f `1) + ((f `2) * <i>))))) is complex real ext-real Element of REAL
sin ((- S) + (Arg ((f `1) + ((f `2) * <i>)))) is complex real ext-real Element of REAL
|.((f `1) + ((f `2) * <i>)).| * (sin ((- S) + (Arg ((f `1) + ((f `2) * <i>))))) is complex real ext-real Element of REAL
(|.((f `1) + ((f `2) * <i>)).| * (sin ((- S) + (Arg ((f `1) + ((f `2) * <i>)))))) * <i> is complex set
(|.((f `1) + ((f `2) * <i>)).| * (cos ((- S) + (Arg ((f `1) + ((f `2) * <i>)))))) + ((|.((f `1) + ((f `2) * <i>)).| * (sin ((- S) + (Arg ((f `1) + ((f `2) * <i>)))))) * <i>) is complex set
Re (Rotate (((f `1) + ((f `2) * <i>)),(- S))) is complex real ext-real Element of REAL
|[(Re (Rotate (((f `1) + ((f `2) * <i>)),(- S)))),(Im (Rotate (((f `1) + ((f `2) * <i>)),((2 * PI) - S))))]| is V40(2) V98() V141() Element of the carrier of (TOP-REAL 2)
Im (Rotate (((f `1) + ((f `2) * <i>)),(- S))) is complex real ext-real Element of REAL
|[(Re (Rotate (((f `1) + ((f `2) * <i>)),(- S)))),(Im (Rotate (((f `1) + ((f `2) * <i>)),(- S))))]| is V40(2) V98() V141() Element of the carrier of (TOP-REAL 2)
S is TopSpace-like TopStruct
the carrier of S is set
f is TopSpace-like TopStruct
the carrier of f is set
K7( the carrier of S, the carrier of f) is V16() set
K6(K7( the carrier of S, the carrier of f)) is set
the topology of S is non empty 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, the topology of S #) is strict TopSpace-like TopStruct
the carrier of TopStruct(# the carrier of S, the topology of S #) is set
the topology of f is non empty Element of K6(K6( the carrier of f))
K6( the carrier of f) is set
K6(K6( the carrier of f)) is set
TopStruct(# the carrier of f, the topology of f #) is strict TopSpace-like TopStruct
the carrier of TopStruct(# the carrier of f, the topology of f #) is set
K7( the carrier of TopStruct(# the carrier of S, the topology of S #), the carrier of TopStruct(# the carrier of f, the topology of f #)) is V16() set
K6(K7( the carrier of TopStruct(# the carrier of S, the topology of S #), the carrier of TopStruct(# the carrier of f, the topology of f #))) is set
s is V16() V19( the carrier of S) V20( the carrier of f) Function-like quasi_total Element of K6(K7( the carrier of S, the carrier of f))
s is V16() V19( the carrier of TopStruct(# the carrier of S, the topology of S #)) V20( the carrier of TopStruct(# the carrier of f, the topology of f #)) Function-like quasi_total Element of K6(K7( the carrier of TopStruct(# the carrier of S, the topology of S #), the carrier of TopStruct(# the carrier of f, the topology of f #)))
dom s is Element of K6( the carrier of S)
[#] TopStruct(# the carrier of S, the topology of S #) is non proper closed Element of K6( the carrier of TopStruct(# the carrier of S, the topology of S #))
K6( the carrier of TopStruct(# the carrier of S, the topology of S #)) is set
rng s is Element of K6( the carrier of f)
[#] TopStruct(# the carrier of f, the topology of f #) is non proper closed Element of K6( the carrier of TopStruct(# the carrier of f, the topology of f #))
K6( the carrier of TopStruct(# the carrier of f, the topology of f #)) is set
[#] S is non proper closed Element of K6( the carrier of S)
[#] f is non proper closed Element of K6( the carrier of f)
s " is V16() V19( the carrier of f) V20( the carrier of S) Function-like quasi_total Element of K6(K7( the carrier of f, the carrier of S))
K7( the carrier of f, the carrier of S) is V16() set
K6(K7( the carrier of f, the carrier of S)) is set
s " is V16() V19( the carrier of TopStruct(# the carrier of f, the topology of f #)) V20( the carrier of TopStruct(# the carrier of S, the topology of S #)) Function-like quasi_total Element of K6(K7( the carrier of TopStruct(# the carrier of f, the topology of f #), the carrier of TopStruct(# the carrier of S, the topology of S #)))
K7( the carrier of TopStruct(# the carrier of f, the topology of f #), the carrier of TopStruct(# the carrier of S, the topology of S #)) is V16() set
K6(K7( the carrier of TopStruct(# the carrier of f, the topology of f #), the carrier of TopStruct(# the carrier of S, the topology of S #))) is set
S is non empty compact being_simple_closed_curve Element of K6( the carrier of (TOP-REAL 2))
s is V40(2) V98() V141() Element of the carrier of (TOP-REAL 2)
s is V40(2) V98() V141() Element of the carrier of (TOP-REAL 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)
A1 `1 is complex real ext-real Element of REAL
- (A1 `1) is complex real ext-real Element of REAL
A1 `2 is complex real ext-real Element of REAL
- (A1 `2) is complex real ext-real Element of REAL
AffineMap (1,(- (A1 `1)),1,(- (A1 `2))) 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)))
B1 is non empty V16() V19( the carrier of (TOP-REAL 2)) V20( the carrier of (TOP-REAL 2)) Function-like one-to-one V26( the carrier of (TOP-REAL 2)) quasi_total onto bijective continuous being_homeomorphism Element of K6(K7( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)))
B1 .: S is Element of K6( the carrier of (TOP-REAL 2))
B1 . A1 is V40(2) V98() V141() Element of the carrier of (TOP-REAL 2)
B1 . A2 is V40(2) V98() V141() Element of the carrier of (TOP-REAL 2)
(B1 . A2) `1 is complex real ext-real Element of REAL
(B1 . A2) `2 is complex real ext-real Element of REAL
((B1 . A2) `2) * <i> is complex set
((B1 . A2) `1) + (((B1 . A2) `2) * <i>) is complex set
Arg (((B1 . A2) `1) + (((B1 . A2) `2) * <i>)) is complex real ext-real Element of REAL
- (Arg (((B1 . A2) `1) + (((B1 . A2) `2) * <i>))) is complex real ext-real Element of REAL
((- (Arg (((B1 . A2) `1) + (((B1 . A2) `2) * <i>))))) 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)))
(2 * PI) - (Arg (((B1 . A2) `1) + (((B1 . A2) `2) * <i>))) is complex real ext-real Element of REAL
(((2 * PI) - (Arg (((B1 . A2) `1) + (((B1 . A2) `2) * <i>))))) 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)))
(((2 * PI) - (Arg (((B1 . A2) `1) + (((B1 . A2) `2) * <i>))))) .: (B1 .: S) is Element of K6( the carrier of (TOP-REAL 2))
(((2 * PI) - (Arg (((B1 . A2) `1) + (((B1 . A2) `2) * <i>))))) . (B1 . A1) is V40(2) V98() V141() Element of the carrier of (TOP-REAL 2)
(((2 * PI) - (Arg (((B1 . A2) `1) + (((B1 . A2) `2) * <i>))))) . (B1 . A2) is V40(2) V98() V141() Element of the carrier of (TOP-REAL 2)
f is complex Element of COMPLEX
Rotate (f,(- (Arg (((B1 . A2) `1) + (((B1 . A2) `2) * <i>))))) is complex Element of COMPLEX
|.f.| is complex real ext-real Element of REAL
Arg f is complex real ext-real Element of REAL
(- (Arg (((B1 . A2) `1) + (((B1 . A2) `2) * <i>)))) + (Arg f) is complex real ext-real Element of REAL
cos ((- (Arg (((B1 . A2) `1) + (((B1 . A2) `2) * <i>)))) + (Arg f)) is complex real ext-real Element of REAL
|.f.| * (cos ((- (Arg (((B1 . A2) `1) + (((B1 . A2) `2) * <i>)))) + (Arg f))) is complex real ext-real Element of REAL
sin ((- (Arg (((B1 . A2) `1) + (((B1 . A2) `2) * <i>)))) + (Arg f)) is complex real ext-real Element of REAL
|.f.| * (sin ((- (Arg (((B1 . A2) `1) + (((B1 . A2) `2) * <i>)))) + (Arg f))) is complex real ext-real Element of REAL
(|.f.| * (sin ((- (Arg (((B1 . A2) `1) + (((B1 . A2) `2) * <i>)))) + (Arg f)))) * <i> is complex set
(|.f.| * (cos ((- (Arg (((B1 . A2) `1) + (((B1 . A2) `2) * <i>)))) + (Arg f)))) + ((|.f.| * (sin ((- (Arg (((B1 . A2) `1) + (((B1 . A2) `2) * <i>)))) + (Arg f)))) * <i>) is complex set
h0 is non empty V16() V19( the carrier of (TopSpaceMetr (Euclid 2))) V20( the carrier of (TopSpaceMetr (Euclid 2))) Function-like one-to-one V26( the carrier of (TopSpaceMetr (Euclid 2))) quasi_total onto bijective continuous being_homeomorphism ( Euclid 2) Element of K6(K7( the carrier of (TopSpaceMetr (Euclid 2)), the carrier of (TopSpaceMetr (Euclid 2))))
h is non empty V16() V19( the carrier of (TOP-REAL 2)) V20( the carrier of (TOP-REAL 2)) Function-like one-to-one V26( the carrier of (TOP-REAL 2)) quasi_total onto bijective continuous being_homeomorphism Element of K6(K7( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)))
h .: (B1 .: S) is Element of K6( the carrier of (TOP-REAL 2))
h . (B1 . A1) is V40(2) V98() V141() Element of the carrier of (TOP-REAL 2)
h . (B1 . A2) is V40(2) V98() V141() Element of the carrier of (TOP-REAL 2)
1 * (A1 `1) is complex real ext-real Element of REAL
(1 * (A1 `1)) + (- (A1 `1)) is complex real ext-real Element of REAL
1 * (A1 `2) is complex real ext-real Element of REAL
(1 * (A1 `2)) + (- (A1 `2)) is complex real ext-real Element of REAL
|[((1 * (A1 `1)) + (- (A1 `1))),((1 * (A1 `2)) + (- (A1 `2)))]| is V40(2) V98() V141() Element of the carrier of (TOP-REAL 2)
|[0,0]| is V40(2) V98() V141() Element of the carrier of (TOP-REAL 2)
|[0,0]| `1 is complex real ext-real Element of REAL
|[0,0]| `2 is complex real ext-real Element of REAL
(|[0,0]| `2) * <i> is complex set
(|[0,0]| `1) + ((|[0,0]| `2) * <i>) is complex set
Rotate (((|[0,0]| `1) + ((|[0,0]| `2) * <i>)),(- (Arg (((B1 . A2) `1) + (((B1 . A2) `2) * <i>))))) is complex Element of COMPLEX
|.((|[0,0]| `1) + ((|[0,0]| `2) * <i>)).| is complex real ext-real Element of REAL
Arg ((|[0,0]| `1) + ((|[0,0]| `2) * <i>)) is complex real ext-real Element of REAL
(- (Arg (((B1 . A2) `1) + (((B1 . A2) `2) * <i>)))) + (Arg ((|[0,0]| `1) + ((|[0,0]| `2) * <i>))) is complex real ext-real Element of REAL
cos ((- (Arg (((B1 . A2) `1) + (((B1 . A2) `2) * <i>)))) + (Arg ((|[0,0]| `1) + ((|[0,0]| `2) * <i>)))) is complex real ext-real Element of REAL
|.((|[0,0]| `1) + ((|[0,0]| `2) * <i>)).| * (cos ((- (Arg (((B1 . A2) `1) + (((B1 . A2) `2) * <i>)))) + (Arg ((|[0,0]| `1) + ((|[0,0]| `2) * <i>))))) is complex real ext-real Element of REAL
sin ((- (Arg (((B1 . A2) `1) + (((B1 . A2) `2) * <i>)))) + (Arg ((|[0,0]| `1) + ((|[0,0]| `2) * <i>)))) is complex real ext-real Element of REAL
|.((|[0,0]| `1) + ((|[0,0]| `2) * <i>)).| * (sin ((- (Arg (((B1 . A2) `1) + (((B1 . A2) `2) * <i>)))) + (Arg ((|[0,0]| `1) + ((|[0,0]| `2) * <i>))))) is complex real ext-real Element of REAL
(|.((|[0,0]| `1) + ((|[0,0]| `2) * <i>)).| * (sin ((- (Arg (((B1 . A2) `1) + (((B1 . A2) `2) * <i>)))) + (Arg ((|[0,0]| `1) + ((|[0,0]| `2) * <i>)))))) * <i> is complex set
(|.((|[0,0]| `1) + ((|[0,0]| `2) * <i>)).| * (cos ((- (Arg (((B1 . A2) `1) + (((B1 . A2) `2) * <i>)))) + (Arg ((|[0,0]| `1) + ((|[0,0]| `2) * <i>)))))) + ((|.((|[0,0]| `1) + ((|[0,0]| `2) * <i>)).| * (sin ((- (Arg (((B1 . A2) `1) + (((B1 . A2) `2) * <i>)))) + (Arg ((|[0,0]| `1) + ((|[0,0]| `2) * <i>)))))) * <i>) is complex set
Re (Rotate (((|[0,0]| `1) + ((|[0,0]| `2) * <i>)),(- (Arg (((B1 . A2) `1) + (((B1 . A2) `2) * <i>)))))) is complex real ext-real Element of REAL
Im (Rotate (((|[0,0]| `1) + ((|[0,0]| `2) * <i>)),(- (Arg (((B1 . A2) `1) + (((B1 . A2) `2) * <i>)))))) is complex real ext-real Element of REAL
|[(Re (Rotate (((|[0,0]| `1) + ((|[0,0]| `2) * <i>)),(- (Arg (((B1 . A2) `1) + (((B1 . A2) `2) * <i>))))))),(Im (Rotate (((|[0,0]| `1) + ((|[0,0]| `2) * <i>)),(- (Arg (((B1 . A2) `1) + (((B1 . A2) `2) * <i>)))))))]| is V40(2) V98() V141() Element of the carrier of (TOP-REAL 2)
0 + ((|[0,0]| `2) * <i>) is complex set
Rotate ((0 + ((|[0,0]| `2) * <i>)),(- (Arg (((B1 . A2) `1) + (((B1 . A2) `2) * <i>))))) is complex Element of COMPLEX
|.(0 + ((|[0,0]| `2) * <i>)).| is complex real ext-real Element of REAL
Arg (0 + ((|[0,0]| `2) * <i>)) is complex real ext-real Element of REAL
(- (Arg (((B1 . A2) `1) + (((B1 . A2) `2) * <i>)))) + (Arg (0 + ((|[0,0]| `2) * <i>))) is complex real ext-real Element of REAL
cos ((- (Arg (((B1 . A2) `1) + (((B1 . A2) `2) * <i>)))) + (Arg (0 + ((|[0,0]| `2) * <i>)))) is complex real ext-real Element of REAL
|.(0 + ((|[0,0]| `2) * <i>)).| * (cos ((- (Arg (((B1 . A2) `1) + (((B1 . A2) `2) * <i>)))) + (Arg (0 + ((|[0,0]| `2) * <i>))))) is complex real ext-real Element of REAL
sin ((- (Arg (((B1 . A2) `1) + (((B1 . A2) `2) * <i>)))) + (Arg (0 + ((|[0,0]| `2) * <i>)))) is complex real ext-real Element of REAL
|.(0 + ((|[0,0]| `2) * <i>)).| * (sin ((- (Arg (((B1 . A2) `1) + (((B1 . A2) `2) * <i>)))) + (Arg (0 + ((|[0,0]| `2) * <i>))))) is complex real ext-real Element of REAL
(|.(0 + ((|[0,0]| `2) * <i>)).| * (sin ((- (Arg (((B1 . A2) `1) + (((B1 . A2) `2) * <i>)))) + (Arg (0 + ((|[0,0]| `2) * <i>)))))) * <i> is complex set
(|.(0 + ((|[0,0]| `2) * <i>)).| * (cos ((- (Arg (((B1 . A2) `1) + (((B1 . A2) `2) * <i>)))) + (Arg (0 + ((|[0,0]| `2) * <i>)))))) + ((|.(0 + ((|[0,0]| `2) * <i>)).| * (sin ((- (Arg (((B1 . A2) `1) + (((B1 . A2) `2) * <i>)))) + (Arg (0 + ((|[0,0]| `2) * <i>)))))) * <i>) is complex set
Re (Rotate ((0 + ((|[0,0]| `2) * <i>)),(- (Arg (((B1 . A2) `1) + (((B1 . A2) `2) * <i>)))))) is complex real ext-real Element of REAL
|[(Re (Rotate ((0 + ((|[0,0]| `2) * <i>)),(- (Arg (((B1 . A2) `1) + (((B1 . A2) `2) * <i>))))))),(Im (Rotate (((|[0,0]| `1) + ((|[0,0]| `2) * <i>)),(- (Arg (((B1 . A2) `1) + (((B1 . A2) `2) * <i>)))))))]| is V40(2) V98() V141() Element of the carrier of (TOP-REAL 2)
0 * <i> is complex set
0 + (0 * <i>) is complex set
Rotate ((0 + (0 * <i>)),(- (Arg (((B1 . A2) `1) + (((B1 . A2) `2) * <i>))))) is complex Element of COMPLEX
|.(0 + (0 * <i>)).| is complex real ext-real Element of REAL
Arg (0 + (0 * <i>)) is complex real ext-real Element of REAL
(- (Arg (((B1 . A2) `1) + (((B1 . A2) `2) * <i>)))) + (Arg (0 + (0 * <i>))) is complex real ext-real Element of REAL
cos ((- (Arg (((B1 . A2) `1) + (((B1 . A2) `2) * <i>)))) + (Arg (0 + (0 * <i>)))) is complex real ext-real Element of REAL
|.(0 + (0 * <i>)).| * (cos ((- (Arg (((B1 . A2) `1) + (((B1 . A2) `2) * <i>)))) + (Arg (0 + (0 * <i>))))) is complex real ext-real Element of REAL
sin ((- (Arg (((B1 . A2) `1) + (((B1 . A2) `2) * <i>)))) + (Arg (0 + (0 * <i>)))) is complex real ext-real Element of REAL
|.(0 + (0 * <i>)).| * (sin ((- (Arg (((B1 . A2) `1) + (((B1 . A2) `2) * <i>)))) + (Arg (0 + (0 * <i>))))) is complex real ext-real Element of REAL
(|.(0 + (0 * <i>)).| * (sin ((- (Arg (((B1 . A2) `1) + (((B1 . A2) `2) * <i>)))) + (Arg (0 + (0 * <i>)))))) * <i> is complex set
(|.(0 + (0 * <i>)).| * (cos ((- (Arg (((B1 . A2) `1) + (((B1 . A2) `2) * <i>)))) + (Arg (0 + (0 * <i>)))))) + ((|.(0 + (0 * <i>)).| * (sin ((- (Arg (((B1 . A2) `1) + (((B1 . A2) `2) * <i>)))) + (Arg (0 + (0 * <i>)))))) * <i>) is complex set
Re (Rotate ((0 + (0 * <i>)),(- (Arg (((B1 . A2) `1) + (((B1 . A2) `2) * <i>)))))) is complex real ext-real Element of REAL
|[(Re (Rotate ((0 + (0 * <i>)),(- (Arg (((B1 . A2) `1) + (((B1 . A2) `2) * <i>))))))),(Im (Rotate (((|[0,0]| `1) + ((|[0,0]| `2) * <i>)),(- (Arg (((B1 . A2) `1) + (((B1 . A2) `2) * <i>)))))))]| is V40(2) V98() V141() Element of the carrier of (TOP-REAL 2)
Im (Rotate ((0 + ((|[0,0]| `2) * <i>)),(- (Arg (((B1 . A2) `1) + (((B1 . A2) `2) * <i>)))))) is complex real ext-real Element of REAL
|[(Re (Rotate ((0 + (0 * <i>)),(- (Arg (((B1 . A2) `1) + (((B1 . A2) `2) * <i>))))))),(Im (Rotate ((0 + ((|[0,0]| `2) * <i>)),(- (Arg (((B1 . A2) `1) + (((B1 . A2) `2) * <i>)))))))]| is V40(2) V98() V141() Element of the carrier of (TOP-REAL 2)
qq is complex Element of COMPLEX
Rotate (qq,(- (Arg (((B1 . A2) `1) + (((B1 . A2) `2) * <i>))))) is complex Element of COMPLEX
|.qq.| is complex real ext-real Element of REAL
Arg qq is complex real ext-real Element of REAL
(- (Arg (((B1 . A2) `1) + (((B1 . A2) `2) * <i>)))) + (Arg qq) is complex real ext-real Element of REAL
cos ((- (Arg (((B1 . A2) `1) + (((B1 . A2) `2) * <i>)))) + (Arg qq)) is complex real ext-real Element of REAL
|.qq.| * (cos ((- (Arg (((B1 . A2) `1) + (((B1 . A2) `2) * <i>)))) + (Arg qq))) is complex real ext-real Element of REAL
sin ((- (Arg (((B1 . A2) `1) + (((B1 . A2) `2) * <i>)))) + (Arg qq)) is complex real ext-real Element of REAL
|.qq.| * (sin ((- (Arg (((B1 . A2) `1) + (((B1 . A2) `2) * <i>)))) + (Arg qq))) is complex real ext-real Element of REAL
(|.qq.| * (sin ((- (Arg (((B1 . A2) `1) + (((B1 . A2) `2) * <i>)))) + (Arg qq)))) * <i> is complex set
(|.qq.| * (cos ((- (Arg (((B1 . A2) `1) + (((B1 . A2) `2) * <i>)))) + (Arg qq)))) + ((|.qq.| * (sin ((- (Arg (((B1 . A2) `1) + (((B1 . A2) `2) * <i>)))) + (Arg qq)))) * <i>) is complex set
|.(((B1 . A2) `1) + (((B1 . A2) `2) * <i>)).| is complex real ext-real Element of REAL
|.(((B1 . A2) `1) + (((B1 . A2) `2) * <i>)).| + (0 * <i>) is complex set
Re (|.(((B1 . A2) `1) + (((B1 . A2) `2) * <i>)).| + (0 * <i>)) is complex real ext-real Element of REAL
Im (|.(((B1 . A2) `1) + (((B1 . A2) `2) * <i>)).| + (0 * <i>)) is complex real ext-real Element of REAL
|[(Re (|.(((B1 . A2) `1) + (((B1 . A2) `2) * <i>)).| + (0 * <i>))),(Im (|.(((B1 . A2) `1) + (((B1 . A2) `2) * <i>)).| + (0 * <i>)))]| is V40(2) V98() V141() Element of the carrier of (TOP-REAL 2)
|[|.(((B1 . A2) `1) + (((B1 . A2) `2) * <i>)).|,(Im (|.(((B1 . A2) `1) + (((B1 . A2) `2) * <i>)).| + (0 * <i>)))]| is V40(2) V98() V141() Element of the carrier of (TOP-REAL 2)
|[|.(((B1 . A2) `1) + (((B1 . A2) `2) * <i>)).|,0]| is V40(2) V98() V141() Element of the carrier of (TOP-REAL 2)
(h . (B1 . A2)) `2 is complex real ext-real Element of REAL
dist (A1,A2) is complex real ext-real Element of REAL
dom B1 is non empty Element of K6( the carrier of (TOP-REAL 2))
(h . (B1 . A2)) `1 is complex real ext-real Element of REAL
dom h is non empty Element of K6( the carrier of (TOP-REAL 2))
2 / ((h . (B1 . A2)) `1) is complex real ext-real Element of REAL
AffineMap ((2 / ((h . (B1 . A2)) `1)),(- 1),(2 / ((h . (B1 . A2)) `1)),0) 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)))
j is non empty V16() V19( the carrier of (TOP-REAL 2)) V20( the carrier of (TOP-REAL 2)) Function-like one-to-one V26( the carrier of (TOP-REAL 2)) quasi_total onto bijective continuous being_homeomorphism Element of K6(K7( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)))
j .: (h .: (B1 .: S)) is Element of K6( the carrier of (TOP-REAL 2))
j . (h . (B1 . A1)) is V40(2) V98() V141() Element of the carrier of (TOP-REAL 2)
j . (h . (B1 . A2)) is V40(2) V98() V141() Element of the carrier of (TOP-REAL 2)
(2 / ((h . (B1 . A2)) `1)) * ((h . (B1 . A2)) `1) is complex real ext-real Element of REAL
((2 / ((h . (B1 . A2)) `1)) * ((h . (B1 . A2)) `1)) + (- 1) is complex real ext-real Element of REAL
(2 / ((h . (B1 . A2)) `1)) * ((h . (B1 . A2)) `2) is complex real ext-real Element of REAL
((2 / ((h . (B1 . A2)) `1)) * ((h . (B1 . A2)) `2)) + 0 is complex real ext-real Element of REAL
|[(((2 / ((h . (B1 . A2)) `1)) * ((h . (B1 . A2)) `1)) + (- 1)),(((2 / ((h . (B1 . A2)) `1)) * ((h . (B1 . A2)) `2)) + 0)]| is V40(2) V98() V141() Element of the carrier of (TOP-REAL 2)
2 + (- 1) is complex real ext-real integer Element of REAL
|[(2 + (- 1)),(((2 / ((h . (B1 . A2)) `1)) * ((h . (B1 . A2)) `2)) + 0)]| is V40(2) V98() V141() Element of the carrier of (TOP-REAL 2)
h * B1 is non empty V16() V19( the carrier of (TOP-REAL 2)) V20( the carrier of (TOP-REAL 2)) Function-like one-to-one V26( the carrier of (TOP-REAL 2)) quasi_total onto bijective Element of K6(K7( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)))
j * (h * B1) is non empty V16() V19( the carrier of (TOP-REAL 2)) V20( the carrier of (TOP-REAL 2)) Function-like one-to-one V26( the carrier of (TOP-REAL 2)) quasi_total onto bijective Element of K6(K7( the carrier of (TOP-REAL 2), 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 one-to-one V26( the carrier of (TOP-REAL 2)) quasi_total onto bijective continuous being_homeomorphism Homeomorphism of TOP-REAL 2
f .: S is Element of K6( the carrier of (TOP-REAL 2))
(h * B1) .: S is Element of K6( the carrier of (TOP-REAL 2))
(h . (B1 . A1)) `1 is complex real ext-real Element of REAL
(2 / ((h . (B1 . A2)) `1)) * ((h . (B1 . A1)) `1) is complex real ext-real Element of REAL
((2 / ((h . (B1 . A2)) `1)) * ((h . (B1 . A1)) `1)) + (- 1) is complex real ext-real Element of REAL
(h . (B1 . A1)) `2 is complex real ext-real Element of REAL
(2 / ((h . (B1 . A2)) `1)) * ((h . (B1 . A1)) `2) is complex real ext-real Element of REAL
((2 / ((h . (B1 . A2)) `1)) * ((h . (B1 . A1)) `2)) + 0 is complex real ext-real Element of REAL
|[(((2 / ((h . (B1 . A2)) `1)) * ((h . (B1 . A1)) `1)) + (- 1)),(((2 / ((h . (B1 . A2)) `1)) * ((h . (B1 . A1)) `2)) + 0)]| is V40(2) V98() V141() Element of the carrier of (TOP-REAL 2)
(2 / ((h . (B1 . A2)) `1)) * 0 is complex real ext-real Element of REAL
((2 / ((h . (B1 . A2)) `1)) * 0) + (- 1) is complex real ext-real Element of REAL
|[(((2 / ((h . (B1 . A2)) `1)) * 0) + (- 1)),(((2 / ((h . (B1 . A2)) `1)) * ((h . (B1 . A1)) `2)) + 0)]| is V40(2) V98() V141() Element of the carrier of (TOP-REAL 2)
S is TopStruct
the carrier of S is set
f is TopStruct
the carrier of f is set
K7( the carrier of S, the carrier of f) is V16() set
K6(K7( the carrier of S, the carrier of f)) is set
S is non empty TopSpace-like TopStruct
the carrier of S is non empty set
f is non empty TopSpace-like TopStruct
the carrier of f is non empty set
K7( the carrier of S, the carrier of f) is V16() set
K6(K7( the carrier of S, the carrier of f)) is set
s is non empty V16() V19( the carrier of S) V20( the carrier of f) Function-like V26( the carrier of S) quasi_total continuous Element of K6(K7( the carrier of S, the carrier of f))
K6( the carrier of S) is set
s is Element of K6( the carrier of S)
s .: s is Element of K6( the carrier of f)
K6( the carrier of f) is set
K6( the carrier of S) is set
[#] S is non empty non proper closed Element of K6( the carrier of S)
[#] f is non empty non proper closed Element of K6( the carrier of f)
K6( the carrier of f) is set
dom s is non empty Element of K6( the carrier of S)
s is Element of K6( the carrier of S)
s .: s is Element of K6( the carrier of f)
s " (s .: s) is Element of K6( the carrier of S)
rng s is non empty Element of K6( the carrier of f)
S is set
K6(S) is set
f is Element of K6(S)
f ` is Element of K6(S)
S \ f is set
(f `) ` is Element of K6(S)
S \ (f `) is set
S is non empty TopSpace-like TopStruct
the carrier of S is non empty set
f is non empty TopSpace-like TopStruct
the carrier of f is non empty set
K7( the carrier of S, the carrier of f) is V16() set
K6(K7( the carrier of S, the carrier of f)) is set
K6( the carrier of S) is set
s is non empty V16() V19( the carrier of S) V20( the carrier of f) Function-like V26( the carrier of S) quasi_total Element of K6(K7( the carrier of S, the carrier of f))
s is Element of K6( the carrier of S)
s .: s is Element of K6( the carrier of f)
K6( the carrier of f) is set
S is non empty TopSpace-like TopStruct
the carrier of S is non empty set
f is non empty TopSpace-like TopStruct
the carrier of f is non empty set
K7( the carrier of S, the carrier of f) is V16() set
K6(K7( the carrier of S, the carrier of f)) is set
K6( the carrier of S) is set
s is non empty V16() V19( the carrier of S) V20( the carrier of f) Function-like V26( the carrier of S) quasi_total Element of K6(K7( the carrier of S, the carrier of f))
s is Element of K6( the carrier of S)
s .: s is Element of K6( the carrier of f)
K6( the carrier of f) is set
A1 is Element of K6( the carrier of f)
[#] f is non empty non proper closed Element of K6( the carrier of f)
rng s is non empty Element of K6( the carrier of f)
s " A1 is Element of K6( the carrier of S)
s .: (s " A1) is Element of K6( the carrier of f)
dom s is non empty Element of K6( the carrier of S)
s " (s .: s) is Element of K6( the carrier of S)
S is non empty TopSpace-like TopStruct
the carrier of S is non empty set
f is non empty TopSpace-like TopStruct
the carrier of f is non empty set
K7( the carrier of S, the carrier of f) is V16() set
K6(K7( the carrier of S, the carrier of f)) is set
K6( the carrier of S) is set
s is non empty V16() V19( the carrier of S) V20( the carrier of f) Function-like V26( the carrier of S) quasi_total Element of K6(K7( the carrier of S, the carrier of f))
s is Element of K6( the carrier of S)
s | s is V16() V19( the carrier of S) V19(s) V19( the carrier of S) V20( the carrier of f) Function-like Element of K6(K7( the carrier of S, the carrier of f))
S | s is strict TopSpace-like SubSpace of S
the carrier of (S | s) is set
s .: s is Element of K6( the carrier of f)
K6( the carrier of f) is set
f | (s .: s) is strict TopSpace-like SubSpace of f
the carrier of (f | (s .: s)) is set
K7( the carrier of (S | s), the carrier of (f | (s .: s))) is V16() set
K6(K7( the carrier of (S | s), the carrier of (f | (s .: s)))) is set
rng (s | s) is Element of K6( the carrier of f)
dom s is non empty Element of K6( the carrier of S)
dom (s | s) is Element of K6(s)
K6(s) is set
[#] (S | s) is non proper closed Element of K6( the carrier of (S | s))
K6( the carrier of (S | s)) is set
[#] (f | (s .: s)) is non proper closed Element of K6( the carrier of (f | (s .: s)))
K6( the carrier of (f | (s .: s))) is set
S is non empty TopSpace-like TopStruct
the carrier of S is non empty set
f is non empty TopSpace-like TopStruct
the carrier of f is non empty set
K7( the carrier of S, the carrier of f) is V16() set
K6(K7( the carrier of S, the carrier of f)) is set
K6( the carrier of S) is set
s is non empty V16() V19( the carrier of S) V20( the carrier of f) Function-like V26( the carrier of S) quasi_total Element of K6(K7( the carrier of S, the carrier of f))
s is Element of K6( the carrier of S)
S | s is strict TopSpace-like SubSpace of S
the carrier of (S | s) is set
s .: s is Element of K6( the carrier of f)
K6( the carrier of f) is set
f | (s .: s) is strict TopSpace-like SubSpace of f
the carrier of (f | (s .: s)) is set
K7( the carrier of (S | s), the carrier of (f | (s .: s))) is V16() set
K6(K7( the carrier of (S | s), the carrier of (f | (s .: s)))) is set
s | s is V16() V19( the carrier of S) V19(s) V19( the carrier of S) V20( the carrier of f) Function-like Element of K6(K7( the carrier of S, the carrier of f))
A1 is V16() V19( the carrier of (S | s)) V20( the carrier of (f | (s .: s))) Function-like quasi_total Element of K6(K7( the carrier of (S | s), the carrier of (f | (s .: s))))
dom s is non empty Element of K6( the carrier of S)
[#] (S | s) is non proper closed Element of K6( the carrier of (S | s))
K6( the carrier of (S | s)) is set
s | (S | s) is V16() V19( the carrier of (S | s)) V20( the carrier of f) Function-like V26( the carrier of (S | s)) quasi_total Element of K6(K7( the carrier of (S | s), the carrier of f))
K7( the carrier of (S | s), the carrier of f) is V16() set
K6(K7( the carrier of (S | s), the carrier of f)) is set
A2 is non empty TopSpace-like TopStruct
the carrier of A2 is non empty set
K7( the carrier of A2, the carrier of f) is V16() set
K6(K7( the carrier of A2, the carrier of f)) is set
B1 is non empty TopSpace-like TopStruct
the carrier of B1 is non empty set
K7( the carrier of A2, the carrier of B1) is V16() set
K6(K7( the carrier of A2, the carrier of B1)) is set
S is non empty TopSpace-like TopStruct
the carrier of S is non empty set
f is non empty TopSpace-like TopStruct
the carrier of f is non empty set
K7( the carrier of S, the carrier of f) is V16() set
K6(K7( the carrier of S, the carrier of f)) is set
K6( the carrier of S) is set
s is non empty V16() V19( the carrier of S) V20( the carrier of f) Function-like V26( the carrier of S) quasi_total Element of K6(K7( the carrier of S, the carrier of f))
dom s is non empty Element of K6( the carrier of S)
[#] S is non empty non proper closed Element of K6( the carrier of S)
rng s is non empty Element of K6( the carrier of f)
K6( the carrier of f) is set
[#] f is non empty non proper closed Element of K6( the carrier of f)
s " is non empty V16() V19( the carrier of f) V20( the carrier of S) Function-like V26( the carrier of f) quasi_total Element of K6(K7( the carrier of f, the carrier of S))
K7( the carrier of f, the carrier of S) is V16() set
K6(K7( the carrier of f, the carrier of S)) is set
s is Element of K6( the carrier of S)
S | s is strict TopSpace-like SubSpace of S
the carrier of (S | s) is set
s .: s is Element of K6( the carrier of f)
f | (s .: s) is strict TopSpace-like SubSpace of f
the carrier of (f | (s .: s)) is set
K7( the carrier of (S | s), the carrier of (f | (s .: s))) is V16() set
K6(K7( the carrier of (S | s), the carrier of (f | (s .: s)))) is set
s | s is V16() V19( the carrier of S) V19(s) V19( the carrier of S) V20( the carrier of f) Function-like Element of K6(K7( the carrier of S, the carrier of f))
s " is V16() Function-like set
(s ") .: (s .: s) is Element of K6( the carrier of S)
s " (s .: s) is Element of K6( the carrier of S)
A1 is V16() V19( the carrier of (S | s)) V20( the carrier of (f | (s .: s))) Function-like quasi_total Element of K6(K7( the carrier of (S | s), the carrier of (f | (s .: s))))
[#] (S | s) is non proper closed Element of K6( the carrier of (S | s))
K6( the carrier of (S | s)) is set
[#] (f | (s .: s)) is non proper closed Element of K6( the carrier of (f | (s .: s)))
K6( the carrier of (f | (s .: s))) is set
dom A1 is Element of K6( the carrier of (S | s))
rng A1 is Element of K6( the carrier of (f | (s .: s)))
A1 " is V16() V19( the carrier of (f | (s .: s))) V20( the carrier of (S | s)) Function-like quasi_total Element of K6(K7( the carrier of (f | (s .: s)), the carrier of (S | s)))
K7( the carrier of (f | (s .: s)), the carrier of (S | s)) is V16() set
K6(K7( the carrier of (f | (s .: s)), the carrier of (S | s))) is set
A1 " is V16() Function-like set
(s ") | (s .: s) is V16() V19( the carrier of f) V19(s .: s) V19( the carrier of f) V20( the carrier of S) Function-like Element of K6(K7( the carrier of f, the carrier of S))
S is non empty TopSpace-like TopStruct
the carrier of S is non empty set
f is non empty TopSpace-like TopStruct
the carrier of f is non empty set
K7( the carrier of S, the carrier of f) is V16() set
K6(K7( the carrier of S, the carrier of f)) is set
K6( the carrier of S) is set
s is non empty V16() V19( the carrier of S) V20( the carrier of f) Function-like V26( the carrier of S) quasi_total Element of K6(K7( the carrier of S, the carrier of f))
A1 is Element of K6( the carrier of S)
s is Element of K6( the carrier of S)
s .: A1 is Element of K6( the carrier of f)
K6( the carrier of f) is set
s .: s is Element of K6( the carrier of f)
S | A1 is strict TopSpace-like SubSpace of S
the carrier of (S | A1) is set
K6( the carrier of (S | A1)) is set
A2 is Element of K6( the carrier of (S | A1))
f | (s .: A1) is strict TopSpace-like SubSpace of f
[#] (f | (s .: A1)) is non proper closed Element of K6( the carrier of (f | (s .: A1)))
the carrier of (f | (s .: A1)) is set
K6( the carrier of (f | (s .: A1))) is set
dom s is non empty Element of K6( the carrier of S)
[#] (S | A1) is non proper closed Element of K6( the carrier of (S | A1))
B1 is Element of K6( the carrier of (f | (s .: A1)))
{} f is empty V16() non-empty empty-yielding closed V149() V150() V151() V152() V153() V154() V155() Element of K6( the carrier of f)
B1 is Element of K6( the carrier of (f | (s .: A1)))
B2 is non empty TopSpace-like TopStruct
the carrier of B2 is non empty set
S2 is non empty TopSpace-like TopStruct
the carrier of S2 is non empty set
K7( the carrier of B2, the carrier of S2) is V16() set
K6(K7( the carrier of B2, the carrier of S2)) is set
s | A1 is V16() V19( the carrier of S) V19(A1) V19( the carrier of S) V20( the carrier of f) Function-like Element of K6(K7( the carrier of S, the carrier of f))
fB is non empty V16() V19( the carrier of B2) V20( the carrier of S2) Function-like V26( the carrier of B2) quasi_total Element of K6(K7( the carrier of B2, the carrier of S2))
fB .: s is Element of K6( the carrier of S2)
K6( the carrier of S2) is set
S is Element of K6( 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 one-to-one V26( the carrier of (TOP-REAL 2)) quasi_total onto bijective continuous being_homeomorphism Homeomorphism of TOP-REAL 2
f .: S is Element of K6( the carrier of (TOP-REAL 2))
S ` is Element of K6( the carrier of (TOP-REAL 2))
the carrier of (TOP-REAL 2) \ S is set
the Element of S ` is Element of S `
A1 is Element of K6( the carrier of (TOP-REAL 2))
A2 is Element of K6( the carrier of (TOP-REAL 2))
A1 \/ A2 is Element of K6( the carrier of (TOP-REAL 2))
Cl A1 is Element of K6( the carrier of (TOP-REAL 2))
(Cl A1) \ A1 is Element of K6( the carrier of (TOP-REAL 2))
Cl A2 is Element of K6( the carrier of (TOP-REAL 2))
(Cl A2) \ A2 is Element of K6( the carrier of (TOP-REAL 2))
s is V40(2) V98() V141() Element of the carrier of (TOP-REAL 2)
(f .: S) ` is Element of K6( the carrier of (TOP-REAL 2))
the carrier of (TOP-REAL 2) \ (f .: S) is set
f . s is V40(2) V98() V141() Element of the carrier of (TOP-REAL 2)
B1 is V40(2) V98() V141() Element of the carrier of (TOP-REAL 2)
f . B1 is V40(2) V98() V141() Element of the carrier of (TOP-REAL 2)
f .: A1 is Element of K6( the carrier of (TOP-REAL 2))
B1 is Element of K6( the carrier of (TOP-REAL 2))
Cl B1 is Element of K6( the carrier of (TOP-REAL 2))
(Cl B1) \ B1 is Element of K6( the carrier of (TOP-REAL 2))
f .: A2 is Element of K6( the carrier of (TOP-REAL 2))
B2 is Element of K6( the carrier of (TOP-REAL 2))
B1 \/ B2 is Element of K6( the carrier of (TOP-REAL 2))
Cl B2 is Element of K6( the carrier of (TOP-REAL 2))
(Cl B2) \ B2 is Element of K6( the carrier of (TOP-REAL 2))
f .: (A1 \/ A2) is Element of K6( the carrier of (TOP-REAL 2))
f .: (Cl A1) is Element of K6( the carrier of (TOP-REAL 2))
(f .: (Cl A1)) \ B1 is Element of K6( the carrier of (TOP-REAL 2))
f .: ((Cl A2) \ A2) is Element of K6( the carrier of (TOP-REAL 2))
f .: (Cl A2) is Element of K6( the carrier of (TOP-REAL 2))
(f .: (Cl A2)) \ B2 is Element of K6( the carrier of (TOP-REAL 2))
f .: (S `) is Element of K6( the carrier of (TOP-REAL 2))