:: SEQ_2 semantic presentation

REAL is non zero V45() V46() V47() V51() V52() set
NAT is non zero epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() Element of K11(REAL)
K11(REAL) is set
COMPLEX is non zero V45() V51() V52() set
RAT is non zero V45() V46() V47() V48() V51() V52() set
INT is non zero V45() V46() V47() V48() V49() V51() V52() set
0 is ext-real non positive non negative zero epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real V45() V46() V47() V48() V49() V50() V51() set
K12(NAT,REAL) is complex-valued ext-real-valued real-valued set
K11(K12(NAT,REAL)) is set
0 is ext-real non positive non negative zero epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real V33() V34() V45() V46() V47() V48() V49() V50() V51() Element of NAT
1 is ext-real positive non negative non zero epsilon-transitive epsilon-connected ordinal natural complex real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
2 is ext-real positive non negative non zero epsilon-transitive epsilon-connected ordinal natural complex real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
K12(2,REAL) is complex-valued ext-real-valued real-valued set
K11(K12(2,REAL)) is set
<i> is complex Element of COMPLEX
|.0.| is ext-real complex real V34() Element of REAL
Re 0 is ext-real complex real Element of REAL
(Re 0) ^2 is ext-real complex real Element of REAL
(Re 0) * (Re 0) is ext-real complex real set
Im 0 is ext-real complex real Element of REAL
(Im 0) ^2 is ext-real complex real Element of REAL
(Im 0) * (Im 0) is ext-real complex real set
((Re 0) ^2) + ((Im 0) ^2) is ext-real complex real Element of REAL
sqrt (((Re 0) ^2) + ((Im 0) ^2)) is ext-real complex real Element of REAL
K12(NAT,COMPLEX) is complex-valued set
K11(K12(NAT,COMPLEX)) is set
0c is ext-real non positive non negative zero epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real V45() V46() V47() V48() V49() V50() V51() Element of COMPLEX
s is ext-real complex real set
- s is ext-real complex real set
s1 is ext-real complex real set
abs s1 is ext-real complex real Element of REAL
Re s1 is ext-real complex real Element of REAL
(Re s1) ^2 is ext-real complex real Element of REAL
(Re s1) * (Re s1) is ext-real complex real set
Im s1 is ext-real complex real Element of REAL
(Im s1) ^2 is ext-real complex real Element of REAL
(Im s1) * (Im s1) is ext-real complex real set
((Re s1) ^2) + ((Im s1) ^2) is ext-real complex real Element of REAL
sqrt (((Re s1) ^2) + ((Im s1) ^2)) is ext-real complex real Element of REAL
- s1 is ext-real complex real set
- 0 is ext-real non positive non negative zero epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real V45() V46() V47() V48() V49() V50() V51() Element of REAL
- (- s) is ext-real complex real set
s is ext-real complex real set
s " is ext-real complex real set
abs s is ext-real complex real Element of REAL
Re s is ext-real complex real Element of REAL
(Re s) ^2 is ext-real complex real Element of REAL
(Re s) * (Re s) is ext-real complex real set
Im s is ext-real complex real Element of REAL
(Im s) ^2 is ext-real complex real Element of REAL
(Im s) * (Im s) is ext-real complex real set
((Re s) ^2) + ((Im s) ^2) is ext-real complex real Element of REAL
sqrt (((Re s) ^2) + ((Im s) ^2)) is ext-real complex real Element of REAL
s1 is ext-real complex real set
s1 " is ext-real complex real set
(s ") - (s1 ") is ext-real complex real set
abs ((s ") - (s1 ")) is ext-real complex real Element of REAL
Re ((s ") - (s1 ")) is ext-real complex real Element of REAL
(Re ((s ") - (s1 "))) ^2 is ext-real complex real Element of REAL
(Re ((s ") - (s1 "))) * (Re ((s ") - (s1 "))) is ext-real complex real set
Im ((s ") - (s1 ")) is ext-real complex real Element of REAL
(Im ((s ") - (s1 "))) ^2 is ext-real complex real Element of REAL
(Im ((s ") - (s1 "))) * (Im ((s ") - (s1 "))) is ext-real complex real set
((Re ((s ") - (s1 "))) ^2) + ((Im ((s ") - (s1 "))) ^2) is ext-real complex real Element of REAL
sqrt (((Re ((s ") - (s1 "))) ^2) + ((Im ((s ") - (s1 "))) ^2)) is ext-real complex real Element of REAL
s - s1 is ext-real complex real set
abs (s - s1) is ext-real complex real Element of REAL
Re (s - s1) is ext-real complex real Element of REAL
(Re (s - s1)) ^2 is ext-real complex real Element of REAL
(Re (s - s1)) * (Re (s - s1)) is ext-real complex real set
Im (s - s1) is ext-real complex real Element of REAL
(Im (s - s1)) ^2 is ext-real complex real Element of REAL
(Im (s - s1)) * (Im (s - s1)) is ext-real complex real set
((Re (s - s1)) ^2) + ((Im (s - s1)) ^2) is ext-real complex real Element of REAL
sqrt (((Re (s - s1)) ^2) + ((Im (s - s1)) ^2)) is ext-real complex real Element of REAL
abs s1 is ext-real complex real Element of REAL
Re s1 is ext-real complex real Element of REAL
(Re s1) ^2 is ext-real complex real Element of REAL
(Re s1) * (Re s1) is ext-real complex real set
Im s1 is ext-real complex real Element of REAL
(Im s1) ^2 is ext-real complex real Element of REAL
(Im s1) * (Im s1) is ext-real complex real set
((Re s1) ^2) + ((Im s1) ^2) is ext-real complex real Element of REAL
sqrt (((Re s1) ^2) + ((Im s1) ^2)) is ext-real complex real Element of REAL
(abs s) * (abs s1) is ext-real complex real Element of REAL
(abs (s - s1)) / ((abs s) * (abs s1)) is ext-real complex real Element of REAL
1 / s is ext-real complex real Element of REAL
(1 / s) - (s1 ") is ext-real complex real Element of REAL
abs ((1 / s) - (s1 ")) is ext-real complex real Element of REAL
Re ((1 / s) - (s1 ")) is ext-real complex real Element of REAL
(Re ((1 / s) - (s1 "))) ^2 is ext-real complex real Element of REAL
(Re ((1 / s) - (s1 "))) * (Re ((1 / s) - (s1 "))) is ext-real complex real set
Im ((1 / s) - (s1 ")) is ext-real complex real Element of REAL
(Im ((1 / s) - (s1 "))) ^2 is ext-real complex real Element of REAL
(Im ((1 / s) - (s1 "))) * (Im ((1 / s) - (s1 "))) is ext-real complex real set
((Re ((1 / s) - (s1 "))) ^2) + ((Im ((1 / s) - (s1 "))) ^2) is ext-real complex real Element of REAL
sqrt (((Re ((1 / s) - (s1 "))) ^2) + ((Im ((1 / s) - (s1 "))) ^2)) is ext-real complex real Element of REAL
1 / s1 is ext-real complex real Element of REAL
(1 / s) - (1 / s1) is ext-real complex real Element of REAL
abs ((1 / s) - (1 / s1)) is ext-real complex real Element of REAL
Re ((1 / s) - (1 / s1)) is ext-real complex real Element of REAL
(Re ((1 / s) - (1 / s1))) ^2 is ext-real complex real Element of REAL
(Re ((1 / s) - (1 / s1))) * (Re ((1 / s) - (1 / s1))) is ext-real complex real set
Im ((1 / s) - (1 / s1)) is ext-real complex real Element of REAL
(Im ((1 / s) - (1 / s1))) ^2 is ext-real complex real Element of REAL
(Im ((1 / s) - (1 / s1))) * (Im ((1 / s) - (1 / s1))) is ext-real complex real set
((Re ((1 / s) - (1 / s1))) ^2) + ((Im ((1 / s) - (1 / s1))) ^2) is ext-real complex real Element of REAL
sqrt (((Re ((1 / s) - (1 / s1))) ^2) + ((Im ((1 / s) - (1 / s1))) ^2)) is ext-real complex real Element of REAL
1 * s1 is ext-real complex real Element of REAL
1 * s is ext-real complex real Element of REAL
(1 * s1) - (1 * s) is ext-real complex real Element of REAL
s * s1 is ext-real complex real set
((1 * s1) - (1 * s)) / (s * s1) is ext-real complex real Element of REAL
abs (((1 * s1) - (1 * s)) / (s * s1)) is ext-real complex real Element of REAL
Re (((1 * s1) - (1 * s)) / (s * s1)) is ext-real complex real Element of REAL
(Re (((1 * s1) - (1 * s)) / (s * s1))) ^2 is ext-real complex real Element of REAL
(Re (((1 * s1) - (1 * s)) / (s * s1))) * (Re (((1 * s1) - (1 * s)) / (s * s1))) is ext-real complex real set
Im (((1 * s1) - (1 * s)) / (s * s1)) is ext-real complex real Element of REAL
(Im (((1 * s1) - (1 * s)) / (s * s1))) ^2 is ext-real complex real Element of REAL
(Im (((1 * s1) - (1 * s)) / (s * s1))) * (Im (((1 * s1) - (1 * s)) / (s * s1))) is ext-real complex real set
((Re (((1 * s1) - (1 * s)) / (s * s1))) ^2) + ((Im (((1 * s1) - (1 * s)) / (s * s1))) ^2) is ext-real complex real Element of REAL
sqrt (((Re (((1 * s1) - (1 * s)) / (s * s1))) ^2) + ((Im (((1 * s1) - (1 * s)) / (s * s1))) ^2)) is ext-real complex real Element of REAL
s1 - s is ext-real complex real set
abs (s1 - s) is ext-real complex real Element of REAL
Re (s1 - s) is ext-real complex real Element of REAL
(Re (s1 - s)) ^2 is ext-real complex real Element of REAL
(Re (s1 - s)) * (Re (s1 - s)) is ext-real complex real set
Im (s1 - s) is ext-real complex real Element of REAL
(Im (s1 - s)) ^2 is ext-real complex real Element of REAL
(Im (s1 - s)) * (Im (s1 - s)) is ext-real complex real set
((Re (s1 - s)) ^2) + ((Im (s1 - s)) ^2) is ext-real complex real Element of REAL
sqrt (((Re (s1 - s)) ^2) + ((Im (s1 - s)) ^2)) is ext-real complex real Element of REAL
abs (s * s1) is ext-real complex real Element of REAL
Re (s * s1) is ext-real complex real Element of REAL
(Re (s * s1)) ^2 is ext-real complex real Element of REAL
(Re (s * s1)) * (Re (s * s1)) is ext-real complex real set
Im (s * s1) is ext-real complex real Element of REAL
(Im (s * s1)) ^2 is ext-real complex real Element of REAL
(Im (s * s1)) * (Im (s * s1)) is ext-real complex real set
((Re (s * s1)) ^2) + ((Im (s * s1)) ^2) is ext-real complex real Element of REAL
sqrt (((Re (s * s1)) ^2) + ((Im (s * s1)) ^2)) is ext-real complex real Element of REAL
(abs (s1 - s)) / (abs (s * s1)) is ext-real complex real Element of REAL
- (s - s1) is ext-real complex real set
abs (- (s - s1)) is ext-real complex real Element of REAL
Re (- (s - s1)) is ext-real complex real Element of REAL
(Re (- (s - s1))) ^2 is ext-real complex real Element of REAL
(Re (- (s - s1))) * (Re (- (s - s1))) is ext-real complex real set
Im (- (s - s1)) is ext-real complex real Element of REAL
(Im (- (s - s1))) ^2 is ext-real complex real Element of REAL
(Im (- (s - s1))) * (Im (- (s - s1))) is ext-real complex real set
((Re (- (s - s1))) ^2) + ((Im (- (s - s1))) ^2) is ext-real complex real Element of REAL
sqrt (((Re (- (s - s1))) ^2) + ((Im (- (s - s1))) ^2)) is ext-real complex real Element of REAL
(abs (- (s - s1))) / ((abs s) * (abs s1)) is ext-real complex real Element of REAL
s is non zero Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K11(K12(NAT,REAL))
dom s is V45() V46() V47() V48() V49() V50() set
s1 is ext-real complex real set
s1 is ext-real epsilon-transitive epsilon-connected ordinal natural complex real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
s . s1 is ext-real complex real Element of REAL
s1 is ext-real complex real set
s1 is set
s . s1 is ext-real complex real Element of REAL
s1 is ext-real complex real set
s1 is ext-real epsilon-transitive epsilon-connected ordinal natural complex real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
s . s1 is ext-real complex real Element of REAL
s1 is ext-real complex real set
s1 is set
s . s1 is ext-real complex real Element of REAL
s is Relation-like Function-like complex-valued ext-real-valued real-valued set
dom s is set
s1 is ext-real complex real set
s1 is set
s . s1 is ext-real complex real Element of REAL
abs (s . s1) is ext-real complex real Element of REAL
Re (s . s1) is ext-real complex real Element of REAL
(Re (s . s1)) ^2 is ext-real complex real Element of REAL
(Re (s . s1)) * (Re (s . s1)) is ext-real complex real set
Im (s . s1) is ext-real complex real Element of REAL
(Im (s . s1)) ^2 is ext-real complex real Element of REAL
(Im (s . s1)) * (Im (s . s1)) is ext-real complex real set
((Re (s . s1)) ^2) + ((Im (s . s1)) ^2) is ext-real complex real Element of REAL
sqrt (((Re (s . s1)) ^2) + ((Im (s . s1)) ^2)) is ext-real complex real Element of REAL
abs s1 is ext-real complex real Element of REAL
Re s1 is ext-real complex real Element of REAL
(Re s1) ^2 is ext-real complex real Element of REAL
(Re s1) * (Re s1) is ext-real complex real set
Im s1 is ext-real complex real Element of REAL
(Im s1) ^2 is ext-real complex real Element of REAL
(Im s1) * (Im s1) is ext-real complex real set
((Re s1) ^2) + ((Im s1) ^2) is ext-real complex real Element of REAL
sqrt (((Re s1) ^2) + ((Im s1) ^2)) is ext-real complex real Element of REAL
- (abs s1) is ext-real complex real Element of REAL
s1 is set
s . s1 is ext-real complex real Element of REAL
abs (s . s1) is ext-real complex real Element of REAL
Re (s . s1) is ext-real complex real Element of REAL
(Re (s . s1)) ^2 is ext-real complex real Element of REAL
(Re (s . s1)) * (Re (s . s1)) is ext-real complex real set
Im (s . s1) is ext-real complex real Element of REAL
(Im (s . s1)) ^2 is ext-real complex real Element of REAL
(Im (s . s1)) * (Im (s . s1)) is ext-real complex real set
((Re (s . s1)) ^2) + ((Im (s . s1)) ^2) is ext-real complex real Element of REAL
sqrt (((Re (s . s1)) ^2) + ((Im (s . s1)) ^2)) is ext-real complex real Element of REAL
- (abs (s . s1)) is ext-real complex real Element of REAL
- s1 is ext-real complex real set
s is Relation-like Function-like complex-valued ext-real-valued real-valued set
dom s is set
s1 is ext-real complex real set
s1 is ext-real complex real set
abs s1 is ext-real complex real Element of REAL
Re s1 is ext-real complex real Element of REAL
(Re s1) ^2 is ext-real complex real Element of REAL
(Re s1) * (Re s1) is ext-real complex real set
Im s1 is ext-real complex real Element of REAL
(Im s1) ^2 is ext-real complex real Element of REAL
(Im s1) * (Im s1) is ext-real complex real set
((Re s1) ^2) + ((Im s1) ^2) is ext-real complex real Element of REAL
sqrt (((Re s1) ^2) + ((Im s1) ^2)) is ext-real complex real Element of REAL
abs s1 is ext-real complex real Element of REAL
Re s1 is ext-real complex real Element of REAL
(Re s1) ^2 is ext-real complex real Element of REAL
(Re s1) * (Re s1) is ext-real complex real set
Im s1 is ext-real complex real Element of REAL
(Im s1) ^2 is ext-real complex real Element of REAL
(Im s1) * (Im s1) is ext-real complex real set
((Re s1) ^2) + ((Im s1) ^2) is ext-real complex real Element of REAL
sqrt (((Re s1) ^2) + ((Im s1) ^2)) is ext-real complex real Element of REAL
(abs s1) + (abs s1) is ext-real complex real Element of REAL
((abs s1) + (abs s1)) + 1 is ext-real complex real Element of REAL
w is ext-real complex real Element of REAL
w is set
s . w is ext-real complex real set
abs (s . w) is ext-real complex real Element of REAL
Re (s . w) is ext-real complex real Element of REAL
(Re (s . w)) ^2 is ext-real complex real Element of REAL
(Re (s . w)) * (Re (s . w)) is ext-real complex real set
Im (s . w) is ext-real complex real Element of REAL
(Im (s . w)) ^2 is ext-real complex real Element of REAL
(Im (s . w)) * (Im (s . w)) is ext-real complex real set
((Re (s . w)) ^2) + ((Im (s . w)) ^2) is ext-real complex real Element of REAL
sqrt (((Re (s . w)) ^2) + ((Im (s . w)) ^2)) is ext-real complex real Element of REAL
s . w is ext-real complex real Element of REAL
(s . w) + 0 is ext-real complex real Element of REAL
- (abs s1) is ext-real complex real Element of REAL
0 + (s . w) is ext-real complex real Element of REAL
- (abs s1) is ext-real complex real Element of REAL
(- (abs s1)) + (- (abs s1)) is ext-real complex real Element of REAL
(- (abs s1)) - (abs s1) is ext-real complex real Element of REAL
- 1 is ext-real non positive negative non zero complex real Element of REAL
((- (abs s1)) - (abs s1)) + (- 1) is ext-real complex real Element of REAL
((- (abs s1)) - (abs s1)) - 1 is ext-real complex real Element of REAL
- w is ext-real complex real Element of REAL
abs (s . w) is ext-real complex real Element of REAL
Re (s . w) is ext-real complex real Element of REAL
(Re (s . w)) ^2 is ext-real complex real Element of REAL
(Re (s . w)) * (Re (s . w)) is ext-real complex real set
Im (s . w) is ext-real complex real Element of REAL
(Im (s . w)) ^2 is ext-real complex real Element of REAL
(Im (s . w)) * (Im (s . w)) is ext-real complex real set
((Re (s . w)) ^2) + ((Im (s . w)) ^2) is ext-real complex real Element of REAL
sqrt (((Re (s . w)) ^2) + ((Im (s . w)) ^2)) is ext-real complex real Element of REAL
s is non zero Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K11(K12(NAT,REAL))
s1 is ext-real complex real set
s1 is ext-real complex real set
abs s1 is ext-real complex real Element of REAL
Re s1 is ext-real complex real Element of REAL
(Re s1) ^2 is ext-real complex real Element of REAL
(Re s1) * (Re s1) is ext-real complex real set
Im s1 is ext-real complex real Element of REAL
(Im s1) ^2 is ext-real complex real Element of REAL
(Im s1) * (Im s1) is ext-real complex real set
((Re s1) ^2) + ((Im s1) ^2) is ext-real complex real Element of REAL
sqrt (((Re s1) ^2) + ((Im s1) ^2)) is ext-real complex real Element of REAL
abs s1 is ext-real complex real Element of REAL
Re s1 is ext-real complex real Element of REAL
(Re s1) ^2 is ext-real complex real Element of REAL
(Re s1) * (Re s1) is ext-real complex real set
Im s1 is ext-real complex real Element of REAL
(Im s1) ^2 is ext-real complex real Element of REAL
(Im s1) * (Im s1) is ext-real complex real set
((Re s1) ^2) + ((Im s1) ^2) is ext-real complex real Element of REAL
sqrt (((Re s1) ^2) + ((Im s1) ^2)) is ext-real complex real Element of REAL
(abs s1) + (abs s1) is ext-real complex real Element of REAL
((abs s1) + (abs s1)) + 1 is ext-real complex real Element of REAL
w is ext-real complex real Element of REAL
w is ext-real epsilon-transitive epsilon-connected ordinal natural complex real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
s . w is ext-real complex real Element of REAL
abs (s . w) is ext-real complex real Element of REAL
Re (s . w) is ext-real complex real Element of REAL
(Re (s . w)) ^2 is ext-real complex real Element of REAL
(Re (s . w)) * (Re (s . w)) is ext-real complex real set
Im (s . w) is ext-real complex real Element of REAL
(Im (s . w)) ^2 is ext-real complex real Element of REAL
(Im (s . w)) * (Im (s . w)) is ext-real complex real set
((Re (s . w)) ^2) + ((Im (s . w)) ^2) is ext-real complex real Element of REAL
sqrt (((Re (s . w)) ^2) + ((Im (s . w)) ^2)) is ext-real complex real Element of REAL
(s . w) + 0 is ext-real complex real Element of REAL
- (abs s1) is ext-real complex real Element of REAL
0 + (s . w) is ext-real complex real Element of REAL
- (abs s1) is ext-real complex real Element of REAL
(- (abs s1)) + (- (abs s1)) is ext-real complex real Element of REAL
(- (abs s1)) - (abs s1) is ext-real complex real Element of REAL
- 1 is ext-real non positive negative non zero complex real Element of REAL
((- (abs s1)) - (abs s1)) + (- 1) is ext-real complex real Element of REAL
((- (abs s1)) - (abs s1)) - 1 is ext-real complex real Element of REAL
- w is ext-real complex real Element of REAL
s1 is ext-real complex real set
dom s is V45() V46() V47() V48() V49() V50() set
s1 is set
s . s1 is ext-real complex real set
abs (s . s1) is ext-real complex real Element of REAL
Re (s . s1) is ext-real complex real Element of REAL
(Re (s . s1)) ^2 is ext-real complex real Element of REAL
(Re (s . s1)) * (Re (s . s1)) is ext-real complex real set
Im (s . s1) is ext-real complex real Element of REAL
(Im (s . s1)) ^2 is ext-real complex real Element of REAL
(Im (s . s1)) * (Im (s . s1)) is ext-real complex real set
((Re (s . s1)) ^2) + ((Im (s . s1)) ^2) is ext-real complex real Element of REAL
sqrt (((Re (s . s1)) ^2) + ((Im (s . s1)) ^2)) is ext-real complex real Element of REAL
s is non zero Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K11(K12(NAT,REAL))
s . 0 is ext-real complex real Element of REAL
abs (s . 0) is ext-real complex real Element of REAL
Re (s . 0) is ext-real complex real Element of REAL
(Re (s . 0)) ^2 is ext-real complex real Element of REAL
(Re (s . 0)) * (Re (s . 0)) is ext-real complex real set
Im (s . 0) is ext-real complex real Element of REAL
(Im (s . 0)) ^2 is ext-real complex real Element of REAL
(Im (s . 0)) * (Im (s . 0)) is ext-real complex real set
((Re (s . 0)) ^2) + ((Im (s . 0)) ^2) is ext-real complex real Element of REAL
sqrt (((Re (s . 0)) ^2) + ((Im (s . 0)) ^2)) is ext-real complex real Element of REAL
(abs (s . 0)) + 1 is ext-real complex real Element of REAL
s1 is ext-real complex real set
0 + 0 is ext-real non positive non negative zero epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real V33() V34() V45() V46() V47() V48() V49() V50() V51() Element of NAT
s1 is ext-real epsilon-transitive epsilon-connected ordinal natural complex real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
s . s1 is ext-real complex real Element of REAL
abs (s . s1) is ext-real complex real Element of REAL
Re (s . s1) is ext-real complex real Element of REAL
(Re (s . s1)) ^2 is ext-real complex real Element of REAL
(Re (s . s1)) * (Re (s . s1)) is ext-real complex real set
Im (s . s1) is ext-real complex real Element of REAL
(Im (s . s1)) ^2 is ext-real complex real Element of REAL
(Im (s . s1)) * (Im (s . s1)) is ext-real complex real set
((Re (s . s1)) ^2) + ((Im (s . s1)) ^2) is ext-real complex real Element of REAL
sqrt (((Re (s . s1)) ^2) + ((Im (s . s1)) ^2)) is ext-real complex real Element of REAL
(abs (s . s1)) + 0 is ext-real complex real Element of REAL
s1 is ext-real epsilon-transitive epsilon-connected ordinal natural complex real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
s1 + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural complex real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
s1 is ext-real complex real set
s . (s1 + 1) is ext-real complex real Element of REAL
abs (s . (s1 + 1)) is ext-real complex real Element of REAL
Re (s . (s1 + 1)) is ext-real complex real Element of REAL
(Re (s . (s1 + 1))) ^2 is ext-real complex real Element of REAL
(Re (s . (s1 + 1))) * (Re (s . (s1 + 1))) is ext-real complex real set
Im (s . (s1 + 1)) is ext-real complex real Element of REAL
(Im (s . (s1 + 1))) ^2 is ext-real complex real Element of REAL
(Im (s . (s1 + 1))) * (Im (s . (s1 + 1))) is ext-real complex real set
((Re (s . (s1 + 1))) ^2) + ((Im (s . (s1 + 1))) ^2) is ext-real complex real Element of REAL
sqrt (((Re (s . (s1 + 1))) ^2) + ((Im (s . (s1 + 1))) ^2)) is ext-real complex real Element of REAL
s1 + 1 is ext-real complex real Element of REAL
w is ext-real complex real Element of REAL
w is ext-real epsilon-transitive epsilon-connected ordinal natural complex real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
s . w is ext-real complex real Element of REAL
abs (s . w) is ext-real complex real Element of REAL
Re (s . w) is ext-real complex real Element of REAL
(Re (s . w)) ^2 is ext-real complex real Element of REAL
(Re (s . w)) * (Re (s . w)) is ext-real complex real set
Im (s . w) is ext-real complex real Element of REAL
(Im (s . w)) ^2 is ext-real complex real Element of REAL
(Im (s . w)) * (Im (s . w)) is ext-real complex real set
((Re (s . w)) ^2) + ((Im (s . w)) ^2) is ext-real complex real Element of REAL
sqrt (((Re (s . w)) ^2) + ((Im (s . w)) ^2)) is ext-real complex real Element of REAL
s1 + 0 is ext-real complex real Element of REAL
(abs (s . (s1 + 1))) + 1 is ext-real complex real Element of REAL
w is ext-real complex real Element of REAL
0 + 0 is ext-real non positive non negative zero epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real V33() V34() V45() V46() V47() V48() V49() V50() V51() Element of NAT
w is ext-real epsilon-transitive epsilon-connected ordinal natural complex real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
s . w is ext-real complex real Element of REAL
abs (s . w) is ext-real complex real Element of REAL
Re (s . w) is ext-real complex real Element of REAL
(Re (s . w)) ^2 is ext-real complex real Element of REAL
(Re (s . w)) * (Re (s . w)) is ext-real complex real set
Im (s . w) is ext-real complex real Element of REAL
(Im (s . w)) ^2 is ext-real complex real Element of REAL
(Im (s . w)) * (Im (s . w)) is ext-real complex real set
((Re (s . w)) ^2) + ((Im (s . w)) ^2) is ext-real complex real Element of REAL
sqrt (((Re (s . w)) ^2) + ((Im (s . w)) ^2)) is ext-real complex real Element of REAL
(abs (s . w)) + 0 is ext-real complex real Element of REAL
w is ext-real complex real Element of REAL
w is ext-real complex real Element of REAL
s is non zero Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K11(K12(NAT,REAL))
s1 is complex Element of COMPLEX
Re s1 is ext-real complex real Element of REAL
Im s1 is ext-real complex real Element of REAL
(Im s1) * <i> is complex set
(Re s1) + ((Im s1) * <i>) is complex set
abs (Im s1) is ext-real complex real Element of REAL
Re (Im s1) is ext-real complex real Element of REAL
(Re (Im s1)) ^2 is ext-real complex real Element of REAL
(Re (Im s1)) * (Re (Im s1)) is ext-real complex real set
Im (Im s1) is ext-real complex real Element of REAL
(Im (Im s1)) ^2 is ext-real complex real Element of REAL
(Im (Im s1)) * (Im (Im s1)) is ext-real complex real set
((Re (Im s1)) ^2) + ((Im (Im s1)) ^2) is ext-real complex real Element of REAL
sqrt (((Re (Im s1)) ^2) + ((Im (Im s1)) ^2)) is ext-real complex real Element of REAL
w is ext-real epsilon-transitive epsilon-connected ordinal natural complex real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
s . w is ext-real complex real Element of REAL
(s . w) - s1 is complex set
|.((s . w) - s1).| is ext-real complex real Element of REAL
Re ((s . w) - s1) is ext-real complex real Element of REAL
(Re ((s . w) - s1)) ^2 is ext-real complex real Element of REAL
(Re ((s . w) - s1)) * (Re ((s . w) - s1)) is ext-real complex real set
Im ((s . w) - s1) is ext-real complex real Element of REAL
(Im ((s . w) - s1)) ^2 is ext-real complex real Element of REAL
(Im ((s . w) - s1)) * (Im ((s . w) - s1)) is ext-real complex real set
((Re ((s . w) - s1)) ^2) + ((Im ((s . w) - s1)) ^2) is ext-real complex real Element of REAL
sqrt (((Re ((s . w) - s1)) ^2) + ((Im ((s . w) - s1)) ^2)) is ext-real complex real Element of REAL
Im (s . w) is ext-real complex real Element of REAL
(Im (s . w)) - (Im s1) is ext-real complex real Element of REAL
(Im s1) ^2 is ext-real complex real Element of REAL
(Im s1) * (Im s1) is ext-real complex real set
((Re ((s . w) - s1)) ^2) + ((Im s1) ^2) is ext-real complex real Element of REAL
sqrt (((Re ((s . w) - s1)) ^2) + ((Im s1) ^2)) is ext-real complex real Element of REAL
|.(Im s1).| is ext-real complex real Element of REAL
|.(Im s1).| ^2 is ext-real complex real Element of REAL
|.(Im s1).| * |.(Im s1).| is ext-real complex real set
((Re ((s . w) - s1)) ^2) + (|.(Im s1).| ^2) is ext-real complex real Element of REAL
sqrt (((Re ((s . w) - s1)) ^2) + (|.(Im s1).| ^2)) is ext-real complex real Element of REAL
s1 is ext-real complex real set
w is ext-real complex real set
w is ext-real complex real Element of REAL
p is ext-real epsilon-transitive epsilon-connected ordinal natural complex real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
s1 is ext-real complex real set
s1 is complex Element of COMPLEX
w is ext-real complex real Element of REAL
s is non zero Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K11(K12(NAT,REAL))
s1 is ext-real complex real set
s1 is ext-real complex real set
s1 - s1 is ext-real complex real set
abs (s1 - s1) is ext-real complex real Element of REAL
Re (s1 - s1) is ext-real complex real Element of REAL
(Re (s1 - s1)) ^2 is ext-real complex real Element of REAL
(Re (s1 - s1)) * (Re (s1 - s1)) is ext-real complex real set
Im (s1 - s1) is ext-real complex real Element of REAL
(Im (s1 - s1)) ^2 is ext-real complex real Element of REAL
(Im (s1 - s1)) * (Im (s1 - s1)) is ext-real complex real set
((Re (s1 - s1)) ^2) + ((Im (s1 - s1)) ^2) is ext-real complex real Element of REAL
sqrt (((Re (s1 - s1)) ^2) + ((Im (s1 - s1)) ^2)) is ext-real complex real Element of REAL
0 + s1 is ext-real complex real Element of REAL
(s1 - s1) + s1 is ext-real complex real set
4 is ext-real positive non negative non zero epsilon-transitive epsilon-connected ordinal natural complex real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
(abs (s1 - s1)) / 4 is ext-real complex real Element of REAL
w is ext-real epsilon-transitive epsilon-connected ordinal natural complex real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
w is ext-real epsilon-transitive epsilon-connected ordinal natural complex real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
w + w is ext-real epsilon-transitive epsilon-connected ordinal natural complex real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
s . (w + w) is ext-real complex real Element of REAL
(s . (w + w)) - s1 is ext-real complex real Element of REAL
abs ((s . (w + w)) - s1) is ext-real complex real Element of REAL
Re ((s . (w + w)) - s1) is ext-real complex real Element of REAL
(Re ((s . (w + w)) - s1)) ^2 is ext-real complex real Element of REAL
(Re ((s . (w + w)) - s1)) * (Re ((s . (w + w)) - s1)) is ext-real complex real set
Im ((s . (w + w)) - s1) is ext-real complex real Element of REAL
(Im ((s . (w + w)) - s1)) ^2 is ext-real complex real Element of REAL
(Im ((s . (w + w)) - s1)) * (Im ((s . (w + w)) - s1)) is ext-real complex real set
((Re ((s . (w + w)) - s1)) ^2) + ((Im ((s . (w + w)) - s1)) ^2) is ext-real complex real Element of REAL
sqrt (((Re ((s . (w + w)) - s1)) ^2) + ((Im ((s . (w + w)) - s1)) ^2)) is ext-real complex real Element of REAL
(s . (w + w)) - s1 is ext-real complex real Element of REAL
abs ((s . (w + w)) - s1) is ext-real complex real Element of REAL
Re ((s . (w + w)) - s1) is ext-real complex real Element of REAL
(Re ((s . (w + w)) - s1)) ^2 is ext-real complex real Element of REAL
(Re ((s . (w + w)) - s1)) * (Re ((s . (w + w)) - s1)) is ext-real complex real set
Im ((s . (w + w)) - s1) is ext-real complex real Element of REAL
(Im ((s . (w + w)) - s1)) ^2 is ext-real complex real Element of REAL
(Im ((s . (w + w)) - s1)) * (Im ((s . (w + w)) - s1)) is ext-real complex real set
((Re ((s . (w + w)) - s1)) ^2) + ((Im ((s . (w + w)) - s1)) ^2) is ext-real complex real Element of REAL
sqrt (((Re ((s . (w + w)) - s1)) ^2) + ((Im ((s . (w + w)) - s1)) ^2)) is ext-real complex real Element of REAL
((abs (s1 - s1)) / 4) + ((abs (s1 - s1)) / 4) is ext-real complex real Element of REAL
(abs ((s . (w + w)) - s1)) + (abs ((s . (w + w)) - s1)) is ext-real complex real Element of REAL
- ((s . (w + w)) - s1) is ext-real complex real Element of REAL
(- ((s . (w + w)) - s1)) + ((s . (w + w)) - s1) is ext-real complex real Element of REAL
abs ((- ((s . (w + w)) - s1)) + ((s . (w + w)) - s1)) is ext-real complex real Element of REAL
Re ((- ((s . (w + w)) - s1)) + ((s . (w + w)) - s1)) is ext-real complex real Element of REAL
(Re ((- ((s . (w + w)) - s1)) + ((s . (w + w)) - s1))) ^2 is ext-real complex real Element of REAL
(Re ((- ((s . (w + w)) - s1)) + ((s . (w + w)) - s1))) * (Re ((- ((s . (w + w)) - s1)) + ((s . (w + w)) - s1))) is ext-real complex real set
Im ((- ((s . (w + w)) - s1)) + ((s . (w + w)) - s1)) is ext-real complex real Element of REAL
(Im ((- ((s . (w + w)) - s1)) + ((s . (w + w)) - s1))) ^2 is ext-real complex real Element of REAL
(Im ((- ((s . (w + w)) - s1)) + ((s . (w + w)) - s1))) * (Im ((- ((s . (w + w)) - s1)) + ((s . (w + w)) - s1))) is ext-real complex real set
((Re ((- ((s . (w + w)) - s1)) + ((s . (w + w)) - s1))) ^2) + ((Im ((- ((s . (w + w)) - s1)) + ((s . (w + w)) - s1))) ^2) is ext-real complex real Element of REAL
sqrt (((Re ((- ((s . (w + w)) - s1)) + ((s . (w + w)) - s1))) ^2) + ((Im ((- ((s . (w + w)) - s1)) + ((s . (w + w)) - s1))) ^2)) is ext-real complex real Element of REAL
abs (- ((s . (w + w)) - s1)) is ext-real complex real Element of REAL
Re (- ((s . (w + w)) - s1)) is ext-real complex real Element of REAL
(Re (- ((s . (w + w)) - s1))) ^2 is ext-real complex real Element of REAL
(Re (- ((s . (w + w)) - s1))) * (Re (- ((s . (w + w)) - s1))) is ext-real complex real set
Im (- ((s . (w + w)) - s1)) is ext-real complex real Element of REAL
(Im (- ((s . (w + w)) - s1))) ^2 is ext-real complex real Element of REAL
(Im (- ((s . (w + w)) - s1))) * (Im (- ((s . (w + w)) - s1))) is ext-real complex real set
((Re (- ((s . (w + w)) - s1))) ^2) + ((Im (- ((s . (w + w)) - s1))) ^2) is ext-real complex real Element of REAL
sqrt (((Re (- ((s . (w + w)) - s1))) ^2) + ((Im (- ((s . (w + w)) - s1))) ^2)) is ext-real complex real Element of REAL
(abs (- ((s . (w + w)) - s1))) + (abs ((s . (w + w)) - s1)) is ext-real complex real Element of REAL
(abs ((s . (w + w)) - s1)) + (abs ((s . (w + w)) - s1)) is ext-real complex real Element of REAL
(abs (s1 - s1)) / 2 is ext-real complex real Element of REAL
s is Relation-like Function-like complex-valued ext-real-valued real-valued set
s is non zero Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K11(K12(NAT,REAL))
(s) is ext-real complex real set
s is non zero Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K11(K12(NAT,REAL))
s1 is ext-real complex real Element of REAL
s1 is ext-real complex real Element of REAL
w is ext-real complex real set
w is ext-real non positive non negative zero epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real V33() V34() V45() V46() V47() V48() V49() V50() V51() Element of NAT
p is ext-real epsilon-transitive epsilon-connected ordinal natural complex real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
s . p is ext-real complex real Element of REAL
(s . p) - s1 is ext-real complex real Element of REAL
abs ((s . p) - s1) is ext-real complex real Element of REAL
Re ((s . p) - s1) is ext-real complex real Element of REAL
(Re ((s . p) - s1)) ^2 is ext-real complex real Element of REAL
(Re ((s . p) - s1)) * (Re ((s . p) - s1)) is ext-real complex real set
Im ((s . p) - s1) is ext-real complex real Element of REAL
(Im ((s . p) - s1)) ^2 is ext-real complex real Element of REAL
(Im ((s . p) - s1)) * (Im ((s . p) - s1)) is ext-real complex real set
((Re ((s . p) - s1)) ^2) + ((Im ((s . p) - s1)) ^2) is ext-real complex real Element of REAL
sqrt (((Re ((s . p) - s1)) ^2) + ((Im ((s . p) - s1)) ^2)) is ext-real complex real Element of REAL
s1 - s1 is ext-real complex real Element of REAL
abs (s1 - s1) is ext-real complex real Element of REAL
Re (s1 - s1) is ext-real complex real Element of REAL
(Re (s1 - s1)) ^2 is ext-real complex real Element of REAL
(Re (s1 - s1)) * (Re (s1 - s1)) is ext-real complex real set
Im (s1 - s1) is ext-real complex real Element of REAL
(Im (s1 - s1)) ^2 is ext-real complex real Element of REAL
(Im (s1 - s1)) * (Im (s1 - s1)) is ext-real complex real set
((Re (s1 - s1)) ^2) + ((Im (s1 - s1)) ^2) is ext-real complex real Element of REAL
sqrt (((Re (s1 - s1)) ^2) + ((Im (s1 - s1)) ^2)) is ext-real complex real Element of REAL
NAT --> 0 is non zero Relation-like NAT -defined NAT -valued RAT -valued INT -valued Function-like constant V26( NAT ) V30( NAT , NAT ) complex-valued ext-real-valued real-valued natural-valued Element of K11(K12(NAT,NAT))
K12(NAT,NAT) is RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued set
K11(K12(NAT,NAT)) is set
s is non zero Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K11(K12(NAT,REAL))
s is non zero Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K11(K12(NAT,REAL))
s1 is non zero Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K11(K12(NAT,REAL))
s + s1 is non zero Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K11(K12(NAT,REAL))
s1 is ext-real complex real set
w is ext-real complex real set
s1 + w is ext-real complex real set
w is ext-real complex real set
p is ext-real complex real set
p / 2 is ext-real complex real Element of REAL
n is ext-real epsilon-transitive epsilon-connected ordinal natural complex real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
n is ext-real epsilon-transitive epsilon-connected ordinal natural complex real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
n + n is ext-real epsilon-transitive epsilon-connected ordinal natural complex real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
m is ext-real epsilon-transitive epsilon-connected ordinal natural complex real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
n is ext-real epsilon-transitive epsilon-connected ordinal natural complex real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
(s + s1) . n is ext-real complex real Element of REAL
((s + s1) . n) - w is ext-real complex real Element of REAL
abs (((s + s1) . n) - w) is ext-real complex real Element of REAL
Re (((s + s1) . n) - w) is ext-real complex real Element of REAL
(Re (((s + s1) . n) - w)) ^2 is ext-real complex real Element of REAL
(Re (((s + s1) . n) - w)) * (Re (((s + s1) . n) - w)) is ext-real complex real set
Im (((s + s1) . n) - w) is ext-real complex real Element of REAL
(Im (((s + s1) . n) - w)) ^2 is ext-real complex real Element of REAL
(Im (((s + s1) . n) - w)) * (Im (((s + s1) . n) - w)) is ext-real complex real set
((Re (((s + s1) . n) - w)) ^2) + ((Im (((s + s1) . n) - w)) ^2) is ext-real complex real Element of REAL
sqrt (((Re (((s + s1) . n) - w)) ^2) + ((Im (((s + s1) . n) - w)) ^2)) is ext-real complex real Element of REAL
s . n is ext-real complex real Element of REAL
(s . n) - s1 is ext-real complex real Element of REAL
abs ((s . n) - s1) is ext-real complex real Element of REAL
Re ((s . n) - s1) is ext-real complex real Element of REAL
(Re ((s . n) - s1)) ^2 is ext-real complex real Element of REAL
(Re ((s . n) - s1)) * (Re ((s . n) - s1)) is ext-real complex real set
Im ((s . n) - s1) is ext-real complex real Element of REAL
(Im ((s . n) - s1)) ^2 is ext-real complex real Element of REAL
(Im ((s . n) - s1)) * (Im ((s . n) - s1)) is ext-real complex real set
((Re ((s . n) - s1)) ^2) + ((Im ((s . n) - s1)) ^2) is ext-real complex real Element of REAL
sqrt (((Re ((s . n) - s1)) ^2) + ((Im ((s . n) - s1)) ^2)) is ext-real complex real Element of REAL
s1 . n is ext-real complex real Element of REAL
(s1 . n) - w is ext-real complex real Element of REAL
abs ((s1 . n) - w) is ext-real complex real Element of REAL
Re ((s1 . n) - w) is ext-real complex real Element of REAL
(Re ((s1 . n) - w)) ^2 is ext-real complex real Element of REAL
(Re ((s1 . n) - w)) * (Re ((s1 . n) - w)) is ext-real complex real set
Im ((s1 . n) - w) is ext-real complex real Element of REAL
(Im ((s1 . n) - w)) ^2 is ext-real complex real Element of REAL
(Im ((s1 . n) - w)) * (Im ((s1 . n) - w)) is ext-real complex real set
((Re ((s1 . n) - w)) ^2) + ((Im ((s1 . n) - w)) ^2) is ext-real complex real Element of REAL
sqrt (((Re ((s1 . n) - w)) ^2) + ((Im ((s1 . n) - w)) ^2)) is ext-real complex real Element of REAL
(p / 2) + (p / 2) is ext-real complex real Element of REAL
(abs ((s . n) - s1)) + (abs ((s1 . n) - w)) is ext-real complex real Element of REAL
(s . n) + (s1 . n) is ext-real complex real Element of REAL
((s . n) + (s1 . n)) - (s1 + w) is ext-real complex real Element of REAL
abs (((s . n) + (s1 . n)) - (s1 + w)) is ext-real complex real Element of REAL
Re (((s . n) + (s1 . n)) - (s1 + w)) is ext-real complex real Element of REAL
(Re (((s . n) + (s1 . n)) - (s1 + w))) ^2 is ext-real complex real Element of REAL
(Re (((s . n) + (s1 . n)) - (s1 + w))) * (Re (((s . n) + (s1 . n)) - (s1 + w))) is ext-real complex real set
Im (((s . n) + (s1 . n)) - (s1 + w)) is ext-real complex real Element of REAL
(Im (((s . n) + (s1 . n)) - (s1 + w))) ^2 is ext-real complex real Element of REAL
(Im (((s . n) + (s1 . n)) - (s1 + w))) * (Im (((s . n) + (s1 . n)) - (s1 + w))) is ext-real complex real set
((Re (((s . n) + (s1 . n)) - (s1 + w))) ^2) + ((Im (((s . n) + (s1 . n)) - (s1 + w))) ^2) is ext-real complex real Element of REAL
sqrt (((Re (((s . n) + (s1 . n)) - (s1 + w))) ^2) + ((Im (((s . n) + (s1 . n)) - (s1 + w))) ^2)) is ext-real complex real Element of REAL
((s . n) - s1) + ((s1 . n) - w) is ext-real complex real Element of REAL
abs (((s . n) - s1) + ((s1 . n) - w)) is ext-real complex real Element of REAL
Re (((s . n) - s1) + ((s1 . n) - w)) is ext-real complex real Element of REAL
(Re (((s . n) - s1) + ((s1 . n) - w))) ^2 is ext-real complex real Element of REAL
(Re (((s . n) - s1) + ((s1 . n) - w))) * (Re (((s . n) - s1) + ((s1 . n) - w))) is ext-real complex real set
Im (((s . n) - s1) + ((s1 . n) - w)) is ext-real complex real Element of REAL
(Im (((s . n) - s1) + ((s1 . n) - w))) ^2 is ext-real complex real Element of REAL
(Im (((s . n) - s1) + ((s1 . n) - w))) * (Im (((s . n) - s1) + ((s1 . n) - w))) is ext-real complex real set
((Re (((s . n) - s1) + ((s1 . n) - w))) ^2) + ((Im (((s . n) - s1) + ((s1 . n) - w))) ^2) is ext-real complex real Element of REAL
sqrt (((Re (((s . n) - s1) + ((s1 . n) - w))) ^2) + ((Im (((s . n) - s1) + ((s1 . n) - w))) ^2)) is ext-real complex real Element of REAL
s is non zero Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued convergent Element of K11(K12(NAT,REAL))
s1 is non zero Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued convergent Element of K11(K12(NAT,REAL))
s + s1 is non zero Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K11(K12(NAT,REAL))
s1 is non zero Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K11(K12(NAT,REAL))
s is non zero Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K11(K12(NAT,REAL))
(s) is ext-real complex real Element of REAL
s1 is non zero Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K11(K12(NAT,REAL))
s + s1 is non zero Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K11(K12(NAT,REAL))
((s + s1)) is ext-real complex real Element of REAL
(s1) is ext-real complex real Element of REAL
(s) + (s1) is ext-real complex real Element of REAL
s1 is ext-real complex real set
s1 / 2 is ext-real complex real Element of REAL
w is ext-real epsilon-transitive epsilon-connected ordinal natural complex real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
w is ext-real epsilon-transitive epsilon-connected ordinal natural complex real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
w + w is ext-real epsilon-transitive epsilon-connected ordinal natural complex real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
p is ext-real epsilon-transitive epsilon-connected ordinal natural complex real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
n is ext-real epsilon-transitive epsilon-connected ordinal natural complex real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
s . n is ext-real complex real Element of REAL
(s . n) - (s) is ext-real complex real Element of REAL
abs ((s . n) - (s)) is ext-real complex real Element of REAL
Re ((s . n) - (s)) is ext-real complex real Element of REAL
(Re ((s . n) - (s))) ^2 is ext-real complex real Element of REAL
(Re ((s . n) - (s))) * (Re ((s . n) - (s))) is ext-real complex real set
Im ((s . n) - (s)) is ext-real complex real Element of REAL
(Im ((s . n) - (s))) ^2 is ext-real complex real Element of REAL
(Im ((s . n) - (s))) * (Im ((s . n) - (s))) is ext-real complex real set
((Re ((s . n) - (s))) ^2) + ((Im ((s . n) - (s))) ^2) is ext-real complex real Element of REAL
sqrt (((Re ((s . n) - (s))) ^2) + ((Im ((s . n) - (s))) ^2)) is ext-real complex real Element of REAL
s1 . n is ext-real complex real Element of REAL
(s1 . n) - (s1) is ext-real complex real Element of REAL
abs ((s1 . n) - (s1)) is ext-real complex real Element of REAL
Re ((s1 . n) - (s1)) is ext-real complex real Element of REAL
(Re ((s1 . n) - (s1))) ^2 is ext-real complex real Element of REAL
(Re ((s1 . n) - (s1))) * (Re ((s1 . n) - (s1))) is ext-real complex real set
Im ((s1 . n) - (s1)) is ext-real complex real Element of REAL
(Im ((s1 . n) - (s1))) ^2 is ext-real complex real Element of REAL
(Im ((s1 . n) - (s1))) * (Im ((s1 . n) - (s1))) is ext-real complex real set
((Re ((s1 . n) - (s1))) ^2) + ((Im ((s1 . n) - (s1))) ^2) is ext-real complex real Element of REAL
sqrt (((Re ((s1 . n) - (s1))) ^2) + ((Im ((s1 . n) - (s1))) ^2)) is ext-real complex real Element of REAL
(s1 / 2) + (s1 / 2) is ext-real complex real Element of REAL
(abs ((s . n) - (s))) + (abs ((s1 . n) - (s1))) is ext-real complex real Element of REAL
(s + s1) . n is ext-real complex real Element of REAL
((s + s1) . n) - ((s) + (s1)) is ext-real complex real Element of REAL
abs (((s + s1) . n) - ((s) + (s1))) is ext-real complex real Element of REAL
Re (((s + s1) . n) - ((s) + (s1))) is ext-real complex real Element of REAL
(Re (((s + s1) . n) - ((s) + (s1)))) ^2 is ext-real complex real Element of REAL
(Re (((s + s1) . n) - ((s) + (s1)))) * (Re (((s + s1) . n) - ((s) + (s1)))) is ext-real complex real set
Im (((s + s1) . n) - ((s) + (s1))) is ext-real complex real Element of REAL
(Im (((s + s1) . n) - ((s) + (s1)))) ^2 is ext-real complex real Element of REAL
(Im (((s + s1) . n) - ((s) + (s1)))) * (Im (((s + s1) . n) - ((s) + (s1)))) is ext-real complex real set
((Re (((s + s1) . n) - ((s) + (s1)))) ^2) + ((Im (((s + s1) . n) - ((s) + (s1)))) ^2) is ext-real complex real Element of REAL
sqrt (((Re (((s + s1) . n) - ((s) + (s1)))) ^2) + ((Im (((s + s1) . n) - ((s) + (s1)))) ^2)) is ext-real complex real Element of REAL
(s . n) + (s1 . n) is ext-real complex real Element of REAL
((s . n) + (s1 . n)) - ((s) + (s1)) is ext-real complex real Element of REAL
abs (((s . n) + (s1 . n)) - ((s) + (s1))) is ext-real complex real Element of REAL
Re (((s . n) + (s1 . n)) - ((s) + (s1))) is ext-real complex real Element of REAL
(Re (((s . n) + (s1 . n)) - ((s) + (s1)))) ^2 is ext-real complex real Element of REAL
(Re (((s . n) + (s1 . n)) - ((s) + (s1)))) * (Re (((s . n) + (s1 . n)) - ((s) + (s1)))) is ext-real complex real set
Im (((s . n) + (s1 . n)) - ((s) + (s1))) is ext-real complex real Element of REAL
(Im (((s . n) + (s1 . n)) - ((s) + (s1)))) ^2 is ext-real complex real Element of REAL
(Im (((s . n) + (s1 . n)) - ((s) + (s1)))) * (Im (((s . n) + (s1 . n)) - ((s) + (s1)))) is ext-real complex real set
((Re (((s . n) + (s1 . n)) - ((s) + (s1)))) ^2) + ((Im (((s . n) + (s1 . n)) - ((s) + (s1)))) ^2) is ext-real complex real Element of REAL
sqrt (((Re (((s . n) + (s1 . n)) - ((s) + (s1)))) ^2) + ((Im (((s . n) + (s1 . n)) - ((s) + (s1)))) ^2)) is ext-real complex real Element of REAL
((s . n) - (s)) + ((s1 . n) - (s1)) is ext-real complex real Element of REAL
abs (((s . n) - (s)) + ((s1 . n) - (s1))) is ext-real complex real Element of REAL
Re (((s . n) - (s)) + ((s1 . n) - (s1))) is ext-real complex real Element of REAL
(Re (((s . n) - (s)) + ((s1 . n) - (s1)))) ^2 is ext-real complex real Element of REAL
(Re (((s . n) - (s)) + ((s1 . n) - (s1)))) * (Re (((s . n) - (s)) + ((s1 . n) - (s1)))) is ext-real complex real set
Im (((s . n) - (s)) + ((s1 . n) - (s1))) is ext-real complex real Element of REAL
(Im (((s . n) - (s)) + ((s1 . n) - (s1)))) ^2 is ext-real complex real Element of REAL
(Im (((s . n) - (s)) + ((s1 . n) - (s1)))) * (Im (((s . n) - (s)) + ((s1 . n) - (s1)))) is ext-real complex real set
((Re (((s . n) - (s)) + ((s1 . n) - (s1)))) ^2) + ((Im (((s . n) - (s)) + ((s1 . n) - (s1)))) ^2) is ext-real complex real Element of REAL
sqrt (((Re (((s . n) - (s)) + ((s1 . n) - (s1)))) ^2) + ((Im (((s . n) - (s)) + ((s1 . n) - (s1)))) ^2)) is ext-real complex real Element of REAL
s is ext-real complex real set
s1 is non zero Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K11(K12(NAT,REAL))
s (#) s1 is non zero Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K11(K12(NAT,REAL))
s1 is ext-real complex real set
s * s1 is ext-real complex real set
w is ext-real complex real set
w is ext-real complex real set
p is ext-real non positive non negative zero epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real V33() V34() V45() V46() V47() V48() V49() V50() V51() Element of NAT
n is ext-real epsilon-transitive epsilon-connected ordinal natural complex real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
(s (#) s1) . n is ext-real complex real Element of REAL
((s (#) s1) . n) - w is ext-real complex real Element of REAL
abs (((s (#) s1) . n) - w) is ext-real complex real Element of REAL
Re (((s (#) s1) . n) - w) is ext-real complex real Element of REAL
(Re (((s (#) s1) . n) - w)) ^2 is ext-real complex real Element of REAL
(Re (((s (#) s1) . n) - w)) * (Re (((s (#) s1) . n) - w)) is ext-real complex real set
Im (((s (#) s1) . n) - w) is ext-real complex real Element of REAL
(Im (((s (#) s1) . n) - w)) ^2 is ext-real complex real Element of REAL
(Im (((s (#) s1) . n) - w)) * (Im (((s (#) s1) . n) - w)) is ext-real complex real set
((Re (((s (#) s1) . n) - w)) ^2) + ((Im (((s (#) s1) . n) - w)) ^2) is ext-real complex real Element of REAL
sqrt (((Re (((s (#) s1) . n) - w)) ^2) + ((Im (((s (#) s1) . n) - w)) ^2)) is ext-real complex real Element of REAL
s1 . n is ext-real complex real Element of REAL
0 * (s1 . n) is ext-real complex real Element of REAL
(0 * (s1 . n)) - 0 is ext-real complex real Element of REAL
abs ((0 * (s1 . n)) - 0) is ext-real complex real Element of REAL
Re ((0 * (s1 . n)) - 0) is ext-real complex real Element of REAL
(Re ((0 * (s1 . n)) - 0)) ^2 is ext-real complex real Element of REAL
(Re ((0 * (s1 . n)) - 0)) * (Re ((0 * (s1 . n)) - 0)) is ext-real complex real set
Im ((0 * (s1 . n)) - 0) is ext-real complex real Element of REAL
(Im ((0 * (s1 . n)) - 0)) ^2 is ext-real complex real Element of REAL
(Im ((0 * (s1 . n)) - 0)) * (Im ((0 * (s1 . n)) - 0)) is ext-real complex real set
((Re ((0 * (s1 . n)) - 0)) ^2) + ((Im ((0 * (s1 . n)) - 0)) ^2) is ext-real complex real Element of REAL
sqrt (((Re ((0 * (s1 . n)) - 0)) ^2) + ((Im ((0 * (s1 . n)) - 0)) ^2)) is ext-real complex real Element of REAL
abs s is ext-real complex real Element of REAL
Re s is ext-real complex real Element of REAL
(Re s) ^2 is ext-real complex real Element of REAL
(Re s) * (Re s) is ext-real complex real set
Im s is ext-real complex real Element of REAL
(Im s) ^2 is ext-real complex real Element of REAL
(Im s) * (Im s) is ext-real complex real set
((Re s) ^2) + ((Im s) ^2) is ext-real complex real Element of REAL
sqrt (((Re s) ^2) + ((Im s) ^2)) is ext-real complex real Element of REAL
w is ext-real complex real set
w / (abs s) is ext-real complex real Element of REAL
p is ext-real epsilon-transitive epsilon-connected ordinal natural complex real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
n is ext-real epsilon-transitive epsilon-connected ordinal natural complex real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
n is ext-real epsilon-transitive epsilon-connected ordinal natural complex real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
s1 . n is ext-real complex real Element of REAL
(s1 . n) - s1 is ext-real complex real Element of REAL
abs ((s1 . n) - s1) is ext-real complex real Element of REAL
Re ((s1 . n) - s1) is ext-real complex real Element of REAL
(Re ((s1 . n) - s1)) ^2 is ext-real complex real Element of REAL
(Re ((s1 . n) - s1)) * (Re ((s1 . n) - s1)) is ext-real complex real set
Im ((s1 . n) - s1) is ext-real complex real Element of REAL
(Im ((s1 . n) - s1)) ^2 is ext-real complex real Element of REAL
(Im ((s1 . n) - s1)) * (Im ((s1 . n) - s1)) is ext-real complex real set
((Re ((s1 . n) - s1)) ^2) + ((Im ((s1 . n) - s1)) ^2) is ext-real complex real Element of REAL
sqrt (((Re ((s1 . n) - s1)) ^2) + ((Im ((s1 . n) - s1)) ^2)) is ext-real complex real Element of REAL
(s (#) s1) . n is ext-real complex real Element of REAL
((s (#) s1) . n) - w is ext-real complex real Element of REAL
abs (((s (#) s1) . n) - w) is ext-real complex real Element of REAL
Re (((s (#) s1) . n) - w) is ext-real complex real Element of REAL
(Re (((s (#) s1) . n) - w)) ^2 is ext-real complex real Element of REAL
(Re (((s (#) s1) . n) - w)) * (Re (((s (#) s1) . n) - w)) is ext-real complex real set
Im (((s (#) s1) . n) - w) is ext-real complex real Element of REAL
(Im (((s (#) s1) . n) - w)) ^2 is ext-real complex real Element of REAL
(Im (((s (#) s1) . n) - w)) * (Im (((s (#) s1) . n) - w)) is ext-real complex real set
((Re (((s (#) s1) . n) - w)) ^2) + ((Im (((s (#) s1) . n) - w)) ^2) is ext-real complex real Element of REAL
sqrt (((Re (((s (#) s1) . n) - w)) ^2) + ((Im (((s (#) s1) . n) - w)) ^2)) is ext-real complex real Element of REAL
s * (s1 . n) is ext-real complex real Element of REAL
(s * (s1 . n)) - (s * s1) is ext-real complex real Element of REAL
abs ((s * (s1 . n)) - (s * s1)) is ext-real complex real Element of REAL
Re ((s * (s1 . n)) - (s * s1)) is ext-real complex real Element of REAL
(Re ((s * (s1 . n)) - (s * s1))) ^2 is ext-real complex real Element of REAL
(Re ((s * (s1 . n)) - (s * s1))) * (Re ((s * (s1 . n)) - (s * s1))) is ext-real complex real set
Im ((s * (s1 . n)) - (s * s1)) is ext-real complex real Element of REAL
(Im ((s * (s1 . n)) - (s * s1))) ^2 is ext-real complex real Element of REAL
(Im ((s * (s1 . n)) - (s * s1))) * (Im ((s * (s1 . n)) - (s * s1))) is ext-real complex real set
((Re ((s * (s1 . n)) - (s * s1))) ^2) + ((Im ((s * (s1 . n)) - (s * s1))) ^2) is ext-real complex real Element of REAL
sqrt (((Re ((s * (s1 . n)) - (s * s1))) ^2) + ((Im ((s * (s1 . n)) - (s * s1))) ^2)) is ext-real complex real Element of REAL
s * ((s1 . n) - s1) is ext-real complex real Element of REAL
abs (s * ((s1 . n) - s1)) is ext-real complex real Element of REAL
Re (s * ((s1 . n) - s1)) is ext-real complex real Element of REAL
(Re (s * ((s1 . n) - s1))) ^2 is ext-real complex real Element of REAL
(Re (s * ((s1 . n) - s1))) * (Re (s * ((s1 . n) - s1))) is ext-real complex real set
Im (s * ((s1 . n) - s1)) is ext-real complex real Element of REAL
(Im (s * ((s1 . n) - s1))) ^2 is ext-real complex real Element of REAL
(Im (s * ((s1 . n) - s1))) * (Im (s * ((s1 . n) - s1))) is ext-real complex real set
((Re (s * ((s1 . n) - s1))) ^2) + ((Im (s * ((s1 . n) - s1))) ^2) is ext-real complex real Element of REAL
sqrt (((Re (s * ((s1 . n) - s1))) ^2) + ((Im (s * ((s1 . n) - s1))) ^2)) is ext-real complex real Element of REAL
(abs s) * (abs ((s1 . n) - s1)) is ext-real complex real Element of REAL
(abs s) * (w / (abs s)) is ext-real complex real Element of REAL
(abs s) " is ext-real complex real Element of REAL
((abs s) ") * w is ext-real complex real Element of REAL
(abs s) * (((abs s) ") * w) is ext-real complex real Element of REAL
(abs s) * ((abs s) ") is ext-real complex real Element of REAL
((abs s) * ((abs s) ")) * w is ext-real complex real Element of REAL
1 * w is ext-real complex real Element of REAL
w is ext-real complex real set
s1 is non zero Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued convergent Element of K11(K12(NAT,REAL))
s is ext-real complex real set
s (#) s1 is non zero Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K11(K12(NAT,REAL))
s1 is non zero Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K11(K12(NAT,REAL))
s is ext-real complex real set
s1 is non zero Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K11(K12(NAT,REAL))
s (#) s1 is non zero Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K11(K12(NAT,REAL))
((s (#) s1)) is ext-real complex real Element of REAL
(s1) is ext-real complex real Element of REAL
s * (s1) is ext-real complex real Element of REAL
s1 is ext-real complex real set
w is ext-real non positive non negative zero epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real V33() V34() V45() V46() V47() V48() V49() V50() V51() Element of NAT
w is ext-real epsilon-transitive epsilon-connected ordinal natural complex real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
(s (#) s1) . w is ext-real complex real Element of REAL
((s (#) s1) . w) - (s * (s1)) is ext-real complex real Element of REAL
abs (((s (#) s1) . w) - (s * (s1))) is ext-real complex real Element of REAL
Re (((s (#) s1) . w) - (s * (s1))) is ext-real complex real Element of REAL
(Re (((s (#) s1) . w) - (s * (s1)))) ^2 is ext-real complex real Element of REAL
(Re (((s (#) s1) . w) - (s * (s1)))) * (Re (((s (#) s1) . w) - (s * (s1)))) is ext-real complex real set
Im (((s (#) s1) . w) - (s * (s1))) is ext-real complex real Element of REAL
(Im (((s (#) s1) . w) - (s * (s1)))) ^2 is ext-real complex real Element of REAL
(Im (((s (#) s1) . w) - (s * (s1)))) * (Im (((s (#) s1) . w) - (s * (s1)))) is ext-real complex real set
((Re (((s (#) s1) . w) - (s * (s1)))) ^2) + ((Im (((s (#) s1) . w) - (s * (s1)))) ^2) is ext-real complex real Element of REAL
sqrt (((Re (((s (#) s1) . w) - (s * (s1)))) ^2) + ((Im (((s (#) s1) . w) - (s * (s1)))) ^2)) is ext-real complex real Element of REAL
s1 . w is ext-real complex real Element of REAL
0 * (s1 . w) is ext-real complex real Element of REAL
(0 * (s1 . w)) - 0 is ext-real complex real Element of REAL
abs ((0 * (s1 . w)) - 0) is ext-real complex real Element of REAL
Re ((0 * (s1 . w)) - 0) is ext-real complex real Element of REAL
(Re ((0 * (s1 . w)) - 0)) ^2 is ext-real complex real Element of REAL
(Re ((0 * (s1 . w)) - 0)) * (Re ((0 * (s1 . w)) - 0)) is ext-real complex real set
Im ((0 * (s1 . w)) - 0) is ext-real complex real Element of REAL
(Im ((0 * (s1 . w)) - 0)) ^2 is ext-real complex real Element of REAL
(Im ((0 * (s1 . w)) - 0)) * (Im ((0 * (s1 . w)) - 0)) is ext-real complex real set
((Re ((0 * (s1 . w)) - 0)) ^2) + ((Im ((0 * (s1 . w)) - 0)) ^2) is ext-real complex real Element of REAL
sqrt (((Re ((0 * (s1 . w)) - 0)) ^2) + ((Im ((0 * (s1 . w)) - 0)) ^2)) is ext-real complex real Element of REAL
abs s is ext-real complex real Element of REAL
Re s is ext-real complex real Element of REAL
(Re s) ^2 is ext-real complex real Element of REAL
(Re s) * (Re s) is ext-real complex real set
Im s is ext-real complex real Element of REAL
(Im s) ^2 is ext-real complex real Element of REAL
(Im s) * (Im s) is ext-real complex real set
((Re s) ^2) + ((Im s) ^2) is ext-real complex real Element of REAL
sqrt (((Re s) ^2) + ((Im s) ^2)) is ext-real complex real Element of REAL
s1 is ext-real complex real set
s1 / (abs s) is ext-real complex real Element of REAL
w is ext-real epsilon-transitive epsilon-connected ordinal natural complex real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
w is ext-real epsilon-transitive epsilon-connected ordinal natural complex real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
p is ext-real epsilon-transitive epsilon-connected ordinal natural complex real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
s1 . p is ext-real complex real Element of REAL
(s1 . p) - (s1) is ext-real complex real Element of REAL
abs ((s1 . p) - (s1)) is ext-real complex real Element of REAL
Re ((s1 . p) - (s1)) is ext-real complex real Element of REAL
(Re ((s1 . p) - (s1))) ^2 is ext-real complex real Element of REAL
(Re ((s1 . p) - (s1))) * (Re ((s1 . p) - (s1))) is ext-real complex real set
Im ((s1 . p) - (s1)) is ext-real complex real Element of REAL
(Im ((s1 . p) - (s1))) ^2 is ext-real complex real Element of REAL
(Im ((s1 . p) - (s1))) * (Im ((s1 . p) - (s1))) is ext-real complex real set
((Re ((s1 . p) - (s1))) ^2) + ((Im ((s1 . p) - (s1))) ^2) is ext-real complex real Element of REAL
sqrt (((Re ((s1 . p) - (s1))) ^2) + ((Im ((s1 . p) - (s1))) ^2)) is ext-real complex real Element of REAL
(s (#) s1) . p is ext-real complex real Element of REAL
((s (#) s1) . p) - (s * (s1)) is ext-real complex real Element of REAL
abs (((s (#) s1) . p) - (s * (s1))) is ext-real complex real Element of REAL
Re (((s (#) s1) . p) - (s * (s1))) is ext-real complex real Element of REAL
(Re (((s (#) s1) . p) - (s * (s1)))) ^2 is ext-real complex real Element of REAL
(Re (((s (#) s1) . p) - (s * (s1)))) * (Re (((s (#) s1) . p) - (s * (s1)))) is ext-real complex real set
Im (((s (#) s1) . p) - (s * (s1))) is ext-real complex real Element of REAL
(Im (((s (#) s1) . p) - (s * (s1)))) ^2 is ext-real complex real Element of REAL
(Im (((s (#) s1) . p) - (s * (s1)))) * (Im (((s (#) s1) . p) - (s * (s1)))) is ext-real complex real set
((Re (((s (#) s1) . p) - (s * (s1)))) ^2) + ((Im (((s (#) s1) . p) - (s * (s1)))) ^2) is ext-real complex real Element of REAL
sqrt (((Re (((s (#) s1) . p) - (s * (s1)))) ^2) + ((Im (((s (#) s1) . p) - (s * (s1)))) ^2)) is ext-real complex real Element of REAL
s * (s1 . p) is ext-real complex real Element of REAL
(s * (s1 . p)) - (s * (s1)) is ext-real complex real Element of REAL
abs ((s * (s1 . p)) - (s * (s1))) is ext-real complex real Element of REAL
Re ((s * (s1 . p)) - (s * (s1))) is ext-real complex real Element of REAL
(Re ((s * (s1 . p)) - (s * (s1)))) ^2 is ext-real complex real Element of REAL
(Re ((s * (s1 . p)) - (s * (s1)))) * (Re ((s * (s1 . p)) - (s * (s1)))) is ext-real complex real set
Im ((s * (s1 . p)) - (s * (s1))) is ext-real complex real Element of REAL
(Im ((s * (s1 . p)) - (s * (s1)))) ^2 is ext-real complex real Element of REAL
(Im ((s * (s1 . p)) - (s * (s1)))) * (Im ((s * (s1 . p)) - (s * (s1)))) is ext-real complex real set
((Re ((s * (s1 . p)) - (s * (s1)))) ^2) + ((Im ((s * (s1 . p)) - (s * (s1)))) ^2) is ext-real complex real Element of REAL
sqrt (((Re ((s * (s1 . p)) - (s * (s1)))) ^2) + ((Im ((s * (s1 . p)) - (s * (s1)))) ^2)) is ext-real complex real Element of REAL
s * ((s1 . p) - (s1)) is ext-real complex real Element of REAL
abs (s * ((s1 . p) - (s1))) is ext-real complex real Element of REAL
Re (s * ((s1 . p) - (s1))) is ext-real complex real Element of REAL
(Re (s * ((s1 . p) - (s1)))) ^2 is ext-real complex real Element of REAL
(Re (s * ((s1 . p) - (s1)))) * (Re (s * ((s1 . p) - (s1)))) is ext-real complex real set
Im (s * ((s1 . p) - (s1))) is ext-real complex real Element of REAL
(Im (s * ((s1 . p) - (s1)))) ^2 is ext-real complex real Element of REAL
(Im (s * ((s1 . p) - (s1)))) * (Im (s * ((s1 . p) - (s1)))) is ext-real complex real set
((Re (s * ((s1 . p) - (s1)))) ^2) + ((Im (s * ((s1 . p) - (s1)))) ^2) is ext-real complex real Element of REAL
sqrt (((Re (s * ((s1 . p) - (s1)))) ^2) + ((Im (s * ((s1 . p) - (s1)))) ^2)) is ext-real complex real Element of REAL
(abs s) * (abs ((s1 . p) - (s1))) is ext-real complex real Element of REAL
(abs s) * (s1 / (abs s)) is ext-real complex real Element of REAL
(abs s) " is ext-real complex real Element of REAL
((abs s) ") * s1 is ext-real complex real Element of REAL
(abs s) * (((abs s) ") * s1) is ext-real complex real Element of REAL
(abs s) * ((abs s) ") is ext-real complex real Element of REAL
((abs s) * ((abs s) ")) * s1 is ext-real complex real Element of REAL
1 * s1 is ext-real complex real Element of REAL
s is non zero Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K11(K12(NAT,REAL))
- s is non zero Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K11(K12(NAT,REAL))
- 1 is ext-real non positive negative non zero complex real set
(- 1) (#) s is Relation-like NAT -defined Function-like V26( NAT ) complex-valued ext-real-valued real-valued set
s is non zero Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued convergent Element of K11(K12(NAT,REAL))
- s is non zero Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K11(K12(NAT,REAL))
- 1 is ext-real non positive negative non zero complex real set
(- 1) (#) s is Relation-like NAT -defined Function-like V26( NAT ) complex-valued ext-real-valued real-valued set
s1 is non zero Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K11(K12(NAT,REAL))
s is non zero Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K11(K12(NAT,REAL))
- s is non zero Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K11(K12(NAT,REAL))
(- 1) (#) s is Relation-like NAT -defined Function-like V26( NAT ) complex-valued ext-real-valued real-valued set
((- s)) is ext-real complex real Element of REAL
(s) is ext-real complex real Element of REAL
- (s) is ext-real complex real Element of REAL
- 1 is ext-real non positive negative non zero complex real Element of REAL
(- 1) (#) s is non zero Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K11(K12(NAT,REAL))
(((- 1) (#) s)) is ext-real complex real Element of REAL
(- 1) * (s) is ext-real complex real Element of REAL
s is non zero Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K11(K12(NAT,REAL))
s1 is non zero Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K11(K12(NAT,REAL))
s - s1 is non zero Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K11(K12(NAT,REAL))
- s1 is Relation-like NAT -defined Function-like V26( NAT ) complex-valued ext-real-valued real-valued set
(- 1) (#) s1 is Relation-like NAT -defined Function-like V26( NAT ) complex-valued ext-real-valued real-valued set
s + (- s1) is Relation-like NAT -defined Function-like V26( NAT ) complex-valued ext-real-valued real-valued set
- s1 is non zero Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K11(K12(NAT,REAL))
s is non zero Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued convergent Element of K11(K12(NAT,REAL))
s1 is non zero Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued convergent Element of K11(K12(NAT,REAL))
s - s1 is non zero Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K11(K12(NAT,REAL))
- s1 is Relation-like NAT -defined Function-like V26( NAT ) complex-valued ext-real-valued real-valued set
(- 1) (#) s1 is Relation-like NAT -defined Function-like V26( NAT ) complex-valued ext-real-valued real-valued set
s + (- s1) is Relation-like NAT -defined Function-like V26( NAT ) complex-valued ext-real-valued real-valued set
s1 is non zero Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K11(K12(NAT,REAL))
s is non zero Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K11(K12(NAT,REAL))
(s) is ext-real complex real Element of REAL
s1 is non zero Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K11(K12(NAT,REAL))
s - s1 is non zero Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K11(K12(NAT,REAL))
- s1 is Relation-like NAT -defined Function-like V26( NAT ) complex-valued ext-real-valued real-valued set
(- 1) (#) s1 is Relation-like NAT -defined Function-like V26( NAT ) complex-valued ext-real-valued real-valued set
s + (- s1) is Relation-like NAT -defined Function-like V26( NAT ) complex-valued ext-real-valued real-valued set
((s - s1)) is ext-real complex real Element of REAL
(s1) is ext-real complex real Element of REAL
(s) - (s1) is ext-real complex real Element of REAL
- s1 is non zero Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K11(K12(NAT,REAL))
((- s1)) is ext-real complex real Element of REAL
(s) + ((- s1)) is ext-real complex real Element of REAL
- (s1) is ext-real complex real Element of REAL
(s) + (- (s1)) is ext-real complex real Element of REAL
s is non zero Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K11(K12(NAT,REAL))
s1 is ext-real complex real set
s1 is ext-real epsilon-transitive epsilon-connected ordinal natural complex real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
abs s1 is ext-real complex real Element of REAL
Re s1 is ext-real complex real Element of REAL
(Re s1) ^2 is ext-real complex real Element of REAL
(Re s1) * (Re s1) is ext-real complex real set
Im s1 is ext-real complex real Element of REAL
(Im s1) ^2 is ext-real complex real Element of REAL
(Im s1) * (Im s1) is ext-real complex real set
((Re s1) ^2) + ((Im s1) ^2) is ext-real complex real Element of REAL
sqrt (((Re s1) ^2) + ((Im s1) ^2)) is ext-real complex real Element of REAL
(abs s1) + 1 is ext-real complex real Element of REAL
w is ext-real complex real Element of REAL
0 + 0 is ext-real non positive non negative zero epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real V33() V34() V45() V46() V47() V48() V49() V50() V51() Element of NAT
w is ext-real epsilon-transitive epsilon-connected ordinal natural complex real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
s . w is ext-real complex real Element of REAL
(s . w) - s1 is ext-real complex real Element of REAL
abs ((s . w) - s1) is ext-real complex real Element of REAL
Re ((s . w) - s1) is ext-real complex real Element of REAL
(Re ((s . w) - s1)) ^2 is ext-real complex real Element of REAL
(Re ((s . w) - s1)) * (Re ((s . w) - s1)) is ext-real complex real set
Im ((s . w) - s1) is ext-real complex real Element of REAL
(Im ((s . w) - s1)) ^2 is ext-real complex real Element of REAL
(Im ((s . w) - s1)) * (Im ((s . w) - s1)) is ext-real complex real set
((Re ((s . w) - s1)) ^2) + ((Im ((s . w) - s1)) ^2) is ext-real complex real Element of REAL
sqrt (((Re ((s . w) - s1)) ^2) + ((Im ((s . w) - s1)) ^2)) is ext-real complex real Element of REAL
abs (s . w) is ext-real complex real Element of REAL
Re (s . w) is ext-real complex real Element of REAL
(Re (s . w)) ^2 is ext-real complex real Element of REAL
(Re (s . w)) * (Re (s . w)) is ext-real complex real set
Im (s . w) is ext-real complex real Element of REAL
(Im (s . w)) ^2 is ext-real complex real Element of REAL
(Im (s . w)) * (Im (s . w)) is ext-real complex real set
((Re (s . w)) ^2) + ((Im (s . w)) ^2) is ext-real complex real Element of REAL
sqrt (((Re (s . w)) ^2) + ((Im (s . w)) ^2)) is ext-real complex real Element of REAL
(abs (s . w)) - (abs s1) is ext-real complex real Element of REAL
((abs (s . w)) - (abs s1)) + (abs s1) is ext-real complex real Element of REAL
w is ext-real complex real Element of REAL
w is ext-real complex real set
w is ext-real complex real set
w + w is ext-real complex real set
p is ext-real complex real set
w + 0 is ext-real complex real Element of REAL
0 + w is ext-real complex real Element of REAL
n is ext-real epsilon-transitive epsilon-connected ordinal natural complex real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
s . n is ext-real complex real Element of REAL
abs (s . n) is ext-real complex real Element of REAL
Re (s . n) is ext-real complex real Element of REAL
(Re (s . n)) ^2 is ext-real complex real Element of REAL
(Re (s . n)) * (Re (s . n)) is ext-real complex real set
Im (s . n) is ext-real complex real Element of REAL
(Im (s . n)) ^2 is ext-real complex real Element of REAL
(Im (s . n)) * (Im (s . n)) is ext-real complex real set
((Re (s . n)) ^2) + ((Im (s . n)) ^2) is ext-real complex real Element of REAL
sqrt (((Re (s . n)) ^2) + ((Im (s . n)) ^2)) is ext-real complex real Element of REAL
w is ext-real complex real set
s is non zero Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K11(K12(NAT,REAL))
s is non zero Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K11(K12(NAT,REAL))
s1 is non zero Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K11(K12(NAT,REAL))
s (#) s1 is non zero Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K11(K12(NAT,REAL))
s1 is ext-real complex real set
w is ext-real complex real set
s1 * w is ext-real complex real set
w is ext-real complex real set
p is ext-real complex real set
abs w is ext-real complex real Element of REAL
Re w is ext-real complex real Element of REAL
(Re w) ^2 is ext-real complex real Element of REAL
(Re w) * (Re w) is ext-real complex real set
Im w is ext-real complex real Element of REAL
(Im w) ^2 is ext-real complex real Element of REAL
(Im w) * (Im w) is ext-real complex real set
((Re w) ^2) + ((Im w) ^2) is ext-real complex real Element of REAL
sqrt (((Re w) ^2) + ((Im w) ^2)) is ext-real complex real Element of REAL
(abs w) + p is ext-real complex real Element of REAL
0 + 0 is ext-real non positive non negative zero epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real V33() V34() V45() V46() V47() V48() V49() V50() V51() Element of NAT
n is ext-real complex real set
n / ((abs w) + p) is ext-real complex real Element of REAL
n is ext-real epsilon-transitive epsilon-connected ordinal natural complex real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
m is ext-real epsilon-transitive epsilon-connected ordinal natural complex real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
n + m is ext-real epsilon-transitive epsilon-connected ordinal natural complex real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
n is ext-real epsilon-transitive epsilon-connected ordinal natural complex real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
m is ext-real epsilon-transitive epsilon-connected ordinal natural complex real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
(s (#) s1) . m is ext-real complex real Element of REAL
((s (#) s1) . m) - w is ext-real complex real Element of REAL
abs (((s (#) s1) . m) - w) is ext-real complex real Element of REAL
Re (((s (#) s1) . m) - w) is ext-real complex real Element of REAL
(Re (((s (#) s1) . m) - w)) ^2 is ext-real complex real Element of REAL
(Re (((s (#) s1) . m) - w)) * (Re (((s (#) s1) . m) - w)) is ext-real complex real set
Im (((s (#) s1) . m) - w) is ext-real complex real Element of REAL
(Im (((s (#) s1) . m) - w)) ^2 is ext-real complex real Element of REAL
(Im (((s (#) s1) . m) - w)) * (Im (((s (#) s1) . m) - w)) is ext-real complex real set
((Re (((s (#) s1) . m) - w)) ^2) + ((Im (((s (#) s1) . m) - w)) ^2) is ext-real complex real Element of REAL
sqrt (((Re (((s (#) s1) . m) - w)) ^2) + ((Im (((s (#) s1) . m) - w)) ^2)) is ext-real complex real Element of REAL
s . m is ext-real complex real Element of REAL
abs (s . m) is ext-real complex real Element of REAL
Re (s . m) is ext-real complex real Element of REAL
(Re (s . m)) ^2 is ext-real complex real Element of REAL
(Re (s . m)) * (Re (s . m)) is ext-real complex real set
Im (s . m) is ext-real complex real Element of REAL
(Im (s . m)) ^2 is ext-real complex real Element of REAL
(Im (s . m)) * (Im (s . m)) is ext-real complex real set
((Re (s . m)) ^2) + ((Im (s . m)) ^2) is ext-real complex real Element of REAL
sqrt (((Re (s . m)) ^2) + ((Im (s . m)) ^2)) is ext-real complex real Element of REAL
s1 . m is ext-real complex real Element of REAL
(s1 . m) - w is ext-real complex real Element of REAL
abs ((s1 . m) - w) is ext-real complex real Element of REAL
Re ((s1 . m) - w) is ext-real complex real Element of REAL
(Re ((s1 . m) - w)) ^2 is ext-real complex real Element of REAL
(Re ((s1 . m) - w)) * (Re ((s1 . m) - w)) is ext-real complex real set
Im ((s1 . m) - w) is ext-real complex real Element of REAL
(Im ((s1 . m) - w)) ^2 is ext-real complex real Element of REAL
(Im ((s1 . m) - w)) * (Im ((s1 . m) - w)) is ext-real complex real set
((Re ((s1 . m) - w)) ^2) + ((Im ((s1 . m) - w)) ^2) is ext-real complex real Element of REAL
sqrt (((Re ((s1 . m) - w)) ^2) + ((Im ((s1 . m) - w)) ^2)) is ext-real complex real Element of REAL
(s . m) - s1 is ext-real complex real Element of REAL
abs ((s . m) - s1) is ext-real complex real Element of REAL
Re ((s . m) - s1) is ext-real complex real Element of REAL
(Re ((s . m) - s1)) ^2 is ext-real complex real Element of REAL
(Re ((s . m) - s1)) * (Re ((s . m) - s1)) is ext-real complex real set
Im ((s . m) - s1) is ext-real complex real Element of REAL
(Im ((s . m) - s1)) ^2 is ext-real complex real Element of REAL
(Im ((s . m) - s1)) * (Im ((s . m) - s1)) is ext-real complex real set
((Re ((s . m) - s1)) ^2) + ((Im ((s . m) - s1)) ^2) is ext-real complex real Element of REAL
sqrt (((Re ((s . m) - s1)) ^2) + ((Im ((s . m) - s1)) ^2)) is ext-real complex real Element of REAL
(s . m) * (s1 . m) is ext-real complex real Element of REAL
(s . m) * w is ext-real complex real Element of REAL
((s . m) * w) - ((s . m) * w) is ext-real complex real Element of REAL
((s . m) * (s1 . m)) - (((s . m) * w) - ((s . m) * w)) is ext-real complex real Element of REAL
(((s . m) * (s1 . m)) - (((s . m) * w) - ((s . m) * w))) - (s1 * w) is ext-real complex real Element of REAL
abs ((((s . m) * (s1 . m)) - (((s . m) * w) - ((s . m) * w))) - (s1 * w)) is ext-real complex real Element of REAL
Re ((((s . m) * (s1 . m)) - (((s . m) * w) - ((s . m) * w))) - (s1 * w)) is ext-real complex real Element of REAL
(Re ((((s . m) * (s1 . m)) - (((s . m) * w) - ((s . m) * w))) - (s1 * w))) ^2 is ext-real complex real Element of REAL
(Re ((((s . m) * (s1 . m)) - (((s . m) * w) - ((s . m) * w))) - (s1 * w))) * (Re ((((s . m) * (s1 . m)) - (((s . m) * w) - ((s . m) * w))) - (s1 * w))) is ext-real complex real set
Im ((((s . m) * (s1 . m)) - (((s . m) * w) - ((s . m) * w))) - (s1 * w)) is ext-real complex real Element of REAL
(Im ((((s . m) * (s1 . m)) - (((s . m) * w) - ((s . m) * w))) - (s1 * w))) ^2 is ext-real complex real Element of REAL
(Im ((((s . m) * (s1 . m)) - (((s . m) * w) - ((s . m) * w))) - (s1 * w))) * (Im ((((s . m) * (s1 . m)) - (((s . m) * w) - ((s . m) * w))) - (s1 * w))) is ext-real complex real set
((Re ((((s . m) * (s1 . m)) - (((s . m) * w) - ((s . m) * w))) - (s1 * w))) ^2) + ((Im ((((s . m) * (s1 . m)) - (((s . m) * w) - ((s . m) * w))) - (s1 * w))) ^2) is ext-real complex real Element of REAL
sqrt (((Re ((((s . m) * (s1 . m)) - (((s . m) * w) - ((s . m) * w))) - (s1 * w))) ^2) + ((Im ((((s . m) * (s1 . m)) - (((s . m) * w) - ((s . m) * w))) - (s1 * w))) ^2)) is ext-real complex real Element of REAL
(s . m) * ((s1 . m) - w) is ext-real complex real Element of REAL
((s . m) - s1) * w is ext-real complex real Element of REAL
((s . m) * ((s1 . m) - w)) + (((s . m) - s1) * w) is ext-real complex real Element of REAL
abs (((s . m) * ((s1 . m) - w)) + (((s . m) - s1) * w)) is ext-real complex real Element of REAL
Re (((s . m) * ((s1 . m) - w)) + (((s . m) - s1) * w)) is ext-real complex real Element of REAL
(Re (((s . m) * ((s1 . m) - w)) + (((s . m) - s1) * w))) ^2 is ext-real complex real Element of REAL
(Re (((s . m) * ((s1 . m) - w)) + (((s . m) - s1) * w))) * (Re (((s . m) * ((s1 . m) - w)) + (((s . m) - s1) * w))) is ext-real complex real set
Im (((s . m) * ((s1 . m) - w)) + (((s . m) - s1) * w)) is ext-real complex real Element of REAL
(Im (((s . m) * ((s1 . m) - w)) + (((s . m) - s1) * w))) ^2 is ext-real complex real Element of REAL
(Im (((s . m) * ((s1 . m) - w)) + (((s . m) - s1) * w))) * (Im (((s . m) * ((s1 . m) - w)) + (((s . m) - s1) * w))) is ext-real complex real set
((Re (((s . m) * ((s1 . m) - w)) + (((s . m) - s1) * w))) ^2) + ((Im (((s . m) * ((s1 . m) - w)) + (((s . m) - s1) * w))) ^2) is ext-real complex real Element of REAL
sqrt (((Re (((s . m) * ((s1 . m) - w)) + (((s . m) - s1) * w))) ^2) + ((Im (((s . m) * ((s1 . m) - w)) + (((s . m) - s1) * w))) ^2)) is ext-real complex real Element of REAL
abs ((s . m) * ((s1 . m) - w)) is ext-real complex real Element of REAL
Re ((s . m) * ((s1 . m) - w)) is ext-real complex real Element of REAL
(Re ((s . m) * ((s1 . m) - w))) ^2 is ext-real complex real Element of REAL
(Re ((s . m) * ((s1 . m) - w))) * (Re ((s . m) * ((s1 . m) - w))) is ext-real complex real set
Im ((s . m) * ((s1 . m) - w)) is ext-real complex real Element of REAL
(Im ((s . m) * ((s1 . m) - w))) ^2 is ext-real complex real Element of REAL
(Im ((s . m) * ((s1 . m) - w))) * (Im ((s . m) * ((s1 . m) - w))) is ext-real complex real set
((Re ((s . m) * ((s1 . m) - w))) ^2) + ((Im ((s . m) * ((s1 . m) - w))) ^2) is ext-real complex real Element of REAL
sqrt (((Re ((s . m) * ((s1 . m) - w))) ^2) + ((Im ((s . m) * ((s1 . m) - w))) ^2)) is ext-real complex real Element of REAL
abs (((s . m) - s1) * w) is ext-real complex real Element of REAL
Re (((s . m) - s1) * w) is ext-real complex real Element of REAL
(Re (((s . m) - s1) * w)) ^2 is ext-real complex real Element of REAL
(Re (((s . m) - s1) * w)) * (Re (((s . m) - s1) * w)) is ext-real complex real set
Im (((s . m) - s1) * w) is ext-real complex real Element of REAL
(Im (((s . m) - s1) * w)) ^2 is ext-real complex real Element of REAL
(Im (((s . m) - s1) * w)) * (Im (((s . m) - s1) * w)) is ext-real complex real set
((Re (((s . m) - s1) * w)) ^2) + ((Im (((s . m) - s1) * w)) ^2) is ext-real complex real Element of REAL
sqrt (((Re (((s . m) - s1) * w)) ^2) + ((Im (((s . m) - s1) * w)) ^2)) is ext-real complex real Element of REAL
(abs ((s . m) * ((s1 . m) - w))) + (abs (((s . m) - s1) * w)) is ext-real complex real Element of REAL
p * (n / ((abs w) + p)) is ext-real complex real Element of REAL
(abs (s . m)) * (abs ((s1 . m) - w)) is ext-real complex real Element of REAL
(abs w) * (abs ((s . m) - s1)) is ext-real complex real Element of REAL
(abs w) * (n / ((abs w) + p)) is ext-real complex real Element of REAL
(p * (n / ((abs w) + p))) + ((abs w) * (n / ((abs w) + p))) is ext-real complex real Element of REAL
(n / ((abs w) + p)) * ((abs w) + p) is ext-real complex real Element of REAL
s is non zero Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued bounded convergent () () Element of K11(K12(NAT,REAL))
s1 is non zero Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued bounded convergent () () Element of K11(K12(NAT,REAL))
s (#) s1 is non zero Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K11(K12(NAT,REAL))
s1 is non zero Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K11(K12(NAT,REAL))
s is non zero Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K11(K12(NAT,REAL))
(s) is ext-real complex real Element of REAL
s1 is non zero Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K11(K12(NAT,REAL))
s (#) s1 is non zero Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K11(K12(NAT,REAL))
((s (#) s1)) is ext-real complex real Element of REAL
(s1) is ext-real complex real Element of REAL
(s) * (s1) is ext-real complex real Element of REAL
s1 is ext-real complex real set
abs (s1) is ext-real complex real Element of REAL
Re (s1) is ext-real complex real Element of REAL
(Re (s1)) ^2 is ext-real complex real Element of REAL
(Re (s1)) * (Re (s1)) is ext-real complex real set
Im (s1) is ext-real complex real Element of REAL
(Im (s1)) ^2 is ext-real complex real Element of REAL
(Im (s1)) * (Im (s1)) is ext-real complex real set
((Re (s1)) ^2) + ((Im (s1)) ^2) is ext-real complex real Element of REAL
sqrt (((Re (s1)) ^2) + ((Im (s1)) ^2)) is ext-real complex real Element of REAL
(abs (s1)) + s1 is ext-real complex real Element of REAL
0 + 0 is ext-real non positive non negative zero epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real V33() V34() V45() V46() V47() V48() V49() V50() V51() Element of NAT
w is ext-real complex real set
w / ((abs (s1)) + s1) is ext-real complex real Element of REAL
w is ext-real epsilon-transitive epsilon-connected ordinal natural complex real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
p is ext-real epsilon-transitive epsilon-connected ordinal natural complex real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
w + p is ext-real epsilon-transitive epsilon-connected ordinal natural complex real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
n is ext-real epsilon-transitive epsilon-connected ordinal natural complex real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
n is ext-real epsilon-transitive epsilon-connected ordinal natural complex real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
s . n is ext-real complex real Element of REAL
abs (s . n) is ext-real complex real Element of REAL
Re (s . n) is ext-real complex real Element of REAL
(Re (s . n)) ^2 is ext-real complex real Element of REAL
(Re (s . n)) * (Re (s . n)) is ext-real complex real set
Im (s . n) is ext-real complex real Element of REAL
(Im (s . n)) ^2 is ext-real complex real Element of REAL
(Im (s . n)) * (Im (s . n)) is ext-real complex real set
((Re (s . n)) ^2) + ((Im (s . n)) ^2) is ext-real complex real Element of REAL
sqrt (((Re (s . n)) ^2) + ((Im (s . n)) ^2)) is ext-real complex real Element of REAL
s1 . n is ext-real complex real Element of REAL
(s1 . n) - (s1) is ext-real complex real Element of REAL
abs ((s1 . n) - (s1)) is ext-real complex real Element of REAL
Re ((s1 . n) - (s1)) is ext-real complex real Element of REAL
(Re ((s1 . n) - (s1))) ^2 is ext-real complex real Element of REAL
(Re ((s1 . n) - (s1))) * (Re ((s1 . n) - (s1))) is ext-real complex real set
Im ((s1 . n) - (s1)) is ext-real complex real Element of REAL
(Im ((s1 . n) - (s1))) ^2 is ext-real complex real Element of REAL
(Im ((s1 . n) - (s1))) * (Im ((s1 . n) - (s1))) is ext-real complex real set
((Re ((s1 . n) - (s1))) ^2) + ((Im ((s1 . n) - (s1))) ^2) is ext-real complex real Element of REAL
sqrt (((Re ((s1 . n) - (s1))) ^2) + ((Im ((s1 . n) - (s1))) ^2)) is ext-real complex real Element of REAL
(s . n) - (s) is ext-real complex real Element of REAL
abs ((s . n) - (s)) is ext-real complex real Element of REAL
Re ((s . n) - (s)) is ext-real complex real Element of REAL
(Re ((s . n) - (s))) ^2 is ext-real complex real Element of REAL
(Re ((s . n) - (s))) * (Re ((s . n) - (s))) is ext-real complex real set
Im ((s . n) - (s)) is ext-real complex real Element of REAL
(Im ((s . n) - (s))) ^2 is ext-real complex real Element of REAL
(Im ((s . n) - (s))) * (Im ((s . n) - (s))) is ext-real complex real set
((Re ((s . n) - (s))) ^2) + ((Im ((s . n) - (s))) ^2) is ext-real complex real Element of REAL
sqrt (((Re ((s . n) - (s))) ^2) + ((Im ((s . n) - (s))) ^2)) is ext-real complex real Element of REAL
(s (#) s1) . n is ext-real complex real Element of REAL
((s (#) s1) . n) - ((s) * (s1)) is ext-real complex real Element of REAL
abs (((s (#) s1) . n) - ((s) * (s1))) is ext-real complex real Element of REAL
Re (((s (#) s1) . n) - ((s) * (s1))) is ext-real complex real Element of REAL
(Re (((s (#) s1) . n) - ((s) * (s1)))) ^2 is ext-real complex real Element of REAL
(Re (((s (#) s1) . n) - ((s) * (s1)))) * (Re (((s (#) s1) . n) - ((s) * (s1)))) is ext-real complex real set
Im (((s (#) s1) . n) - ((s) * (s1))) is ext-real complex real Element of REAL
(Im (((s (#) s1) . n) - ((s) * (s1)))) ^2 is ext-real complex real Element of REAL
(Im (((s (#) s1) . n) - ((s) * (s1)))) * (Im (((s (#) s1) . n) - ((s) * (s1)))) is ext-real complex real set
((Re (((s (#) s1) . n) - ((s) * (s1)))) ^2) + ((Im (((s (#) s1) . n) - ((s) * (s1)))) ^2) is ext-real complex real Element of REAL
sqrt (((Re (((s (#) s1) . n) - ((s) * (s1)))) ^2) + ((Im (((s (#) s1) . n) - ((s) * (s1)))) ^2)) is ext-real complex real Element of REAL
(s . n) * (s1 . n) is ext-real complex real Element of REAL
(s . n) * (s1) is ext-real complex real Element of REAL
((s . n) * (s1)) - ((s . n) * (s1)) is ext-real complex real Element of REAL
((s . n) * (s1 . n)) - (((s . n) * (s1)) - ((s . n) * (s1))) is ext-real complex real Element of REAL
(((s . n) * (s1 . n)) - (((s . n) * (s1)) - ((s . n) * (s1)))) - ((s) * (s1)) is ext-real complex real Element of REAL
abs ((((s . n) * (s1 . n)) - (((s . n) * (s1)) - ((s . n) * (s1)))) - ((s) * (s1))) is ext-real complex real Element of REAL
Re ((((s . n) * (s1 . n)) - (((s . n) * (s1)) - ((s . n) * (s1)))) - ((s) * (s1))) is ext-real complex real Element of REAL
(Re ((((s . n) * (s1 . n)) - (((s . n) * (s1)) - ((s . n) * (s1)))) - ((s) * (s1)))) ^2 is ext-real complex real Element of REAL
(Re ((((s . n) * (s1 . n)) - (((s . n) * (s1)) - ((s . n) * (s1)))) - ((s) * (s1)))) * (Re ((((s . n) * (s1 . n)) - (((s . n) * (s1)) - ((s . n) * (s1)))) - ((s) * (s1)))) is ext-real complex real set
Im ((((s . n) * (s1 . n)) - (((s . n) * (s1)) - ((s . n) * (s1)))) - ((s) * (s1))) is ext-real complex real Element of REAL
(Im ((((s . n) * (s1 . n)) - (((s . n) * (s1)) - ((s . n) * (s1)))) - ((s) * (s1)))) ^2 is ext-real complex real Element of REAL
(Im ((((s . n) * (s1 . n)) - (((s . n) * (s1)) - ((s . n) * (s1)))) - ((s) * (s1)))) * (Im ((((s . n) * (s1 . n)) - (((s . n) * (s1)) - ((s . n) * (s1)))) - ((s) * (s1)))) is ext-real complex real set
((Re ((((s . n) * (s1 . n)) - (((s . n) * (s1)) - ((s . n) * (s1)))) - ((s) * (s1)))) ^2) + ((Im ((((s . n) * (s1 . n)) - (((s . n) * (s1)) - ((s . n) * (s1)))) - ((s) * (s1)))) ^2) is ext-real complex real Element of REAL
sqrt (((Re ((((s . n) * (s1 . n)) - (((s . n) * (s1)) - ((s . n) * (s1)))) - ((s) * (s1)))) ^2) + ((Im ((((s . n) * (s1 . n)) - (((s . n) * (s1)) - ((s . n) * (s1)))) - ((s) * (s1)))) ^2)) is ext-real complex real Element of REAL
(s . n) * ((s1 . n) - (s1)) is ext-real complex real Element of REAL
((s . n) - (s)) * (s1) is ext-real complex real Element of REAL
((s . n) * ((s1 . n) - (s1))) + (((s . n) - (s)) * (s1)) is ext-real complex real Element of REAL
abs (((s . n) * ((s1 . n) - (s1))) + (((s . n) - (s)) * (s1))) is ext-real complex real Element of REAL
Re (((s . n) * ((s1 . n) - (s1))) + (((s . n) - (s)) * (s1))) is ext-real complex real Element of REAL
(Re (((s . n) * ((s1 . n) - (s1))) + (((s . n) - (s)) * (s1)))) ^2 is ext-real complex real Element of REAL
(Re (((s . n) * ((s1 . n) - (s1))) + (((s . n) - (s)) * (s1)))) * (Re (((s . n) * ((s1 . n) - (s1))) + (((s . n) - (s)) * (s1)))) is ext-real complex real set
Im (((s . n) * ((s1 . n) - (s1))) + (((s . n) - (s)) * (s1))) is ext-real complex real Element of REAL
(Im (((s . n) * ((s1 . n) - (s1))) + (((s . n) - (s)) * (s1)))) ^2 is ext-real complex real Element of REAL
(Im (((s . n) * ((s1 . n) - (s1))) + (((s . n) - (s)) * (s1)))) * (Im (((s . n) * ((s1 . n) - (s1))) + (((s . n) - (s)) * (s1)))) is ext-real complex real set
((Re (((s . n) * ((s1 . n) - (s1))) + (((s . n) - (s)) * (s1)))) ^2) + ((Im (((s . n) * ((s1 . n) - (s1))) + (((s . n) - (s)) * (s1)))) ^2) is ext-real complex real Element of REAL
sqrt (((Re (((s . n) * ((s1 . n) - (s1))) + (((s . n) - (s)) * (s1)))) ^2) + ((Im (((s . n) * ((s1 . n) - (s1))) + (((s . n) - (s)) * (s1)))) ^2)) is ext-real complex real Element of REAL
abs ((s . n) * ((s1 . n) - (s1))) is ext-real complex real Element of REAL
Re ((s . n) * ((s1 . n) - (s1))) is ext-real complex real Element of REAL
(Re ((s . n) * ((s1 . n) - (s1)))) ^2 is ext-real complex real Element of REAL
(Re ((s . n) * ((s1 . n) - (s1)))) * (Re ((s . n) * ((s1 . n) - (s1)))) is ext-real complex real set
Im ((s . n) * ((s1 . n) - (s1))) is ext-real complex real Element of REAL
(Im ((s . n) * ((s1 . n) - (s1)))) ^2 is ext-real complex real Element of REAL
(Im ((s . n) * ((s1 . n) - (s1)))) * (Im ((s . n) * ((s1 . n) - (s1)))) is ext-real complex real set
((Re ((s . n) * ((s1 . n) - (s1)))) ^2) + ((Im ((s . n) * ((s1 . n) - (s1)))) ^2) is ext-real complex real Element of REAL
sqrt (((Re ((s . n) * ((s1 . n) - (s1)))) ^2) + ((Im ((s . n) * ((s1 . n) - (s1)))) ^2)) is ext-real complex real Element of REAL
abs (((s . n) - (s)) * (s1)) is ext-real complex real Element of REAL
Re (((s . n) - (s)) * (s1)) is ext-real complex real Element of REAL
(Re (((s . n) - (s)) * (s1))) ^2 is ext-real complex real Element of REAL
(Re (((s . n) - (s)) * (s1))) * (Re (((s . n) - (s)) * (s1))) is ext-real complex real set
Im (((s . n) - (s)) * (s1)) is ext-real complex real Element of REAL
(Im (((s . n) - (s)) * (s1))) ^2 is ext-real complex real Element of REAL
(Im (((s . n) - (s)) * (s1))) * (Im (((s . n) - (s)) * (s1))) is ext-real complex real set
((Re (((s . n) - (s)) * (s1))) ^2) + ((Im (((s . n) - (s)) * (s1))) ^2) is ext-real complex real Element of REAL
sqrt (((Re (((s . n) - (s)) * (s1))) ^2) + ((Im (((s . n) - (s)) * (s1))) ^2)) is ext-real complex real Element of REAL
(abs ((s . n) * ((s1 . n) - (s1)))) + (abs (((s . n) - (s)) * (s1))) is ext-real complex real Element of REAL
s1 * (w / ((abs (s1)) + s1)) is ext-real complex real Element of REAL
(abs (s . n)) * (abs ((s1 . n) - (s1))) is ext-real complex real Element of REAL
(abs (s1)) * (abs ((s . n) - (s))) is ext-real complex real Element of REAL
(abs (s1)) * (w / ((abs (s1)) + s1)) is ext-real complex real Element of REAL
(s1 * (w / ((abs (s1)) + s1))) + ((abs (s1)) * (w / ((abs (s1)) + s1))) is ext-real complex real Element of REAL
(w / ((abs (s1)) + s1)) * ((abs (s1)) + s1) is ext-real complex real Element of REAL
s is non zero Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K11(K12(NAT,REAL))
(s) is ext-real complex real Element of REAL
abs (s) is ext-real complex real Element of REAL
Re (s) is ext-real complex real Element of REAL
(Re (s)) ^2 is ext-real complex real Element of REAL
(Re (s)) * (Re (s)) is ext-real complex real set
Im (s) is ext-real complex real Element of REAL
(Im (s)) ^2 is ext-real complex real Element of REAL
(Im (s)) * (Im (s)) is ext-real complex real set
((Re (s)) ^2) + ((Im (s)) ^2) is ext-real complex real Element of REAL
sqrt (((Re (s)) ^2) + ((Im (s)) ^2)) is ext-real complex real Element of REAL
(abs (s)) / 2 is ext-real complex real Element of REAL
s1 is ext-real epsilon-transitive epsilon-connected ordinal natural complex real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
s1 is ext-real epsilon-transitive epsilon-connected ordinal natural complex real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
w is ext-real epsilon-transitive epsilon-connected ordinal natural complex real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
s . w is ext-real complex real Element of REAL
abs (s . w) is ext-real complex real Element of REAL
Re (s . w) is ext-real complex real Element of REAL
(Re (s . w)) ^2 is ext-real complex real Element of REAL
(Re (s . w)) * (Re (s . w)) is ext-real complex real set
Im (s . w) is ext-real complex real Element of REAL
(Im (s . w)) ^2 is ext-real complex real Element of REAL
(Im (s . w)) * (Im (s . w)) is ext-real complex real set
((Re (s . w)) ^2) + ((Im (s . w)) ^2) is ext-real complex real Element of REAL
sqrt (((Re (s . w)) ^2) + ((Im (s . w)) ^2)) is ext-real complex real Element of REAL
(s . w) - (s) is ext-real complex real Element of REAL
abs ((s . w) - (s)) is ext-real complex real Element of REAL
Re ((s . w) - (s)) is ext-real complex real Element of REAL
(Re ((s . w) - (s))) ^2 is ext-real complex real Element of REAL
(Re ((s . w) - (s))) * (Re ((s . w) - (s))) is ext-real complex real set
Im ((s . w) - (s)) is ext-real complex real Element of REAL
(Im ((s . w) - (s))) ^2 is ext-real complex real Element of REAL
(Im ((s . w) - (s))) * (Im ((s . w) - (s))) is ext-real complex real set
((Re ((s . w) - (s))) ^2) + ((Im ((s . w) - (s))) ^2) is ext-real complex real Element of REAL
sqrt (((Re ((s . w) - (s))) ^2) + ((Im ((s . w) - (s))) ^2)) is ext-real complex real Element of REAL
(abs (s)) - (abs (s . w)) is ext-real complex real Element of REAL
(s) - (s . w) is ext-real complex real Element of REAL
abs ((s) - (s . w)) is ext-real complex real Element of REAL
Re ((s) - (s . w)) is ext-real complex real Element of REAL
(Re ((s) - (s . w))) ^2 is ext-real complex real Element of REAL
(Re ((s) - (s . w))) * (Re ((s) - (s . w))) is ext-real complex real set
Im ((s) - (s . w)) is ext-real complex real Element of REAL
(Im ((s) - (s . w))) ^2 is ext-real complex real Element of REAL
(Im ((s) - (s . w))) * (Im ((s) - (s . w))) is ext-real complex real set
((Re ((s) - (s . w))) ^2) + ((Im ((s) - (s . w))) ^2) is ext-real complex real Element of REAL
sqrt (((Re ((s) - (s . w))) ^2) + ((Im ((s) - (s . w))) ^2)) is ext-real complex real Element of REAL
- ((s . w) - (s)) is ext-real complex real Element of REAL
abs (- ((s . w) - (s))) is ext-real complex real Element of REAL
Re (- ((s . w) - (s))) is ext-real complex real Element of REAL
(Re (- ((s . w) - (s)))) ^2 is ext-real complex real Element of REAL
(Re (- ((s . w) - (s)))) * (Re (- ((s . w) - (s)))) is ext-real complex real set
Im (- ((s . w) - (s))) is ext-real complex real Element of REAL
(Im (- ((s . w) - (s)))) ^2 is ext-real complex real Element of REAL
(Im (- ((s . w) - (s)))) * (Im (- ((s . w) - (s)))) is ext-real complex real set
((Re (- ((s . w) - (s)))) ^2) + ((Im (- ((s . w) - (s)))) ^2) is ext-real complex real Element of REAL
sqrt (((Re (- ((s . w) - (s)))) ^2) + ((Im (- ((s . w) - (s)))) ^2)) is ext-real complex real Element of REAL
(abs (s . w)) - ((abs (s)) / 2) is ext-real complex real Element of REAL
((abs (s)) / 2) + ((abs (s . w)) - ((abs (s)) / 2)) is ext-real complex real Element of REAL
((abs (s)) - (abs (s . w))) + ((abs (s . w)) - ((abs (s)) / 2)) is ext-real complex real Element of REAL
s is non zero Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K11(K12(NAT,REAL))
(s) is ext-real complex real Element of REAL
- (s) is ext-real complex real Element of REAL
s1 is ext-real epsilon-transitive epsilon-connected ordinal natural complex real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
s . s1 is ext-real complex real Element of REAL
(s . s1) - (s) is ext-real complex real Element of REAL
abs ((s . s1) - (s)) is ext-real complex real Element of REAL
Re ((s . s1) - (s)) is ext-real complex real Element of REAL
(Re ((s . s1) - (s))) ^2 is ext-real complex real Element of REAL
(Re ((s . s1) - (s))) * (Re ((s . s1) - (s))) is ext-real complex real set
Im ((s . s1) - (s)) is ext-real complex real Element of REAL
(Im ((s . s1) - (s))) ^2 is ext-real complex real Element of REAL
(Im ((s . s1) - (s))) * (Im ((s . s1) - (s))) is ext-real complex real set
((Re ((s . s1) - (s))) ^2) + ((Im ((s . s1) - (s))) ^2) is ext-real complex real Element of REAL
sqrt (((Re ((s . s1) - (s))) ^2) + ((Im ((s . s1) - (s))) ^2)) is ext-real complex real Element of REAL
((s . s1) - (s)) + (s) is ext-real complex real Element of REAL
(- (s)) + (s) is ext-real complex real Element of REAL
s is non zero Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K11(K12(NAT,REAL))
(s) is ext-real complex real Element of REAL
s1 is non zero Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K11(K12(NAT,REAL))
(s1) is ext-real complex real Element of REAL
s1 is ext-real epsilon-transitive epsilon-connected ordinal natural complex real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
s . s1 is ext-real complex real Element of REAL
s1 . s1 is ext-real complex real Element of REAL
(s . s1) - (s . s1) is ext-real complex real Element of REAL
(s1 . s1) - (s . s1) is ext-real complex real Element of REAL
s1 - s is non zero Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K11(K12(NAT,REAL))
- s is Relation-like NAT -defined Function-like V26( NAT ) complex-valued ext-real-valued real-valued set
(- 1) (#) s is Relation-like NAT -defined Function-like V26( NAT ) complex-valued ext-real-valued real-valued set
s1 + (- s) is Relation-like NAT -defined Function-like V26( NAT ) complex-valued ext-real-valued real-valued set
(s1 - s) . s1 is ext-real complex real Element of REAL
- s is non zero Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K11(K12(NAT,REAL))
(- s) . s1 is ext-real complex real Element of REAL
(s1 . s1) + ((- s) . s1) is ext-real complex real Element of REAL
- (s . s1) is ext-real complex real Element of REAL
(s1 . s1) + (- (s . s1)) is ext-real complex real Element of REAL
((s1 - s)) is ext-real complex real Element of REAL
(s1) - (s) is ext-real complex real Element of REAL
0 + (s) is ext-real complex real Element of REAL
((s1) - (s)) + (s) is ext-real complex real Element of REAL
s is non zero Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K11(K12(NAT,REAL))
(s) is ext-real complex real Element of REAL
s1 is non zero Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K11(K12(NAT,REAL))
(s1) is ext-real complex real Element of REAL
s1 is non zero Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K11(K12(NAT,REAL))
w is ext-real complex real set
w is ext-real epsilon-transitive epsilon-connected ordinal natural complex real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
p is ext-real epsilon-transitive epsilon-connected ordinal natural complex real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
w + p is ext-real epsilon-transitive epsilon-connected ordinal natural complex real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
n is ext-real epsilon-transitive epsilon-connected ordinal natural complex real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
n is ext-real epsilon-transitive epsilon-connected ordinal natural complex real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
s1 . n is ext-real complex real Element of REAL
(s1 . n) - (s) is ext-real complex real Element of REAL
abs ((s1 . n) - (s)) is ext-real complex real Element of REAL
Re ((s1 . n) - (s)) is ext-real complex real Element of REAL
(Re ((s1 . n) - (s))) ^2 is ext-real complex real Element of REAL
(Re ((s1 . n) - (s))) * (Re ((s1 . n) - (s))) is ext-real complex real set
Im ((s1 . n) - (s)) is ext-real complex real Element of REAL
(Im ((s1 . n) - (s))) ^2 is ext-real complex real Element of REAL
(Im ((s1 . n) - (s))) * (Im ((s1 . n) - (s))) is ext-real complex real set
((Re ((s1 . n) - (s))) ^2) + ((Im ((s1 . n) - (s))) ^2) is ext-real complex real Element of REAL
sqrt (((Re ((s1 . n) - (s))) ^2) + ((Im ((s1 . n) - (s))) ^2)) is ext-real complex real Element of REAL
s1 . n is ext-real complex real Element of REAL
(s1 . n) - (s) is ext-real complex real Element of REAL
abs ((s1 . n) - (s)) is ext-real complex real Element of REAL
Re ((s1 . n) - (s)) is ext-real complex real Element of REAL
(Re ((s1 . n) - (s))) ^2 is ext-real complex real Element of REAL
(Re ((s1 . n) - (s))) * (Re ((s1 . n) - (s))) is ext-real complex real set
Im ((s1 . n) - (s)) is ext-real complex real Element of REAL
(Im ((s1 . n) - (s))) ^2 is ext-real complex real Element of REAL
(Im ((s1 . n) - (s))) * (Im ((s1 . n) - (s))) is ext-real complex real set
((Re ((s1 . n) - (s))) ^2) + ((Im ((s1 . n) - (s))) ^2) is ext-real complex real Element of REAL
sqrt (((Re ((s1 . n) - (s))) ^2) + ((Im ((s1 . n) - (s))) ^2)) is ext-real complex real Element of REAL
s . n is ext-real complex real Element of REAL
(s . n) - (s) is ext-real complex real Element of REAL
abs ((s . n) - (s)) is ext-real complex real Element of REAL
Re ((s . n) - (s)) is ext-real complex real Element of REAL
(Re ((s . n) - (s))) ^2 is ext-real complex real Element of REAL
(Re ((s . n) - (s))) * (Re ((s . n) - (s))) is ext-real complex real set
Im ((s . n) - (s)) is ext-real complex real Element of REAL
(Im ((s . n) - (s))) ^2 is ext-real complex real Element of REAL
(Im ((s . n) - (s))) * (Im ((s . n) - (s))) is ext-real complex real set
((Re ((s . n) - (s))) ^2) + ((Im ((s . n) - (s))) ^2) is ext-real complex real Element of REAL
sqrt (((Re ((s . n) - (s))) ^2) + ((Im ((s . n) - (s))) ^2)) is ext-real complex real Element of REAL
- w is ext-real complex real set
s is non zero Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K11(K12(NAT,REAL))
(s) is ext-real complex real Element of REAL
s1 is non zero Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K11(K12(NAT,REAL))
(s1) is ext-real complex real Element of REAL
s1 is non zero Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K11(K12(NAT,REAL))
(s1) is ext-real complex real Element of REAL
w is ext-real complex real set
w is ext-real epsilon-transitive epsilon-connected ordinal natural complex real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
p is ext-real epsilon-transitive epsilon-connected ordinal natural complex real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
w + p is ext-real epsilon-transitive epsilon-connected ordinal natural complex real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
n is ext-real epsilon-transitive epsilon-connected ordinal natural complex real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
n is ext-real epsilon-transitive epsilon-connected ordinal natural complex real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
s1 . n is ext-real complex real Element of REAL
(s1 . n) - (s) is ext-real complex real Element of REAL
abs ((s1 . n) - (s)) is ext-real complex real Element of REAL
Re ((s1 . n) - (s)) is ext-real complex real Element of REAL
(Re ((s1 . n) - (s))) ^2 is ext-real complex real Element of REAL
(Re ((s1 . n) - (s))) * (Re ((s1 . n) - (s))) is ext-real complex real set
Im ((s1 . n) - (s)) is ext-real complex real Element of REAL
(Im ((s1 . n) - (s))) ^2 is ext-real complex real Element of REAL
(Im ((s1 . n) - (s))) * (Im ((s1 . n) - (s))) is ext-real complex real set
((Re ((s1 . n) - (s))) ^2) + ((Im ((s1 . n) - (s))) ^2) is ext-real complex real Element of REAL
sqrt (((Re ((s1 . n) - (s))) ^2) + ((Im ((s1 . n) - (s))) ^2)) is ext-real complex real Element of REAL
s . n is ext-real complex real Element of REAL
(s . n) - (s) is ext-real complex real Element of REAL
abs ((s . n) - (s)) is ext-real complex real Element of REAL
Re ((s . n) - (s)) is ext-real complex real Element of REAL
(Re ((s . n) - (s))) ^2 is ext-real complex real Element of REAL
(Re ((s . n) - (s))) * (Re ((s . n) - (s))) is ext-real complex real set
Im ((s . n) - (s)) is ext-real complex real Element of REAL
(Im ((s . n) - (s))) ^2 is ext-real complex real Element of REAL
(Im ((s . n) - (s))) * (Im ((s . n) - (s))) is ext-real complex real set
((Re ((s . n) - (s))) ^2) + ((Im ((s . n) - (s))) ^2) is ext-real complex real Element of REAL
sqrt (((Re ((s . n) - (s))) ^2) + ((Im ((s . n) - (s))) ^2)) is ext-real complex real Element of REAL
- w is ext-real complex real set
s1 . n is ext-real complex real Element of REAL
(s1 . n) - (s) is ext-real complex real Element of REAL
abs ((s1 . n) - (s)) is ext-real complex real Element of REAL
Re ((s1 . n) - (s)) is ext-real complex real Element of REAL
(Re ((s1 . n) - (s))) ^2 is ext-real complex real Element of REAL
(Re ((s1 . n) - (s))) * (Re ((s1 . n) - (s))) is ext-real complex real set
Im ((s1 . n) - (s)) is ext-real complex real Element of REAL
(Im ((s1 . n) - (s))) ^2 is ext-real complex real Element of REAL
(Im ((s1 . n) - (s))) * (Im ((s1 . n) - (s))) is ext-real complex real set
((Re ((s1 . n) - (s))) ^2) + ((Im ((s1 . n) - (s))) ^2) is ext-real complex real Element of REAL
sqrt (((Re ((s1 . n) - (s))) ^2) + ((Im ((s1 . n) - (s))) ^2)) is ext-real complex real Element of REAL
s is non zero Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K11(K12(NAT,REAL))
(s) is ext-real complex real Element of REAL
s " is non zero Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K11(K12(NAT,REAL))
abs (s) is ext-real complex real Element of REAL
Re (s) is ext-real complex real Element of REAL
(Re (s)) ^2 is ext-real complex real Element of REAL
(Re (s)) * (Re (s)) is ext-real complex real set
Im (s) is ext-real complex real Element of REAL
(Im (s)) ^2 is ext-real complex real Element of REAL
(Im (s)) * (Im (s)) is ext-real complex real set
((Re (s)) ^2) + ((Im (s)) ^2) is ext-real complex real Element of REAL
sqrt (((Re (s)) ^2) + ((Im (s)) ^2)) is ext-real complex real Element of REAL
(abs (s)) / 2 is ext-real complex real Element of REAL
s1 is ext-real epsilon-transitive epsilon-connected ordinal natural complex real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
(abs (s)) * (abs (s)) is ext-real complex real Element of REAL
0 * 0 is ext-real non positive non negative zero epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real V33() V34() V45() V46() V47() V48() V49() V50() V51() Element of NAT
((abs (s)) * (abs (s))) / 2 is ext-real complex real Element of REAL
(s) " is ext-real complex real Element of REAL
s1 is ext-real complex real set
s1 * (((abs (s)) * (abs (s))) / 2) is ext-real complex real Element of REAL
w is ext-real epsilon-transitive epsilon-connected ordinal natural complex real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
s1 + w is ext-real epsilon-transitive epsilon-connected ordinal natural complex real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
w is ext-real epsilon-transitive epsilon-connected ordinal natural complex real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
p is ext-real epsilon-transitive epsilon-connected ordinal natural complex real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
(s ") . p is ext-real complex real Element of REAL
((s ") . p) - ((s) ") is ext-real complex real Element of REAL
abs (((s ") . p) - ((s) ")) is ext-real complex real Element of REAL
Re (((s ") . p) - ((s) ")) is ext-real complex real Element of REAL
(Re (((s ") . p) - ((s) "))) ^2 is ext-real complex real Element of REAL
(Re (((s ") . p) - ((s) "))) * (Re (((s ") . p) - ((s) "))) is ext-real complex real set
Im (((s ") . p) - ((s) ")) is ext-real complex real Element of REAL
(Im (((s ") . p) - ((s) "))) ^2 is ext-real complex real Element of REAL
(Im (((s ") . p) - ((s) "))) * (Im (((s ") . p) - ((s) "))) is ext-real complex real set
((Re (((s ") . p) - ((s) "))) ^2) + ((Im (((s ") . p) - ((s) "))) ^2) is ext-real complex real Element of REAL
sqrt (((Re (((s ") . p) - ((s) "))) ^2) + ((Im (((s ") . p) - ((s) "))) ^2)) is ext-real complex real Element of REAL
s . p is ext-real complex real Element of REAL
(s . p) - (s) is ext-real complex real Element of REAL
abs ((s . p) - (s)) is ext-real complex real Element of REAL
Re ((s . p) - (s)) is ext-real complex real Element of REAL
(Re ((s . p) - (s))) ^2 is ext-real complex real Element of REAL
(Re ((s . p) - (s))) * (Re ((s . p) - (s))) is ext-real complex real set
Im ((s . p) - (s)) is ext-real complex real Element of REAL
(Im ((s . p) - (s))) ^2 is ext-real complex real Element of REAL
(Im ((s . p) - (s))) * (Im ((s . p) - (s))) is ext-real complex real set
((Re ((s . p) - (s))) ^2) + ((Im ((s . p) - (s))) ^2) is ext-real complex real Element of REAL
sqrt (((Re ((s . p) - (s))) ^2) + ((Im ((s . p) - (s))) ^2)) is ext-real complex real Element of REAL
abs (s . p) is ext-real complex real Element of REAL
Re (s . p) is ext-real complex real Element of REAL
(Re (s . p)) ^2 is ext-real complex real Element of REAL
(Re (s . p)) * (Re (s . p)) is ext-real complex real set
Im (s . p) is ext-real complex real Element of REAL
(Im (s . p)) ^2 is ext-real complex real Element of REAL
(Im (s . p)) * (Im (s . p)) is ext-real complex real set
((Re (s . p)) ^2) + ((Im (s . p)) ^2) is ext-real complex real Element of REAL
sqrt (((Re (s . p)) ^2) + ((Im (s . p)) ^2)) is ext-real complex real Element of REAL
(s . p) * (s) is ext-real complex real Element of REAL
abs ((s . p) * (s)) is ext-real complex real Element of REAL
Re ((s . p) * (s)) is ext-real complex real Element of REAL
(Re ((s . p) * (s))) ^2 is ext-real complex real Element of REAL
(Re ((s . p) * (s))) * (Re ((s . p) * (s))) is ext-real complex real set
Im ((s . p) * (s)) is ext-real complex real Element of REAL
(Im ((s . p) * (s))) ^2 is ext-real complex real Element of REAL
(Im ((s . p) * (s))) * (Im ((s . p) * (s))) is ext-real complex real set
((Re ((s . p) * (s))) ^2) + ((Im ((s . p) * (s))) ^2) is ext-real complex real Element of REAL
sqrt (((Re ((s . p) * (s))) ^2) + ((Im ((s . p) * (s))) ^2)) is ext-real complex real Element of REAL
(abs (s . p)) * (abs (s)) is ext-real complex real Element of REAL
(s1 * (((abs (s)) * (abs (s))) / 2)) / ((abs (s . p)) * (abs (s))) is ext-real complex real Element of REAL
(abs ((s . p) - (s))) / ((abs (s . p)) * (abs (s))) is ext-real complex real Element of REAL
2 " is ext-real positive non negative non zero complex real Element of REAL
(2 ") * ((abs (s)) * (abs (s))) is ext-real complex real Element of REAL
s1 * ((2 ") * ((abs (s)) * (abs (s)))) is ext-real complex real Element of REAL
((abs (s . p)) * (abs (s))) " is ext-real complex real Element of REAL
(s1 * ((2 ") * ((abs (s)) * (abs (s))))) * (((abs (s . p)) * (abs (s))) ") is ext-real complex real Element of REAL
s1 * (2 ") is ext-real complex real Element of REAL
(abs (s)) * (abs (s . p)) is ext-real complex real Element of REAL
((abs (s)) * (abs (s . p))) " is ext-real complex real Element of REAL
((abs (s)) * (abs (s))) * (((abs (s)) * (abs (s . p))) ") is ext-real complex real Element of REAL
(s1 * (2 ")) * (((abs (s)) * (abs (s))) * (((abs (s)) * (abs (s . p))) ")) is ext-real complex real Element of REAL
(abs (s)) " is ext-real complex real Element of REAL
(abs (s . p)) " is ext-real complex real Element of REAL
((abs (s)) ") * ((abs (s . p)) ") is ext-real complex real Element of REAL
((abs (s)) * (abs (s))) * (((abs (s)) ") * ((abs (s . p)) ")) is ext-real complex real Element of REAL
(s1 * (2 ")) * (((abs (s)) * (abs (s))) * (((abs (s)) ") * ((abs (s . p)) "))) is ext-real complex real Element of REAL
(abs (s)) * ((abs (s)) ") is ext-real complex real Element of REAL
(abs (s)) * ((abs (s)) * ((abs (s)) ")) is ext-real complex real Element of REAL
((abs (s)) * ((abs (s)) * ((abs (s)) "))) * ((abs (s . p)) ") is ext-real complex real Element of REAL
(s1 * (2 ")) * (((abs (s)) * ((abs (s)) * ((abs (s)) "))) * ((abs (s . p)) ")) is ext-real complex real Element of REAL
(abs (s)) * 1 is ext-real complex real Element of REAL
((abs (s)) * 1) * ((abs (s . p)) ") is ext-real complex real Element of REAL
(s1 * (2 ")) * (((abs (s)) * 1) * ((abs (s . p)) ")) is ext-real complex real Element of REAL
s1 * ((abs (s)) / 2) is ext-real complex real Element of REAL
(s1 * ((abs (s)) / 2)) * ((abs (s . p)) ") is ext-real complex real Element of REAL
(s1 * ((abs (s)) / 2)) / (abs (s . p)) is ext-real complex real Element of REAL
(s . p) " is ext-real complex real Element of REAL
((s . p) ") - ((s) ") is ext-real complex real Element of REAL
abs (((s . p) ") - ((s) ")) is ext-real complex real Element of REAL
Re (((s . p) ") - ((s) ")) is ext-real complex real Element of REAL
(Re (((s . p) ") - ((s) "))) ^2 is ext-real complex real Element of REAL
(Re (((s . p) ") - ((s) "))) * (Re (((s . p) ") - ((s) "))) is ext-real complex real set
Im (((s . p) ") - ((s) ")) is ext-real complex real Element of REAL
(Im (((s . p) ") - ((s) "))) ^2 is ext-real complex real Element of REAL
(Im (((s . p) ") - ((s) "))) * (Im (((s . p) ") - ((s) "))) is ext-real complex real set
((Re (((s . p) ") - ((s) "))) ^2) + ((Im (((s . p) ") - ((s) "))) ^2) is ext-real complex real Element of REAL
sqrt (((Re (((s . p) ") - ((s) "))) ^2) + ((Im (((s . p) ") - ((s) "))) ^2)) is ext-real complex real Element of REAL
(s1 * ((abs (s)) / 2)) / ((abs (s)) / 2) is ext-real complex real Element of REAL
((abs (s)) / 2) " is ext-real complex real Element of REAL
(s1 * ((abs (s)) / 2)) * (((abs (s)) / 2) ") is ext-real complex real Element of REAL
((abs (s)) / 2) * (((abs (s)) / 2) ") is ext-real complex real Element of REAL
s1 * (((abs (s)) / 2) * (((abs (s)) / 2) ")) is ext-real complex real Element of REAL
s1 * 1 is ext-real complex real Element of REAL
s is non zero Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K11(K12(NAT,REAL))
(s) is ext-real complex real Element of REAL
s " is non zero Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K11(K12(NAT,REAL))
((s ")) is ext-real complex real Element of REAL
(s) " is ext-real complex real Element of REAL
abs (s) is ext-real complex real Element of REAL
Re (s) is ext-real complex real Element of REAL
(Re (s)) ^2 is ext-real complex real Element of REAL
(Re (s)) * (Re (s)) is ext-real complex real set
Im (s) is ext-real complex real Element of REAL
(Im (s)) ^2 is ext-real complex real Element of REAL
(Im (s)) * (Im (s)) is ext-real complex real set
((Re (s)) ^2) + ((Im (s)) ^2) is ext-real complex real Element of REAL
sqrt (((Re (s)) ^2) + ((Im (s)) ^2)) is ext-real complex real Element of REAL
(abs (s)) / 2 is ext-real complex real Element of REAL
s1 is ext-real epsilon-transitive epsilon-connected ordinal natural complex real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
(abs (s)) * (abs (s)) is ext-real complex real Element of REAL
0 * 0 is ext-real non positive non negative zero epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real V33() V34() V45() V46() V47() V48() V49() V50() V51() Element of NAT
((abs (s)) * (abs (s))) / 2 is ext-real complex real Element of REAL
s1 is ext-real complex real set
s1 * (((abs (s)) * (abs (s))) / 2) is ext-real complex real Element of REAL
w is ext-real epsilon-transitive epsilon-connected ordinal natural complex real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
s1 + w is ext-real epsilon-transitive epsilon-connected ordinal natural complex real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
w is ext-real epsilon-transitive epsilon-connected ordinal natural complex real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
p is ext-real epsilon-transitive epsilon-connected ordinal natural complex real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
s . p is ext-real complex real Element of REAL
(s . p) - (s) is ext-real complex real Element of REAL
abs ((s . p) - (s)) is ext-real complex real Element of REAL
Re ((s . p) - (s)) is ext-real complex real Element of REAL
(Re ((s . p) - (s))) ^2 is ext-real complex real Element of REAL
(Re ((s . p) - (s))) * (Re ((s . p) - (s))) is ext-real complex real set
Im ((s . p) - (s)) is ext-real complex real Element of REAL
(Im ((s . p) - (s))) ^2 is ext-real complex real Element of REAL
(Im ((s . p) - (s))) * (Im ((s . p) - (s))) is ext-real complex real set
((Re ((s . p) - (s))) ^2) + ((Im ((s . p) - (s))) ^2) is ext-real complex real Element of REAL
sqrt (((Re ((s . p) - (s))) ^2) + ((Im ((s . p) - (s))) ^2)) is ext-real complex real Element of REAL
abs (s . p) is ext-real complex real Element of REAL
Re (s . p) is ext-real complex real Element of REAL
(Re (s . p)) ^2 is ext-real complex real Element of REAL
(Re (s . p)) * (Re (s . p)) is ext-real complex real set
Im (s . p) is ext-real complex real Element of REAL
(Im (s . p)) ^2 is ext-real complex real Element of REAL
(Im (s . p)) * (Im (s . p)) is ext-real complex real set
((Re (s . p)) ^2) + ((Im (s . p)) ^2) is ext-real complex real Element of REAL
sqrt (((Re (s . p)) ^2) + ((Im (s . p)) ^2)) is ext-real complex real Element of REAL
(s . p) * (s) is ext-real complex real Element of REAL
abs ((s . p) * (s)) is ext-real complex real Element of REAL
Re ((s . p) * (s)) is ext-real complex real Element of REAL
(Re ((s . p) * (s))) ^2 is ext-real complex real Element of REAL
(Re ((s . p) * (s))) * (Re ((s . p) * (s))) is ext-real complex real set
Im ((s . p) * (s)) is ext-real complex real Element of REAL
(Im ((s . p) * (s))) ^2 is ext-real complex real Element of REAL
(Im ((s . p) * (s))) * (Im ((s . p) * (s))) is ext-real complex real set
((Re ((s . p) * (s))) ^2) + ((Im ((s . p) * (s))) ^2) is ext-real complex real Element of REAL
sqrt (((Re ((s . p) * (s))) ^2) + ((Im ((s . p) * (s))) ^2)) is ext-real complex real Element of REAL
(abs (s . p)) * (abs (s)) is ext-real complex real Element of REAL
(s1 * (((abs (s)) * (abs (s))) / 2)) / ((abs (s . p)) * (abs (s))) is ext-real complex real Element of REAL
(abs ((s . p) - (s))) / ((abs (s . p)) * (abs (s))) is ext-real complex real Element of REAL
2 " is ext-real positive non negative non zero complex real Element of REAL
(2 ") * ((abs (s)) * (abs (s))) is ext-real complex real Element of REAL
s1 * ((2 ") * ((abs (s)) * (abs (s)))) is ext-real complex real Element of REAL
((abs (s . p)) * (abs (s))) " is ext-real complex real Element of REAL
(s1 * ((2 ") * ((abs (s)) * (abs (s))))) * (((abs (s . p)) * (abs (s))) ") is ext-real complex real Element of REAL
s1 * (2 ") is ext-real complex real Element of REAL
(abs (s)) * (abs (s . p)) is ext-real complex real Element of REAL
((abs (s)) * (abs (s . p))) " is ext-real complex real Element of REAL
((abs (s)) * (abs (s))) * (((abs (s)) * (abs (s . p))) ") is ext-real complex real Element of REAL
(s1 * (2 ")) * (((abs (s)) * (abs (s))) * (((abs (s)) * (abs (s . p))) ")) is ext-real complex real Element of REAL
(abs (s)) " is ext-real complex real Element of REAL
(abs (s . p)) " is ext-real complex real Element of REAL
((abs (s)) ") * ((abs (s . p)) ") is ext-real complex real Element of REAL
((abs (s)) * (abs (s))) * (((abs (s)) ") * ((abs (s . p)) ")) is ext-real complex real Element of REAL
(s1 * (2 ")) * (((abs (s)) * (abs (s))) * (((abs (s)) ") * ((abs (s . p)) "))) is ext-real complex real Element of REAL
(abs (s)) * ((abs (s)) ") is ext-real complex real Element of REAL
(abs (s)) * ((abs (s)) * ((abs (s)) ")) is ext-real complex real Element of REAL
((abs (s)) * ((abs (s)) * ((abs (s)) "))) * ((abs (s . p)) ") is ext-real complex real Element of REAL
(s1 * (2 ")) * (((abs (s)) * ((abs (s)) * ((abs (s)) "))) * ((abs (s . p)) ")) is ext-real complex real Element of REAL
(abs (s)) * 1 is ext-real complex real Element of REAL
((abs (s)) * 1) * ((abs (s . p)) ") is ext-real complex real Element of REAL
(s1 * (2 ")) * (((abs (s)) * 1) * ((abs (s . p)) ")) is ext-real complex real Element of REAL
s1 * ((abs (s)) / 2) is ext-real complex real Element of REAL
(s1 * ((abs (s)) / 2)) * ((abs (s . p)) ") is ext-real complex real Element of REAL
(s1 * ((abs (s)) / 2)) / (abs (s . p)) is ext-real complex real Element of REAL
(s ") . p is ext-real complex real Element of REAL
((s ") . p) - ((s) ") is ext-real complex real Element of REAL
abs (((s ") . p) - ((s) ")) is ext-real complex real Element of REAL
Re (((s ") . p) - ((s) ")) is ext-real complex real Element of REAL
(Re (((s ") . p) - ((s) "))) ^2 is ext-real complex real Element of REAL
(Re (((s ") . p) - ((s) "))) * (Re (((s ") . p) - ((s) "))) is ext-real complex real set
Im (((s ") . p) - ((s) ")) is ext-real complex real Element of REAL
(Im (((s ") . p) - ((s) "))) ^2 is ext-real complex real Element of REAL
(Im (((s ") . p) - ((s) "))) * (Im (((s ") . p) - ((s) "))) is ext-real complex real set
((Re (((s ") . p) - ((s) "))) ^2) + ((Im (((s ") . p) - ((s) "))) ^2) is ext-real complex real Element of REAL
sqrt (((Re (((s ") . p) - ((s) "))) ^2) + ((Im (((s ") . p) - ((s) "))) ^2)) is ext-real complex real Element of REAL
(s . p) " is ext-real complex real Element of REAL
((s . p) ") - ((s) ") is ext-real complex real Element of REAL
abs (((s . p) ") - ((s) ")) is ext-real complex real Element of REAL
Re (((s . p) ") - ((s) ")) is ext-real complex real Element of REAL
(Re (((s . p) ") - ((s) "))) ^2 is ext-real complex real Element of REAL
(Re (((s . p) ") - ((s) "))) * (Re (((s . p) ") - ((s) "))) is ext-real complex real set
Im (((s . p) ") - ((s) ")) is ext-real complex real Element of REAL
(Im (((s . p) ") - ((s) "))) ^2 is ext-real complex real Element of REAL
(Im (((s . p) ") - ((s) "))) * (Im (((s . p) ") - ((s) "))) is ext-real complex real set
((Re (((s . p) ") - ((s) "))) ^2) + ((Im (((s . p) ") - ((s) "))) ^2) is ext-real complex real Element of REAL
sqrt (((Re (((s . p) ") - ((s) "))) ^2) + ((Im (((s . p) ") - ((s) "))) ^2)) is ext-real complex real Element of REAL
(s1 * ((abs (s)) / 2)) / ((abs (s)) / 2) is ext-real complex real Element of REAL
((abs (s)) / 2) " is ext-real complex real Element of REAL
(s1 * ((abs (s)) / 2)) * (((abs (s)) / 2) ") is ext-real complex real Element of REAL
((abs (s)) / 2) * (((abs (s)) / 2) ") is ext-real complex real Element of REAL
s1 * (((abs (s)) / 2) * (((abs (s)) / 2) ")) is ext-real complex real Element of REAL
s1 * 1 is ext-real complex real Element of REAL
s is non zero Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K11(K12(NAT,REAL))
s1 is non zero Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K11(K12(NAT,REAL))
(s1) is ext-real complex real Element of REAL
s /" s1 is non zero Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K11(K12(NAT,REAL))
s1 " is Relation-like NAT -defined Function-like V26( NAT ) complex-valued ext-real-valued real-valued set
s (#) (s1 ") is Relation-like NAT -defined Function-like V26( NAT ) complex-valued ext-real-valued real-valued set
s1 " is non zero Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K11(K12(NAT,REAL))
s is non zero Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K11(K12(NAT,REAL))
(s) is ext-real complex real Element of REAL
s1 is non zero Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K11(K12(NAT,REAL))
(s1) is ext-real complex real Element of REAL
s /" s1 is non zero Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K11(K12(NAT,REAL))
s1 " is Relation-like NAT -defined Function-like V26( NAT ) complex-valued ext-real-valued real-valued set
s (#) (s1 ") is Relation-like NAT -defined Function-like V26( NAT ) complex-valued ext-real-valued real-valued set
((s /" s1)) is ext-real complex real Element of REAL
(s) / (s1) is ext-real complex real Element of REAL
s1 " is non zero Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K11(K12(NAT,REAL))
s (#) (s1 ") is non zero Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K11(K12(NAT,REAL))
((s (#) (s1 "))) is ext-real complex real Element of REAL
((s1 ")) is ext-real complex real Element of REAL
(s) * ((s1 ")) is ext-real complex real Element of REAL
(s1) " is ext-real complex real Element of REAL
(s) * ((s1) ") is ext-real complex real Element of REAL
s is non zero Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K11(K12(NAT,REAL))
(s) is ext-real complex real Element of REAL
s1 is non zero Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K11(K12(NAT,REAL))
s (#) s1 is non zero Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K11(K12(NAT,REAL))
s1 is ext-real complex real Element of REAL
w is ext-real complex real Element of REAL
w is ext-real complex real set
p is ext-real complex real set
w / p is ext-real complex real Element of COMPLEX
n is ext-real epsilon-transitive epsilon-connected ordinal natural complex real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
n is ext-real epsilon-transitive epsilon-connected ordinal natural complex real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
m is ext-real epsilon-transitive epsilon-connected ordinal natural complex real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
(s (#) s1) . m is ext-real complex real Element of REAL
((s (#) s1) . m) - w is ext-real complex real Element of REAL
abs (((s (#) s1) . m) - w) is ext-real complex real Element of REAL
Re (((s (#) s1) . m) - w) is ext-real complex real Element of REAL
(Re (((s (#) s1) . m) - w)) ^2 is ext-real complex real Element of REAL
(Re (((s (#) s1) . m) - w)) * (Re (((s (#) s1) . m) - w)) is ext-real complex real set
Im (((s (#) s1) . m) - w) is ext-real complex real Element of REAL
(Im (((s (#) s1) . m) - w)) ^2 is ext-real complex real Element of REAL
(Im (((s (#) s1) . m) - w)) * (Im (((s (#) s1) . m) - w)) is ext-real complex real set
((Re (((s (#) s1) . m) - w)) ^2) + ((Im (((s (#) s1) . m) - w)) ^2) is ext-real complex real Element of REAL
sqrt (((Re (((s (#) s1) . m) - w)) ^2) + ((Im (((s (#) s1) . m) - w)) ^2)) is ext-real complex real Element of REAL
s . m is ext-real complex real Element of REAL
abs (s . m) is ext-real complex real Element of REAL
Re (s . m) is ext-real complex real Element of REAL
(Re (s . m)) ^2 is ext-real complex real Element of REAL
(Re (s . m)) * (Re (s . m)) is ext-real complex real set
Im (s . m) is ext-real complex real Element of REAL
(Im (s . m)) ^2 is ext-real complex real Element of REAL
(Im (s . m)) * (Im (s . m)) is ext-real complex real set
((Re (s . m)) ^2) + ((Im (s . m)) ^2) is ext-real complex real Element of REAL
sqrt (((Re (s . m)) ^2) + ((Im (s . m)) ^2)) is ext-real complex real Element of REAL
(s . m) - 0 is ext-real complex real Element of REAL
abs ((s . m) - 0) is ext-real complex real Element of REAL
Re ((s . m) - 0) is ext-real complex real Element of REAL
(Re ((s . m) - 0)) ^2 is ext-real complex real Element of REAL
(Re ((s . m) - 0)) * (Re ((s . m) - 0)) is ext-real complex real set
Im ((s . m) - 0) is ext-real complex real Element of REAL
(Im ((s . m) - 0)) ^2 is ext-real complex real Element of REAL
(Im ((s . m) - 0)) * (Im ((s . m) - 0)) is ext-real complex real set
((Re ((s . m) - 0)) ^2) + ((Im ((s . m) - 0)) ^2) is ext-real complex real Element of REAL
sqrt (((Re ((s . m) - 0)) ^2) + ((Im ((s . m) - 0)) ^2)) is ext-real complex real Element of REAL
s1 . m is ext-real complex real Element of REAL
(s . m) * (s1 . m) is ext-real complex real Element of REAL
((s . m) * (s1 . m)) - 0 is ext-real complex real Element of REAL
abs (((s . m) * (s1 . m)) - 0) is ext-real complex real Element of REAL
Re (((s . m) * (s1 . m)) - 0) is ext-real complex real Element of REAL
(Re (((s . m) * (s1 . m)) - 0)) ^2 is ext-real complex real Element of REAL
(Re (((s . m) * (s1 . m)) - 0)) * (Re (((s . m) * (s1 . m)) - 0)) is ext-real complex real set
Im (((s . m) * (s1 . m)) - 0) is ext-real complex real Element of REAL
(Im (((s . m) * (s1 . m)) - 0)) ^2 is ext-real complex real Element of REAL
(Im (((s . m) * (s1 . m)) - 0)) * (Im (((s . m) * (s1 . m)) - 0)) is ext-real complex real set
((Re (((s . m) * (s1 . m)) - 0)) ^2) + ((Im (((s . m) * (s1 . m)) - 0)) ^2) is ext-real complex real Element of REAL
sqrt (((Re (((s . m) * (s1 . m)) - 0)) ^2) + ((Im (((s . m) * (s1 . m)) - 0)) ^2)) is ext-real complex real Element of REAL
abs (s1 . m) is ext-real complex real Element of REAL
Re (s1 . m) is ext-real complex real Element of REAL
(Re (s1 . m)) ^2 is ext-real complex real Element of REAL
(Re (s1 . m)) * (Re (s1 . m)) is ext-real complex real set
Im (s1 . m) is ext-real complex real Element of REAL
(Im (s1 . m)) ^2 is ext-real complex real Element of REAL
(Im (s1 . m)) * (Im (s1 . m)) is ext-real complex real set
((Re (s1 . m)) ^2) + ((Im (s1 . m)) ^2) is ext-real complex real Element of REAL
sqrt (((Re (s1 . m)) ^2) + ((Im (s1 . m)) ^2)) is ext-real complex real Element of REAL
(abs (s . m)) * (abs (s1 . m)) is ext-real complex real Element of REAL
(w / p) * p is ext-real complex real set
p " is ext-real complex real set
w * (p ") is ext-real complex real set
(w * (p ")) * p is ext-real complex real set
(p ") * p is ext-real complex real set
w * ((p ") * p) is ext-real complex real set
w * 1 is ext-real complex real Element of REAL
(w / p) * (abs (s1 . m)) is ext-real complex real Element of REAL
s is non zero Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K11(K12(NAT,REAL))
(s) is ext-real complex real Element of REAL
s1 is non zero Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K11(K12(NAT,REAL))
s (#) s1 is non zero Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K11(K12(NAT,REAL))
((s (#) s1)) is ext-real complex real Element of REAL
s1 is ext-real complex real set
w is ext-real complex real set
s1 / w is ext-real complex real Element of COMPLEX
w is ext-real epsilon-transitive epsilon-connected ordinal natural complex real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
p is ext-real epsilon-transitive epsilon-connected ordinal natural complex real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
n is ext-real epsilon-transitive epsilon-connected ordinal natural complex real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
s . n is ext-real complex real Element of REAL
(s . n) - 0 is ext-real complex real Element of REAL
abs ((s . n) - 0) is ext-real complex real Element of REAL
Re ((s . n) - 0) is ext-real complex real Element of REAL
(Re ((s . n) - 0)) ^2 is ext-real complex real Element of REAL
(Re ((s . n) - 0)) * (Re ((s . n) - 0)) is ext-real complex real set
Im ((s . n) - 0) is ext-real complex real Element of REAL
(Im ((s . n) - 0)) ^2 is ext-real complex real Element of REAL
(Im ((s . n) - 0)) * (Im ((s . n) - 0)) is ext-real complex real set
((Re ((s . n) - 0)) ^2) + ((Im ((s . n) - 0)) ^2) is ext-real complex real Element of REAL
sqrt (((Re ((s . n) - 0)) ^2) + ((Im ((s . n) - 0)) ^2)) is ext-real complex real Element of REAL
(s (#) s1) . n is ext-real complex real Element of REAL
((s (#) s1) . n) - 0 is ext-real complex real Element of REAL
abs (((s (#) s1) . n) - 0) is ext-real complex real Element of REAL
Re (((s (#) s1) . n) - 0) is ext-real complex real Element of REAL
(Re (((s (#) s1) . n) - 0)) ^2 is ext-real complex real Element of REAL
(Re (((s (#) s1) . n) - 0)) * (Re (((s (#) s1) . n) - 0)) is ext-real complex real set
Im (((s (#) s1) . n) - 0) is ext-real complex real Element of REAL
(Im (((s (#) s1) . n) - 0)) ^2 is ext-real complex real Element of REAL
(Im (((s (#) s1) . n) - 0)) * (Im (((s (#) s1) . n) - 0)) is ext-real complex real set
((Re (((s (#) s1) . n) - 0)) ^2) + ((Im (((s (#) s1) . n) - 0)) ^2) is ext-real complex real Element of REAL
sqrt (((Re (((s (#) s1) . n) - 0)) ^2) + ((Im (((s (#) s1) . n) - 0)) ^2)) is ext-real complex real Element of REAL
s1 . n is ext-real complex real Element of REAL
(s . n) * (s1 . n) is ext-real complex real Element of REAL
((s . n) * (s1 . n)) - 0 is ext-real complex real Element of REAL
abs (((s . n) * (s1 . n)) - 0) is ext-real complex real Element of REAL
Re (((s . n) * (s1 . n)) - 0) is ext-real complex real Element of REAL
(Re (((s . n) * (s1 . n)) - 0)) ^2 is ext-real complex real Element of REAL
(Re (((s . n) * (s1 . n)) - 0)) * (Re (((s . n) * (s1 . n)) - 0)) is ext-real complex real set
Im (((s . n) * (s1 . n)) - 0) is ext-real complex real Element of REAL
(Im (((s . n) * (s1 . n)) - 0)) ^2 is ext-real complex real Element of REAL
(Im (((s . n) * (s1 . n)) - 0)) * (Im (((s . n) * (s1 . n)) - 0)) is ext-real complex real set
((Re (((s . n) * (s1 . n)) - 0)) ^2) + ((Im (((s . n) * (s1 . n)) - 0)) ^2) is ext-real complex real Element of REAL
sqrt (((Re (((s . n) * (s1 . n)) - 0)) ^2) + ((Im (((s . n) * (s1 . n)) - 0)) ^2)) is ext-real complex real Element of REAL
abs (s . n) is ext-real complex real Element of REAL
Re (s . n) is ext-real complex real Element of REAL
(Re (s . n)) ^2 is ext-real complex real Element of REAL
(Re (s . n)) * (Re (s . n)) is ext-real complex real set
Im (s . n) is ext-real complex real Element of REAL
(Im (s . n)) ^2 is ext-real complex real Element of REAL
(Im (s . n)) * (Im (s . n)) is ext-real complex real set
((Re (s . n)) ^2) + ((Im (s . n)) ^2) is ext-real complex real Element of REAL
sqrt (((Re (s . n)) ^2) + ((Im (s . n)) ^2)) is ext-real complex real Element of REAL
abs (s1 . n) is ext-real complex real Element of REAL
Re (s1 . n) is ext-real complex real Element of REAL
(Re (s1 . n)) ^2 is ext-real complex real Element of REAL
(Re (s1 . n)) * (Re (s1 . n)) is ext-real complex real set
Im (s1 . n) is ext-real complex real Element of REAL
(Im (s1 . n)) ^2 is ext-real complex real Element of REAL
(Im (s1 . n)) * (Im (s1 . n)) is ext-real complex real set
((Re (s1 . n)) ^2) + ((Im (s1 . n)) ^2) is ext-real complex real Element of REAL
sqrt (((Re (s1 . n)) ^2) + ((Im (s1 . n)) ^2)) is ext-real complex real Element of REAL
(abs (s . n)) * (abs (s1 . n)) is ext-real complex real Element of REAL
(s1 / w) * w is ext-real complex real set
w " is ext-real complex real set
s1 * (w ") is ext-real complex real set
(s1 * (w ")) * w is ext-real complex real set
(w ") * w is ext-real complex real set
s1 * ((w ") * w) is ext-real complex real set
s1 * 1 is ext-real complex real Element of REAL
(s1 / w) * (abs (s1 . n)) is ext-real complex real Element of REAL
s is non zero Relation-like NAT -defined COMPLEX -valued Function-like V26( NAT ) V30( NAT , COMPLEX ) complex-valued bounded convergent Element of K11(K12(NAT,COMPLEX))
|.s.| is non zero Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K11(K12(NAT,REAL))
s1 is complex Element of COMPLEX
|.s1.| is ext-real complex real Element of REAL
Re s1 is ext-real complex real Element of REAL
(Re s1) ^2 is ext-real complex real Element of REAL
(Re s1) * (Re s1) is ext-real complex real set
Im s1 is ext-real complex real Element of REAL
(Im s1) ^2 is ext-real complex real Element of REAL
(Im s1) * (Im s1) is ext-real complex real set
((Re s1) ^2) + ((Im s1) ^2) is ext-real complex real Element of REAL
sqrt (((Re s1) ^2) + ((Im s1) ^2)) is ext-real complex real Element of REAL
s1 is ext-real complex real set
w is ext-real epsilon-transitive epsilon-connected ordinal natural complex real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
w is ext-real epsilon-transitive epsilon-connected ordinal natural complex real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
|.s.| . w is ext-real complex real Element of REAL
(|.s.| . w) - |.s1.| is ext-real complex real Element of REAL
abs ((|.s.| . w) - |.s1.|) is ext-real complex real Element of REAL
Re ((|.s.| . w) - |.s1.|) is ext-real complex real Element of REAL
(Re ((|.s.| . w) - |.s1.|)) ^2 is ext-real complex real Element of REAL
(Re ((|.s.| . w) - |.s1.|)) * (Re ((|.s.| . w) - |.s1.|)) is ext-real complex real set
Im ((|.s.| . w) - |.s1.|) is ext-real complex real Element of REAL
(Im ((|.s.| . w) - |.s1.|)) ^2 is ext-real complex real Element of REAL
(Im ((|.s.| . w) - |.s1.|)) * (Im ((|.s.| . w) - |.s1.|)) is ext-real complex real set
((Re ((|.s.| . w) - |.s1.|)) ^2) + ((Im ((|.s.| . w) - |.s1.|)) ^2) is ext-real complex real Element of REAL
sqrt (((Re ((|.s.| . w) - |.s1.|)) ^2) + ((Im ((|.s.| . w) - |.s1.|)) ^2)) is ext-real complex real Element of REAL
s . w is complex set
(s . w) - s1 is complex set
|.((s . w) - s1).| is ext-real complex real Element of REAL
Re ((s . w) - s1) is ext-real complex real Element of REAL
(Re ((s . w) - s1)) ^2 is ext-real complex real Element of REAL
(Re ((s . w) - s1)) * (Re ((s . w) - s1)) is ext-real complex real set
Im ((s . w) - s1) is ext-real complex real Element of REAL
(Im ((s . w) - s1)) ^2 is ext-real complex real Element of REAL
(Im ((s . w) - s1)) * (Im ((s . w) - s1)) is ext-real complex real set
((Re ((s . w) - s1)) ^2) + ((Im ((s . w) - s1)) ^2) is ext-real complex real Element of REAL
sqrt (((Re ((s . w) - s1)) ^2) + ((Im ((s . w) - s1)) ^2)) is ext-real complex real Element of REAL
s1 + |.((s . w) - s1).| is ext-real complex real Element of REAL
|.(s . w).| is ext-real complex real Element of REAL
Re (s . w) is ext-real complex real Element of REAL
(Re (s . w)) ^2 is ext-real complex real Element of REAL
(Re (s . w)) * (Re (s . w)) is ext-real complex real set
Im (s . w) is ext-real complex real Element of REAL
(Im (s . w)) ^2 is ext-real complex real Element of REAL
(Im (s . w)) * (Im (s . w)) is ext-real complex real set
((Re (s . w)) ^2) + ((Im (s . w)) ^2) is ext-real complex real Element of REAL
sqrt (((Re (s . w)) ^2) + ((Im (s . w)) ^2)) is ext-real complex real Element of REAL
|.(s . w).| - |.s1.| is ext-real complex real Element of REAL
abs (|.(s . w).| - |.s1.|) is ext-real complex real Element of REAL
Re (|.(s . w).| - |.s1.|) is ext-real complex real Element of REAL
(Re (|.(s . w).| - |.s1.|)) ^2 is ext-real complex real Element of REAL
(Re (|.(s . w).| - |.s1.|)) * (Re (|.(s . w).| - |.s1.|)) is ext-real complex real set
Im (|.(s . w).| - |.s1.|) is ext-real complex real Element of REAL
(Im (|.(s . w).| - |.s1.|)) ^2 is ext-real complex real Element of REAL
(Im (|.(s . w).| - |.s1.|)) * (Im (|.(s . w).| - |.s1.|)) is ext-real complex real set
((Re (|.(s . w).| - |.s1.|)) ^2) + ((Im (|.(s . w).| - |.s1.|)) ^2) is ext-real complex real Element of REAL
sqrt (((Re (|.(s . w).| - |.s1.|)) ^2) + ((Im (|.(s . w).| - |.s1.|)) ^2)) is ext-real complex real Element of REAL
(abs (|.(s . w).| - |.s1.|)) + |.((s . w) - s1).| is ext-real complex real Element of REAL
(s1 + |.((s . w) - s1).|) - |.((s . w) - s1).| is ext-real complex real Element of REAL
((abs (|.(s . w).| - |.s1.|)) + |.((s . w) - s1).|) - |.((s . w) - s1).| is ext-real complex real Element of REAL
s1 is non zero Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K11(K12(NAT,REAL))
s is non zero Relation-like NAT -defined COMPLEX -valued Function-like V26( NAT ) V30( NAT , COMPLEX ) complex-valued Element of K11(K12(NAT,COMPLEX))
|.s.| is non zero Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K11(K12(NAT,REAL))
(|.s.|) is ext-real complex real Element of REAL
lim s is complex Element of COMPLEX
|.(lim s).| is ext-real complex real Element of REAL
Re (lim s) is ext-real complex real Element of REAL
(Re (lim s)) ^2 is ext-real complex real Element of REAL
(Re (lim s)) * (Re (lim s)) is ext-real complex real set
Im (lim s) is ext-real complex real Element of REAL
(Im (lim s)) ^2 is ext-real complex real Element of REAL
(Im (lim s)) * (Im (lim s)) is ext-real complex real set
((Re (lim s)) ^2) + ((Im (lim s)) ^2) is ext-real complex real Element of REAL
sqrt (((Re (lim s)) ^2) + ((Im (lim s)) ^2)) is ext-real complex real Element of REAL
s1 is non zero Relation-like NAT -defined COMPLEX -valued Function-like V26( NAT ) V30( NAT , COMPLEX ) complex-valued bounded convergent Element of K11(K12(NAT,COMPLEX))
|.s1.| is non zero Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued bounded convergent () () Element of K11(K12(NAT,REAL))
w is non zero Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K11(K12(NAT,REAL))
p is ext-real complex real set
n is ext-real epsilon-transitive epsilon-connected ordinal natural complex real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
n is ext-real epsilon-transitive epsilon-connected ordinal natural complex real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
m is ext-real epsilon-transitive epsilon-connected ordinal natural complex real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
s . m is complex set
(s . m) - (lim s) is complex set
|.((s . m) - (lim s)).| is ext-real complex real Element of REAL
Re ((s . m) - (lim s)) is ext-real complex real Element of REAL
(Re ((s . m) - (lim s))) ^2 is ext-real complex real Element of REAL
(Re ((s . m) - (lim s))) * (Re ((s . m) - (lim s))) is ext-real complex real set
Im ((s . m) - (lim s)) is ext-real complex real Element of REAL
(Im ((s . m) - (lim s))) ^2 is ext-real complex real Element of REAL
(Im ((s . m) - (lim s))) * (Im ((s . m) - (lim s))) is ext-real complex real set
((Re ((s . m) - (lim s))) ^2) + ((Im ((s . m) - (lim s))) ^2) is ext-real complex real Element of REAL
sqrt (((Re ((s . m) - (lim s))) ^2) + ((Im ((s . m) - (lim s))) ^2)) is ext-real complex real Element of REAL
p + |.((s . m) - (lim s)).| is ext-real complex real Element of REAL
|.(s . m).| is ext-real complex real Element of REAL
Re (s . m) is ext-real complex real Element of REAL
(Re (s . m)) ^2 is ext-real complex real Element of REAL
(Re (s . m)) * (Re (s . m)) is ext-real complex real set
Im (s . m) is ext-real complex real Element of REAL
(Im (s . m)) ^2 is ext-real complex real Element of REAL
(Im (s . m)) * (Im (s . m)) is ext-real complex real set
((Re (s . m)) ^2) + ((Im (s . m)) ^2) is ext-real complex real Element of REAL
sqrt (((Re (s . m)) ^2) + ((Im (s . m)) ^2)) is ext-real complex real Element of REAL
|.(s . m).| - |.(lim s).| is ext-real complex real Element of REAL
abs (|.(s . m).| - |.(lim s).|) is ext-real complex real Element of REAL
Re (|.(s . m).| - |.(lim s).|) is ext-real complex real Element of REAL
(Re (|.(s . m).| - |.(lim s).|)) ^2 is ext-real complex real Element of REAL
(Re (|.(s . m).| - |.(lim s).|)) * (Re (|.(s . m).| - |.(lim s).|)) is ext-real complex real set
Im (|.(s . m).| - |.(lim s).|) is ext-real complex real Element of REAL
(Im (|.(s . m).| - |.(lim s).|)) ^2 is ext-real complex real Element of REAL
(Im (|.(s . m).| - |.(lim s).|)) * (Im (|.(s . m).| - |.(lim s).|)) is ext-real complex real set
((Re (|.(s . m).| - |.(lim s).|)) ^2) + ((Im (|.(s . m).| - |.(lim s).|)) ^2) is ext-real complex real Element of REAL
sqrt (((Re (|.(s . m).| - |.(lim s).|)) ^2) + ((Im (|.(s . m).| - |.(lim s).|)) ^2)) is ext-real complex real Element of REAL
(abs (|.(s . m).| - |.(lim s).|)) + |.((s . m) - (lim s)).| is ext-real complex real Element of REAL
(p + |.((s . m) - (lim s)).|) - |.((s . m) - (lim s)).| is ext-real complex real Element of REAL
((abs (|.(s . m).| - |.(lim s).|)) + |.((s . m) - (lim s)).|) - |.((s . m) - (lim s)).| is ext-real complex real Element of REAL
|.s.| . m is ext-real complex real Element of REAL
w is ext-real complex real Element of REAL
(|.s.| . m) - w is ext-real complex real Element of REAL
abs ((|.s.| . m) - w) is ext-real complex real Element of REAL
Re ((|.s.| . m) - w) is ext-real complex real Element of REAL
(Re ((|.s.| . m) - w)) ^2 is ext-real complex real Element of REAL
(Re ((|.s.| . m) - w)) * (Re ((|.s.| . m) - w)) is ext-real complex real set
Im ((|.s.| . m) - w) is ext-real complex real Element of REAL
(Im ((|.s.| . m) - w)) ^2 is ext-real complex real Element of REAL
(Im ((|.s.| . m) - w)) * (Im ((|.s.| . m) - w)) is ext-real complex real set
((Re ((|.s.| . m) - w)) ^2) + ((Im ((|.s.| . m) - w)) ^2) is ext-real complex real Element of REAL
sqrt (((Re ((|.s.| . m) - w)) ^2) + ((Im ((|.s.| . m) - w)) ^2)) is ext-real complex real Element of REAL
s is non zero Relation-like NAT -defined COMPLEX -valued Function-like V26( NAT ) V30( NAT , COMPLEX ) complex-valued bounded convergent Element of K11(K12(NAT,COMPLEX))
s1 is non zero Relation-like NAT -defined COMPLEX -valued Function-like V26( NAT ) V30( NAT , COMPLEX ) complex-valued bounded convergent Element of K11(K12(NAT,COMPLEX))
s + s1 is non zero Relation-like NAT -defined COMPLEX -valued Function-like V26( NAT ) V30( NAT , COMPLEX ) complex-valued bounded convergent Element of K11(K12(NAT,COMPLEX))
|.(s + s1).| is non zero Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued bounded convergent () () Element of K11(K12(NAT,REAL))
(|.(s + s1).|) is ext-real complex real Element of REAL
lim s is complex Element of COMPLEX
lim s1 is complex Element of COMPLEX
(lim s) + (lim s1) is complex Element of COMPLEX
|.((lim s) + (lim s1)).| is ext-real complex real Element of REAL
Re ((lim s) + (lim s1)) is ext-real complex real Element of REAL
(Re ((lim s) + (lim s1))) ^2 is ext-real complex real Element of REAL
(Re ((lim s) + (lim s1))) * (Re ((lim s) + (lim s1))) is ext-real complex real set
Im ((lim s) + (lim s1)) is ext-real complex real Element of REAL
(Im ((lim s) + (lim s1))) ^2 is ext-real complex real Element of REAL
(Im ((lim s) + (lim s1))) * (Im ((lim s) + (lim s1))) is ext-real complex real set
((Re ((lim s) + (lim s1))) ^2) + ((Im ((lim s) + (lim s1))) ^2) is ext-real complex real Element of REAL
sqrt (((Re ((lim s) + (lim s1))) ^2) + ((Im ((lim s) + (lim s1))) ^2)) is ext-real complex real Element of REAL
lim (s + s1) is complex Element of COMPLEX
|.(lim (s + s1)).| is ext-real complex real Element of REAL
Re (lim (s + s1)) is ext-real complex real Element of REAL
(Re (lim (s + s1))) ^2 is ext-real complex real Element of REAL
(Re (lim (s + s1))) * (Re (lim (s + s1))) is ext-real complex real set
Im (lim (s + s1)) is ext-real complex real Element of REAL
(Im (lim (s + s1))) ^2 is ext-real complex real Element of REAL
(Im (lim (s + s1))) * (Im (lim (s + s1))) is ext-real complex real set
((Re (lim (s + s1))) ^2) + ((Im (lim (s + s1))) ^2) is ext-real complex real Element of REAL
sqrt (((Re (lim (s + s1))) ^2) + ((Im (lim (s + s1))) ^2)) is ext-real complex real Element of REAL
s is ext-real complex real set
|.s.| is ext-real complex real Element of REAL
Re s is ext-real complex real Element of REAL
(Re s) ^2 is ext-real complex real Element of REAL
(Re s) * (Re s) is ext-real complex real set
Im s is ext-real complex real Element of REAL
(Im s) ^2 is ext-real complex real Element of REAL
(Im s) * (Im s) is ext-real complex real set
((Re s) ^2) + ((Im s) ^2) is ext-real complex real Element of REAL
sqrt (((Re s) ^2) + ((Im s) ^2)) is ext-real complex real Element of REAL
s1 is non zero Relation-like NAT -defined COMPLEX -valued Function-like V26( NAT ) V30( NAT , COMPLEX ) complex-valued bounded convergent Element of K11(K12(NAT,COMPLEX))
s (#) s1 is non zero Relation-like NAT -defined COMPLEX -valued Function-like V26( NAT ) V30( NAT , COMPLEX ) complex-valued bounded convergent Element of K11(K12(NAT,COMPLEX))
|.(s (#) s1).| is non zero Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued bounded convergent () () Element of K11(K12(NAT,REAL))
(|.(s (#) s1).|) is ext-real complex real Element of REAL
lim s1 is complex Element of COMPLEX
|.(lim s1).| is ext-real complex real Element of REAL
Re (lim s1) is ext-real complex real Element of REAL
(Re (lim s1)) ^2 is ext-real complex real Element of REAL
(Re (lim s1)) * (Re (lim s1)) is ext-real complex real set
Im (lim s1) is ext-real complex real Element of REAL
(Im (lim s1)) ^2 is ext-real complex real Element of REAL
(Im (lim s1)) * (Im (lim s1)) is ext-real complex real set
((Re (lim s1)) ^2) + ((Im (lim s1)) ^2) is ext-real complex real Element of REAL
sqrt (((Re (lim s1)) ^2) + ((Im (lim s1)) ^2)) is ext-real complex real Element of REAL
|.s.| * |.(lim s1).| is ext-real complex real Element of REAL
lim (s (#) s1) is complex Element of COMPLEX
|.(lim (s (#) s1)).| is ext-real complex real Element of REAL
Re (lim (s (#) s1)) is ext-real complex real Element of REAL
(Re (lim (s (#) s1))) ^2 is ext-real complex real Element of REAL
(Re (lim (s (#) s1))) * (Re (lim (s (#) s1))) is ext-real complex real set
Im (lim (s (#) s1)) is ext-real complex real Element of REAL
(Im (lim (s (#) s1))) ^2 is ext-real complex real Element of REAL
(Im (lim (s (#) s1))) * (Im (lim (s (#) s1))) is ext-real complex real set
((Re (lim (s (#) s1))) ^2) + ((Im (lim (s (#) s1))) ^2) is ext-real complex real Element of REAL
sqrt (((Re (lim (s (#) s1))) ^2) + ((Im (lim (s (#) s1))) ^2)) is ext-real complex real Element of REAL
s * (lim s1) is complex set
|.(s * (lim s1)).| is ext-real complex real Element of REAL
Re (s * (lim s1)) is ext-real complex real Element of REAL
(Re (s * (lim s1))) ^2 is ext-real complex real Element of REAL
(Re (s * (lim s1))) * (Re (s * (lim s1))) is ext-real complex real set
Im (s * (lim s1)) is ext-real complex real Element of REAL
(Im (s * (lim s1))) ^2 is ext-real complex real Element of REAL
(Im (s * (lim s1))) * (Im (s * (lim s1))) is ext-real complex real set
((Re (s * (lim s1))) ^2) + ((Im (s * (lim s1))) ^2) is ext-real complex real Element of REAL
sqrt (((Re (s * (lim s1))) ^2) + ((Im (s * (lim s1))) ^2)) is ext-real complex real Element of REAL
s is non zero Relation-like NAT -defined COMPLEX -valued Function-like V26( NAT ) V30( NAT , COMPLEX ) complex-valued bounded convergent Element of K11(K12(NAT,COMPLEX))
- s is non zero Relation-like NAT -defined COMPLEX -valued Function-like V26( NAT ) V30( NAT , COMPLEX ) complex-valued bounded convergent Element of K11(K12(NAT,COMPLEX))
(- 1) (#) s is Relation-like NAT -defined Function-like V26( NAT ) complex-valued set
|.(- s).| is non zero Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued bounded convergent () () Element of K11(K12(NAT,REAL))
(|.(- s).|) is ext-real complex real Element of REAL
lim s is complex Element of COMPLEX
|.(lim s).| is ext-real complex real Element of REAL
Re (lim s) is ext-real complex real Element of REAL
(Re (lim s)) ^2 is ext-real complex real Element of REAL
(Re (lim s)) * (Re (lim s)) is ext-real complex real set
Im (lim s) is ext-real complex real Element of REAL
(Im (lim s)) ^2 is ext-real complex real Element of REAL
(Im (lim s)) * (Im (lim s)) is ext-real complex real set
((Re (lim s)) ^2) + ((Im (lim s)) ^2) is ext-real complex real Element of REAL
sqrt (((Re (lim s)) ^2) + ((Im (lim s)) ^2)) is ext-real complex real Element of REAL
lim (- s) is complex Element of COMPLEX
|.(lim (- s)).| is ext-real complex real Element of REAL
Re (lim (- s)) is ext-real complex real Element of REAL
(Re (lim (- s))) ^2 is ext-real complex real Element of REAL
(Re (lim (- s))) * (Re (lim (- s))) is ext-real complex real set
Im (lim (- s)) is ext-real complex real Element of REAL
(Im (lim (- s))) ^2 is ext-real complex real Element of REAL
(Im (lim (- s))) * (Im (lim (- s))) is ext-real complex real set
((Re (lim (- s))) ^2) + ((Im (lim (- s))) ^2) is ext-real complex real Element of REAL
sqrt (((Re (lim (- s))) ^2) + ((Im (lim (- s))) ^2)) is ext-real complex real Element of REAL
- (lim s) is complex Element of COMPLEX
|.(- (lim s)).| is ext-real complex real Element of REAL
Re (- (lim s)) is ext-real complex real Element of REAL
(Re (- (lim s))) ^2 is ext-real complex real Element of REAL
(Re (- (lim s))) * (Re (- (lim s))) is ext-real complex real set
Im (- (lim s)) is ext-real complex real Element of REAL
(Im (- (lim s))) ^2 is ext-real complex real Element of REAL
(Im (- (lim s))) * (Im (- (lim s))) is ext-real complex real set
((Re (- (lim s))) ^2) + ((Im (- (lim s))) ^2) is ext-real complex real Element of REAL
sqrt (((Re (- (lim s))) ^2) + ((Im (- (lim s))) ^2)) is ext-real complex real Element of REAL
s is non zero Relation-like NAT -defined COMPLEX -valued Function-like V26( NAT ) V30( NAT , COMPLEX ) complex-valued bounded convergent Element of K11(K12(NAT,COMPLEX))
s1 is non zero Relation-like NAT -defined COMPLEX -valued Function-like V26( NAT ) V30( NAT , COMPLEX ) complex-valued bounded convergent Element of K11(K12(NAT,COMPLEX))
s - s1 is non zero Relation-like NAT -defined COMPLEX -valued Function-like V26( NAT ) V30( NAT , COMPLEX ) complex-valued bounded convergent Element of K11(K12(NAT,COMPLEX))
- s1 is Relation-like NAT -defined Function-like V26( NAT ) complex-valued set
(- 1) (#) s1 is Relation-like NAT -defined Function-like V26( NAT ) complex-valued set
s + (- s1) is Relation-like NAT -defined Function-like V26( NAT ) complex-valued set
|.(s - s1).| is non zero Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued bounded convergent () () Element of K11(K12(NAT,REAL))
(|.(s - s1).|) is ext-real complex real Element of REAL
lim s is complex Element of COMPLEX
lim s1 is complex Element of COMPLEX
(lim s) - (lim s1) is complex Element of COMPLEX
|.((lim s) - (lim s1)).| is ext-real complex real Element of REAL
Re ((lim s) - (lim s1)) is ext-real complex real Element of REAL
(Re ((lim s) - (lim s1))) ^2 is ext-real complex real Element of REAL
(Re ((lim s) - (lim s1))) * (Re ((lim s) - (lim s1))) is ext-real complex real set
Im ((lim s) - (lim s1)) is ext-real complex real Element of REAL
(Im ((lim s) - (lim s1))) ^2 is ext-real complex real Element of REAL
(Im ((lim s) - (lim s1))) * (Im ((lim s) - (lim s1))) is ext-real complex real set
((Re ((lim s) - (lim s1))) ^2) + ((Im ((lim s) - (lim s1))) ^2) is ext-real complex real Element of REAL
sqrt (((Re ((lim s) - (lim s1))) ^2) + ((Im ((lim s) - (lim s1))) ^2)) is ext-real complex real Element of REAL
lim (s - s1) is complex Element of COMPLEX
|.(lim (s - s1)).| is ext-real complex real Element of REAL
Re (lim (s - s1)) is ext-real complex real Element of REAL
(Re (lim (s - s1))) ^2 is ext-real complex real Element of REAL
(Re (lim (s - s1))) * (Re (lim (s - s1))) is ext-real complex real set
Im (lim (s - s1)) is ext-real complex real Element of REAL
(Im (lim (s - s1))) ^2 is ext-real complex real Element of REAL
(Im (lim (s - s1))) * (Im (lim (s - s1))) is ext-real complex real set
((Re (lim (s - s1))) ^2) + ((Im (lim (s - s1))) ^2) is ext-real complex real Element of REAL
sqrt (((Re (lim (s - s1))) ^2) + ((Im (lim (s - s1))) ^2)) is ext-real complex real Element of REAL
s is non zero Relation-like NAT -defined COMPLEX -valued Function-like V26( NAT ) V30( NAT , COMPLEX ) complex-valued bounded convergent Element of K11(K12(NAT,COMPLEX))
s1 is non zero Relation-like NAT -defined COMPLEX -valued Function-like V26( NAT ) V30( NAT , COMPLEX ) complex-valued bounded convergent Element of K11(K12(NAT,COMPLEX))
s (#) s1 is non zero Relation-like NAT -defined COMPLEX -valued Function-like V26( NAT ) V30( NAT , COMPLEX ) complex-valued bounded convergent Element of K11(K12(NAT,COMPLEX))
|.(s (#) s1).| is non zero Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued bounded convergent () () Element of K11(K12(NAT,REAL))
(|.(s (#) s1).|) is ext-real complex real Element of REAL
lim s is complex Element of COMPLEX
|.(lim s).| is ext-real complex real Element of REAL
Re (lim s) is ext-real complex real Element of REAL
(Re (lim s)) ^2 is ext-real complex real Element of REAL
(Re (lim s)) * (Re (lim s)) is ext-real complex real set
Im (lim s) is ext-real complex real Element of REAL
(Im (lim s)) ^2 is ext-real complex real Element of REAL
(Im (lim s)) * (Im (lim s)) is ext-real complex real set
((Re (lim s)) ^2) + ((Im (lim s)) ^2) is ext-real complex real Element of REAL
sqrt (((Re (lim s)) ^2) + ((Im (lim s)) ^2)) is ext-real complex real Element of REAL
lim s1 is complex Element of COMPLEX
|.(lim s1).| is ext-real complex real Element of REAL
Re (lim s1) is ext-real complex real Element of REAL
(Re (lim s1)) ^2 is ext-real complex real Element of REAL
(Re (lim s1)) * (Re (lim s1)) is ext-real complex real set
Im (lim s1) is ext-real complex real Element of REAL
(Im (lim s1)) ^2 is ext-real complex real Element of REAL
(Im (lim s1)) * (Im (lim s1)) is ext-real complex real set
((Re (lim s1)) ^2) + ((Im (lim s1)) ^2) is ext-real complex real Element of REAL
sqrt (((Re (lim s1)) ^2) + ((Im (lim s1)) ^2)) is ext-real complex real Element of REAL
|.(lim s).| * |.(lim s1).| is ext-real complex real Element of REAL
lim (s (#) s1) is complex Element of COMPLEX
|.(lim (s (#) s1)).| is ext-real complex real Element of REAL
Re (lim (s (#) s1)) is ext-real complex real Element of REAL
(Re (lim (s (#) s1))) ^2 is ext-real complex real Element of REAL
(Re (lim (s (#) s1))) * (Re (lim (s (#) s1))) is ext-real complex real set
Im (lim (s (#) s1)) is ext-real complex real Element of REAL
(Im (lim (s (#) s1))) ^2 is ext-real complex real Element of REAL
(Im (lim (s (#) s1))) * (Im (lim (s (#) s1))) is ext-real complex real set
((Re (lim (s (#) s1))) ^2) + ((Im (lim (s (#) s1))) ^2) is ext-real complex real Element of REAL
sqrt (((Re (lim (s (#) s1))) ^2) + ((Im (lim (s (#) s1))) ^2)) is ext-real complex real Element of REAL
(lim s) * (lim s1) is complex Element of COMPLEX
|.((lim s) * (lim s1)).| is ext-real complex real Element of REAL
Re ((lim s) * (lim s1)) is ext-real complex real Element of REAL
(Re ((lim s) * (lim s1))) ^2 is ext-real complex real Element of REAL
(Re ((lim s) * (lim s1))) * (Re ((lim s) * (lim s1))) is ext-real complex real set
Im ((lim s) * (lim s1)) is ext-real complex real Element of REAL
(Im ((lim s) * (lim s1))) ^2 is ext-real complex real Element of REAL
(Im ((lim s) * (lim s1))) * (Im ((lim s) * (lim s1))) is ext-real complex real set
((Re ((lim s) * (lim s1))) ^2) + ((Im ((lim s) * (lim s1))) ^2) is ext-real complex real Element of REAL
sqrt (((Re ((lim s) * (lim s1))) ^2) + ((Im ((lim s) * (lim s1))) ^2)) is ext-real complex real Element of REAL
s is non zero Relation-like NAT -defined COMPLEX -valued Function-like V26( NAT ) V30( NAT , COMPLEX ) complex-valued Element of K11(K12(NAT,COMPLEX))
lim s is complex Element of COMPLEX
s " is non zero Relation-like NAT -defined COMPLEX -valued Function-like V26( NAT ) V30( NAT , COMPLEX ) complex-valued Element of K11(K12(NAT,COMPLEX))
|.(s ").| is non zero Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K11(K12(NAT,REAL))
(|.(s ").|) is ext-real complex real Element of REAL
|.(lim s).| is ext-real complex real Element of REAL
Re (lim s) is ext-real complex real Element of REAL
(Re (lim s)) ^2 is ext-real complex real Element of REAL
(Re (lim s)) * (Re (lim s)) is ext-real complex real set
Im (lim s) is ext-real complex real Element of REAL
(Im (lim s)) ^2 is ext-real complex real Element of REAL
(Im (lim s)) * (Im (lim s)) is ext-real complex real set
((Re (lim s)) ^2) + ((Im (lim s)) ^2) is ext-real complex real Element of REAL
sqrt (((Re (lim s)) ^2) + ((Im (lim s)) ^2)) is ext-real complex real Element of REAL
|.(lim s).| " is ext-real complex real Element of REAL
lim (s ") is complex Element of COMPLEX
|.(lim (s ")).| is ext-real complex real Element of REAL
Re (lim (s ")) is ext-real complex real Element of REAL
(Re (lim (s "))) ^2 is ext-real complex real Element of REAL
(Re (lim (s "))) * (Re (lim (s "))) is ext-real complex real set
Im (lim (s ")) is ext-real complex real Element of REAL
(Im (lim (s "))) ^2 is ext-real complex real Element of REAL
(Im (lim (s "))) * (Im (lim (s "))) is ext-real complex real set
((Re (lim (s "))) ^2) + ((Im (lim (s "))) ^2) is ext-real complex real Element of REAL
sqrt (((Re (lim (s "))) ^2) + ((Im (lim (s "))) ^2)) is ext-real complex real Element of REAL
(lim s) " is complex Element of COMPLEX
(Re (lim s)) / (((Re (lim s)) ^2) + ((Im (lim s)) ^2)) is ext-real complex real Element of REAL
- (Im (lim s)) is ext-real complex real Element of REAL
(- (Im (lim s))) / (((Re (lim s)) ^2) + ((Im (lim s)) ^2)) is ext-real complex real Element of REAL
((- (Im (lim s))) / (((Re (lim s)) ^2) + ((Im (lim s)) ^2))) * <i> is complex set
((Re (lim s)) / (((Re (lim s)) ^2) + ((Im (lim s)) ^2))) + (((- (Im (lim s))) / (((Re (lim s)) ^2) + ((Im (lim s)) ^2))) * <i>) is complex set
|.((lim s) ").| is ext-real complex real Element of REAL
Re ((lim s) ") is ext-real complex real Element of REAL
(Re ((lim s) ")) ^2 is ext-real complex real Element of REAL
(Re ((lim s) ")) * (Re ((lim s) ")) is ext-real complex real set
Im ((lim s) ") is ext-real complex real Element of REAL
(Im ((lim s) ")) ^2 is ext-real complex real Element of REAL
(Im ((lim s) ")) * (Im ((lim s) ")) is ext-real complex real set
((Re ((lim s) ")) ^2) + ((Im ((lim s) ")) ^2) is ext-real complex real Element of REAL
sqrt (((Re ((lim s) ")) ^2) + ((Im ((lim s) ")) ^2)) is ext-real complex real Element of REAL
s is non zero Relation-like NAT -defined COMPLEX -valued Function-like V26( NAT ) V30( NAT , COMPLEX ) complex-valued Element of K11(K12(NAT,COMPLEX))
lim s is complex Element of COMPLEX
|.(lim s).| is ext-real complex real Element of REAL
Re (lim s) is ext-real complex real Element of REAL
(Re (lim s)) ^2 is ext-real complex real Element of REAL
(Re (lim s)) * (Re (lim s)) is ext-real complex real set
Im (lim s) is ext-real complex real Element of REAL
(Im (lim s)) ^2 is ext-real complex real Element of REAL
(Im (lim s)) * (Im (lim s)) is ext-real complex real set
((Re (lim s)) ^2) + ((Im (lim s)) ^2) is ext-real complex real Element of REAL
sqrt (((Re (lim s)) ^2) + ((Im (lim s)) ^2)) is ext-real complex real Element of REAL
s1 is non zero Relation-like NAT -defined COMPLEX -valued Function-like V26( NAT ) V30( NAT , COMPLEX ) complex-valued Element of K11(K12(NAT,COMPLEX))
lim s1 is complex Element of COMPLEX
s /" s1 is non zero Relation-like NAT -defined COMPLEX -valued Function-like V26( NAT ) V30( NAT , COMPLEX ) complex-valued Element of K11(K12(NAT,COMPLEX))
s1 " is Relation-like NAT -defined Function-like V26( NAT ) complex-valued set
s (#) (s1 ") is Relation-like NAT -defined Function-like V26( NAT ) complex-valued set
|.(s /" s1).| is non zero Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K11(K12(NAT,REAL))
(|.(s /" s1).|) is ext-real complex real Element of REAL
|.(lim s1).| is ext-real complex real Element of REAL
Re (lim s1) is ext-real complex real Element of REAL
(Re (lim s1)) ^2 is ext-real complex real Element of REAL
(Re (lim s1)) * (Re (lim s1)) is ext-real complex real set
Im (lim s1) is ext-real complex real Element of REAL
(Im (lim s1)) ^2 is ext-real complex real Element of REAL
(Im (lim s1)) * (Im (lim s1)) is ext-real complex real set
((Re (lim s1)) ^2) + ((Im (lim s1)) ^2) is ext-real complex real Element of REAL
sqrt (((Re (lim s1)) ^2) + ((Im (lim s1)) ^2)) is ext-real complex real Element of REAL
|.(lim s).| / |.(lim s1).| is ext-real complex real Element of REAL
lim (s /" s1) is complex Element of COMPLEX
|.(lim (s /" s1)).| is ext-real complex real Element of REAL
Re (lim (s /" s1)) is ext-real complex real Element of REAL
(Re (lim (s /" s1))) ^2 is ext-real complex real Element of REAL
(Re (lim (s /" s1))) * (Re (lim (s /" s1))) is ext-real complex real set
Im (lim (s /" s1)) is ext-real complex real Element of REAL
(Im (lim (s /" s1))) ^2 is ext-real complex real Element of REAL
(Im (lim (s /" s1))) * (Im (lim (s /" s1))) is ext-real complex real set
((Re (lim (s /" s1))) ^2) + ((Im (lim (s /" s1))) ^2) is ext-real complex real Element of REAL
sqrt (((Re (lim (s /" s1))) ^2) + ((Im (lim (s /" s1))) ^2)) is ext-real complex real Element of REAL
(lim s) / (lim s1) is complex Element of COMPLEX
|.((lim s) / (lim s1)).| is ext-real complex real Element of REAL
Re ((lim s) / (lim s1)) is ext-real complex real Element of REAL
(Re ((lim s) / (lim s1))) ^2 is ext-real complex real Element of REAL
(Re ((lim s) / (lim s1))) * (Re ((lim s) / (lim s1))) is ext-real complex real set
Im ((lim s) / (lim s1)) is ext-real complex real Element of REAL
(Im ((lim s) / (lim s1))) ^2 is ext-real complex real Element of REAL
(Im ((lim s) / (lim s1))) * (Im ((lim s) / (lim s1))) is ext-real complex real set
((Re ((lim s) / (lim s1))) ^2) + ((Im ((lim s) / (lim s1))) ^2) is ext-real complex real Element of REAL
sqrt (((Re ((lim s) / (lim s1))) ^2) + ((Im ((lim s) / (lim s1))) ^2)) is ext-real complex real Element of REAL
s is non zero Relation-like NAT -defined COMPLEX -valued Function-like V26( NAT ) V30( NAT , COMPLEX ) complex-valued Element of K11(K12(NAT,COMPLEX))
lim s is complex Element of COMPLEX
s1 is non zero Relation-like NAT -defined COMPLEX -valued Function-like V26( NAT ) V30( NAT , COMPLEX ) complex-valued Element of K11(K12(NAT,COMPLEX))
s (#) s1 is non zero Relation-like NAT -defined COMPLEX -valued Function-like V26( NAT ) V30( NAT , COMPLEX ) complex-valued Element of K11(K12(NAT,COMPLEX))
|.(s (#) s1).| is non zero Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K11(K12(NAT,REAL))
(|.(s (#) s1).|) is ext-real complex real Element of REAL
lim (s (#) s1) is complex Element of COMPLEX
|.(lim (s (#) s1)).| is ext-real complex real Element of REAL
Re (lim (s (#) s1)) is ext-real complex real Element of REAL
(Re (lim (s (#) s1))) ^2 is ext-real complex real Element of REAL
(Re (lim (s (#) s1))) * (Re (lim (s (#) s1))) is ext-real complex real set
Im (lim (s (#) s1)) is ext-real complex real Element of REAL
(Im (lim (s (#) s1))) ^2 is ext-real complex real Element of REAL
(Im (lim (s (#) s1))) * (Im (lim (s (#) s1))) is ext-real complex real set
((Re (lim (s (#) s1))) ^2) + ((Im (lim (s (#) s1))) ^2) is ext-real complex real Element of REAL
sqrt (((Re (lim (s (#) s1))) ^2) + ((Im (lim (s (#) s1))) ^2)) is ext-real complex real Element of REAL