:: COMSEQ_2 semantic presentation

REAL is non empty V47() V48() V49() V53() V54() set
NAT is non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() Element of K19(REAL)
K19(REAL) is set
COMPLEX is non empty V47() V53() V54() set
RAT is non empty V47() V48() V49() V50() V53() V54() set
INT is non empty V47() V48() V49() V50() V51() V53() V54() set
K20(NAT,COMPLEX) is complex-valued set
K19(K20(NAT,COMPLEX)) is set
0c is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative V47() V48() V49() V50() V51() V52() V53() Element of COMPLEX
1r is complex Element of COMPLEX
1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative V35() V36() V47() V48() V49() V50() V51() V52() V53() Element of NAT
0 *' is complex Element of COMPLEX
|.0.| is complex real ext-real V36() Element of REAL
{} is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative V47() V48() V49() V50() V51() V52() V53() set
sc is complex Element of COMPLEX
sc " is complex Element of COMPLEX
|.sc.| is complex real ext-real Element of REAL
s is complex Element of COMPLEX
s " is complex Element of COMPLEX
(sc ") - (s ") is complex Element of COMPLEX
|.((sc ") - (s ")).| is complex real ext-real Element of REAL
sc - s is complex Element of COMPLEX
|.(sc - s).| is complex real ext-real Element of REAL
|.s.| is complex real ext-real Element of REAL
|.sc.| * |.s.| is complex real ext-real Element of REAL
|.(sc - s).| / (|.sc.| * |.s.|) is complex real ext-real Element of REAL
1r / sc is complex Element of COMPLEX
(1r / sc) - (s ") is complex Element of COMPLEX
|.((1r / sc) - (s ")).| is complex real ext-real Element of REAL
1r / s is complex Element of COMPLEX
(1r / sc) - (1r / s) is complex Element of COMPLEX
|.((1r / sc) - (1r / s)).| is complex real ext-real Element of REAL
- (1r / s) is complex Element of COMPLEX
(1r / sc) + (- (1r / s)) is complex Element of COMPLEX
|.((1r / sc) + (- (1r / s))).| is complex real ext-real Element of REAL
1r * (s ") is complex Element of COMPLEX
- (1r * (s ")) is complex Element of COMPLEX
(1r / sc) + (- (1r * (s "))) is complex Element of COMPLEX
|.((1r / sc) + (- (1r * (s ")))).| is complex real ext-real Element of REAL
- 1r is complex Element of COMPLEX
(- 1r) * (s ") is complex Element of COMPLEX
(1r / sc) + ((- 1r) * (s ")) is complex Element of COMPLEX
|.((1r / sc) + ((- 1r) * (s "))).| is complex real ext-real Element of REAL
(- 1r) / s is complex Element of COMPLEX
(1r / sc) + ((- 1r) / s) is complex Element of COMPLEX
|.((1r / sc) + ((- 1r) / s)).| is complex real ext-real Element of REAL
1r * s is complex Element of COMPLEX
(- 1r) * sc is complex Element of COMPLEX
(1r * s) + ((- 1r) * sc) is complex Element of COMPLEX
s * sc is complex Element of COMPLEX
((1r * s) + ((- 1r) * sc)) / (s * sc) is complex Element of COMPLEX
|.(((1r * s) + ((- 1r) * sc)) / (s * sc)).| is complex real ext-real Element of REAL
s - sc is complex Element of COMPLEX
|.(s - sc).| is complex real ext-real Element of REAL
sc * s is complex Element of COMPLEX
|.(sc * s).| is complex real ext-real Element of REAL
|.(s - sc).| / |.(sc * s).| is complex real ext-real Element of REAL
- (sc - s) is complex Element of COMPLEX
|.(- (sc - s)).| is complex real ext-real Element of REAL
|.(- (sc - s)).| / (|.sc.| * |.s.|) is complex real ext-real Element of REAL
sc is Relation-like NAT -defined COMPLEX -valued Function-like non empty total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
s is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
s1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
s1 + 1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
R is complex real ext-real set
sc . (s1 + 1) is complex Element of COMPLEX
|.(sc . (s1 + 1)).| is complex real ext-real Element of REAL
|.(sc . (s1 + 1)).| + 1 is complex real ext-real Element of REAL
p is complex real ext-real Element of REAL
0 + 0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative V35() V36() V47() V48() V49() V50() V51() V52() V53() Element of NAT
n1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
sc . n1 is complex Element of COMPLEX
|.(sc . n1).| is complex real ext-real Element of REAL
|.(sc . n1).| + 0 is complex real ext-real Element of REAL
R + 1 is complex real ext-real Element of REAL
p is complex real ext-real Element of REAL
n1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
sc . n1 is complex Element of COMPLEX
|.(sc . n1).| is complex real ext-real Element of REAL
R + 0 is complex real ext-real Element of REAL
p is complex real ext-real Element of REAL
n1 is complex real ext-real Element of REAL
sc . 0 is complex Element of COMPLEX
|.(sc . 0).| is complex real ext-real Element of REAL
|.(sc . 0).| + 1 is complex real ext-real Element of REAL
s1 is complex real ext-real Element of REAL
0 + 0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative V35() V36() V47() V48() V49() V50() V51() V52() V53() Element of NAT
R is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
sc . R is complex Element of COMPLEX
|.(sc . R).| is complex real ext-real Element of REAL
|.(sc . R).| + 0 is complex real ext-real Element of REAL
s1 is complex real ext-real set
sc is Relation-like Function-like complex-valued set
dom sc is set
s is Relation-like Function-like set
dom s is set
s1 is set
s . s1 is set
sc . s1 is complex set
(sc . s1) *' is complex Element of COMPLEX
s1 is Relation-like Function-like complex-valued set
dom s1 is set
R is set
s1 . R is complex set
sc . R is complex set
(sc . R) *' is complex Element of COMPLEX
s is Relation-like Function-like complex-valued set
dom s is set
s1 is Relation-like Function-like complex-valued set
dom s1 is set
R is set
s . R is complex set
s1 . R is complex set
sc . R is complex set
(sc . R) *' is complex Element of COMPLEX
s is Relation-like Function-like complex-valued set
dom s is set
s1 is Relation-like Function-like complex-valued set
dom s1 is set
R is set
s1 . R is complex set
s . R is complex set
(s . R) *' is complex Element of COMPLEX
(s1 . R) *' is complex Element of COMPLEX
((s1 . R) *') *' is complex Element of COMPLEX
sc is non empty set
K20(sc,COMPLEX) is complex-valued set
K19(K20(sc,COMPLEX)) is set
s is Relation-like sc -defined COMPLEX -valued Function-like non empty total V18(sc, COMPLEX ) complex-valued Element of K19(K20(sc,COMPLEX))
(s) is Relation-like Function-like complex-valued set
dom (s) is set
dom s is Element of K19(sc)
K19(sc) is set
s1 is set
(s) . s1 is complex set
s1 is Relation-like sc -defined COMPLEX -valued Function-like non empty total V18(sc, COMPLEX ) complex-valued Element of K19(K20(sc,COMPLEX))
dom s1 is Element of K19(sc)
K19(sc) is set
R is Element of sc
s1 . R is complex Element of COMPLEX
s . R is complex Element of COMPLEX
(s . R) *' is complex Element of COMPLEX
dom s is Element of K19(sc)
R is set
s1 . R is complex set
s . R is complex set
(s . R) *' is complex Element of COMPLEX
sc is non empty set
s is Relation-like sc -defined Function-like non empty total complex-valued set
(s) is Relation-like Function-like complex-valued set
dom s is Element of K19(sc)
K19(sc) is set
dom (s) is set
sc is non empty set
s is Relation-like sc -defined Function-like non empty total complex-valued set
(s) is Relation-like sc -defined Function-like complex-valued set
s1 is Relation-like sc -defined Function-like set
dom s1 is Element of K19(sc)
K19(sc) is set
dom s is Element of K19(sc)
sc is Relation-like NAT -defined COMPLEX -valued Function-like non empty total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
(NAT,sc) is Relation-like NAT -defined COMPLEX -valued Function-like non empty total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
s is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
sc . s is complex Element of COMPLEX
(sc . s) *' is complex Element of COMPLEX
(NAT,sc) . s is complex Element of COMPLEX
sc is complex Element of COMPLEX
sc *' is complex Element of COMPLEX
s is Relation-like NAT -defined COMPLEX -valued Function-like non empty total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
sc (#) s is Relation-like NAT -defined COMPLEX -valued Function-like non empty total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
(NAT,(sc (#) s)) is Relation-like NAT -defined COMPLEX -valued Function-like non empty total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
(NAT,s) is Relation-like NAT -defined COMPLEX -valued Function-like non empty total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
(sc *') (#) (NAT,s) is Relation-like NAT -defined COMPLEX -valued Function-like non empty total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
s1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
(NAT,(sc (#) s)) . s1 is complex Element of COMPLEX
(sc (#) s) . s1 is complex Element of COMPLEX
((sc (#) s) . s1) *' is complex Element of COMPLEX
s . s1 is complex Element of COMPLEX
sc * (s . s1) is complex Element of COMPLEX
(sc * (s . s1)) *' is complex Element of COMPLEX
(s . s1) *' is complex Element of COMPLEX
(sc *') * ((s . s1) *') is complex Element of COMPLEX
(NAT,s) . s1 is complex Element of COMPLEX
(sc *') * ((NAT,s) . s1) is complex Element of COMPLEX
((sc *') (#) (NAT,s)) . s1 is complex Element of COMPLEX
sc is Relation-like NAT -defined COMPLEX -valued Function-like non empty total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
(NAT,sc) is Relation-like NAT -defined COMPLEX -valued Function-like non empty total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
s is Relation-like NAT -defined COMPLEX -valued Function-like non empty total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
sc (#) s is Relation-like NAT -defined COMPLEX -valued Function-like non empty total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
(NAT,(sc (#) s)) is Relation-like NAT -defined COMPLEX -valued Function-like non empty total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
(NAT,s) is Relation-like NAT -defined COMPLEX -valued Function-like non empty total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
(NAT,sc) (#) (NAT,s) is Relation-like NAT -defined COMPLEX -valued Function-like non empty total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
s1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
(NAT,(sc (#) s)) . s1 is complex Element of COMPLEX
(sc (#) s) . s1 is complex Element of COMPLEX
((sc (#) s) . s1) *' is complex Element of COMPLEX
sc . s1 is complex Element of COMPLEX
s . s1 is complex Element of COMPLEX
(sc . s1) * (s . s1) is complex Element of COMPLEX
((sc . s1) * (s . s1)) *' is complex Element of COMPLEX
(sc . s1) *' is complex Element of COMPLEX
(s . s1) *' is complex Element of COMPLEX
((sc . s1) *') * ((s . s1) *') is complex Element of COMPLEX
(NAT,sc) . s1 is complex Element of COMPLEX
((NAT,sc) . s1) * ((s . s1) *') is complex Element of COMPLEX
(NAT,s) . s1 is complex Element of COMPLEX
((NAT,sc) . s1) * ((NAT,s) . s1) is complex Element of COMPLEX
((NAT,sc) (#) (NAT,s)) . s1 is complex Element of COMPLEX
sc is Relation-like NAT -defined COMPLEX -valued Function-like non empty total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
(NAT,sc) is Relation-like NAT -defined COMPLEX -valued Function-like non empty total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
(NAT,sc) " is Relation-like NAT -defined COMPLEX -valued Function-like non empty total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
sc " is Relation-like NAT -defined COMPLEX -valued Function-like non empty total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
(NAT,(sc ")) is Relation-like NAT -defined COMPLEX -valued Function-like non empty total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
s is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
((NAT,sc) ") . s is complex Element of COMPLEX
(NAT,sc) . s is complex Element of COMPLEX
((NAT,sc) . s) " is complex Element of COMPLEX
sc . s is complex Element of COMPLEX
(sc . s) *' is complex Element of COMPLEX
((sc . s) *') " is complex Element of COMPLEX
(sc . s) " is complex Element of COMPLEX
((sc . s) ") *' is complex Element of COMPLEX
(sc ") . s is complex Element of COMPLEX
((sc ") . s) *' is complex Element of COMPLEX
(NAT,(sc ")) . s is complex Element of COMPLEX
sc is Relation-like NAT -defined COMPLEX -valued Function-like non empty total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
(NAT,sc) is Relation-like NAT -defined COMPLEX -valued Function-like non empty total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
s is Relation-like NAT -defined COMPLEX -valued Function-like non empty total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
sc /" s is Relation-like NAT -defined COMPLEX -valued Function-like non empty total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
s " is Relation-like NAT -defined Function-like non empty total complex-valued set
sc (#) (s ") is Relation-like NAT -defined Function-like non empty total complex-valued set
(NAT,(sc /" s)) is Relation-like NAT -defined COMPLEX -valued Function-like non empty total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
(NAT,s) is Relation-like NAT -defined COMPLEX -valued Function-like non empty total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
(NAT,sc) /" (NAT,s) is Relation-like NAT -defined COMPLEX -valued Function-like non empty total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
(NAT,s) " is Relation-like NAT -defined Function-like non empty total complex-valued set
(NAT,sc) (#) ((NAT,s) ") is Relation-like NAT -defined Function-like non empty total complex-valued set
s1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
(NAT,(sc /" s)) . s1 is complex Element of COMPLEX
s " is Relation-like NAT -defined COMPLEX -valued Function-like non empty total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
sc (#) (s ") is Relation-like NAT -defined COMPLEX -valued Function-like non empty total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
(sc (#) (s ")) . s1 is complex Element of COMPLEX
((sc (#) (s ")) . s1) *' is complex Element of COMPLEX
sc . s1 is complex Element of COMPLEX
(s ") . s1 is complex Element of COMPLEX
(sc . s1) * ((s ") . s1) is complex Element of COMPLEX
((sc . s1) * ((s ") . s1)) *' is complex Element of COMPLEX
s . s1 is complex Element of COMPLEX
(s . s1) " is complex Element of COMPLEX
(sc . s1) * ((s . s1) ") is complex Element of COMPLEX
((sc . s1) * ((s . s1) ")) *' is complex Element of COMPLEX
(sc . s1) *' is complex Element of COMPLEX
((s . s1) ") *' is complex Element of COMPLEX
((sc . s1) *') * (((s . s1) ") *') is complex Element of COMPLEX
(s . s1) *' is complex Element of COMPLEX
((s . s1) *') " is complex Element of COMPLEX
((sc . s1) *') * (((s . s1) *') ") is complex Element of COMPLEX
(NAT,sc) . s1 is complex Element of COMPLEX
((NAT,sc) . s1) * (((s . s1) *') ") is complex Element of COMPLEX
(NAT,s) . s1 is complex Element of COMPLEX
((NAT,s) . s1) " is complex Element of COMPLEX
((NAT,sc) . s1) * (((NAT,s) . s1) ") is complex Element of COMPLEX
(NAT,s) " is Relation-like NAT -defined COMPLEX -valued Function-like non empty total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
((NAT,s) ") . s1 is complex Element of COMPLEX
((NAT,sc) . s1) * (((NAT,s) ") . s1) is complex Element of COMPLEX
((NAT,sc) /" (NAT,s)) . s1 is complex Element of COMPLEX
sc is Relation-like NAT -defined COMPLEX -valued Function-like non empty total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
dom sc is V47() V48() V49() V50() V51() V52() Element of K19(NAT)
K19(NAT) is set
s is complex real ext-real set
s1 is complex real ext-real Element of REAL
R is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
sc . R is complex Element of COMPLEX
|.(sc . R).| is complex real ext-real Element of REAL
s is complex real ext-real Element of REAL
dom sc is V47() V48() V49() V50() V51() V52() set
s1 is set
sc . s1 is complex set
abs (sc . s1) is complex real ext-real Element of REAL
dom sc is V47() V48() V49() V50() V51() V52() Element of K19(NAT)
K19(NAT) is set
NAT --> 0c is Relation-like NAT -defined COMPLEX -valued Function-like non empty total V18( NAT , COMPLEX ) complex-valued ext-real-valued real-valued natural-valued Element of K19(K20(NAT,COMPLEX))
sc is Relation-like NAT -defined COMPLEX -valued Function-like non empty total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
s is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
sc . s is complex Element of COMPLEX
|.(sc . s).| is complex real ext-real Element of REAL
s is Relation-like NAT -defined COMPLEX -valued Function-like non empty total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
s1 is complex real ext-real Element of REAL
R is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
s . R is complex Element of COMPLEX
|.(s . R).| is complex real ext-real Element of REAL
R is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
s . R is complex Element of COMPLEX
|.(s . R).| is complex real ext-real Element of REAL
s1 is complex real ext-real Element of REAL
s is Relation-like NAT -defined COMPLEX -valued Function-like non empty total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
s1 is complex Element of COMPLEX
R is complex Element of COMPLEX
s1 - R is complex Element of COMPLEX
|.(s1 - R).| is complex real ext-real Element of REAL
2 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
|.(s1 - R).| / 2 is complex real ext-real Element of REAL
p is complex real ext-real Element of REAL
n1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
max (n1,n) is complex real ext-real set
m is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
2 * p is complex real ext-real Element of REAL
m is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
m + n is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
m + m is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
s . m is complex Element of COMPLEX
(s . m) - R is complex Element of COMPLEX
|.((s . m) - R).| is complex real ext-real Element of REAL
s1 - (s . m) is complex Element of COMPLEX
R - (s . m) is complex Element of COMPLEX
(s1 - (s . m)) - (R - (s . m)) is complex Element of COMPLEX
|.((s1 - (s . m)) - (R - (s . m))).| is complex real ext-real Element of REAL
|.(s1 - (s . m)).| is complex real ext-real Element of REAL
|.(R - (s . m)).| is complex real ext-real Element of REAL
|.(s1 - (s . m)).| + |.(R - (s . m)).| is complex real ext-real Element of REAL
(s . m) - s1 is complex Element of COMPLEX
|.((s . m) - s1).| is complex real ext-real Element of REAL
|.((s . m) - s1).| + |.(R - (s . m)).| is complex real ext-real Element of REAL
m + n1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
p + p is complex real ext-real Element of REAL
|.((s . m) - s1).| + |.((s . m) - R).| is complex real ext-real Element of REAL
s is Relation-like NAT -defined COMPLEX -valued Function-like non empty total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
s1 is complex Element of COMPLEX
R is complex real ext-real Element of REAL
p is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative V35() V36() V47() V48() V49() V50() V51() V52() V53() Element of NAT
n1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
s . n1 is complex Element of COMPLEX
(s . n1) - s1 is complex Element of COMPLEX
|.((s . n1) - s1).| is complex real ext-real Element of REAL
R is complex real ext-real Element of REAL
s is Relation-like NAT -defined COMPLEX -valued Function-like non empty total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
(s) is complex Element of COMPLEX
s1 is complex Element of COMPLEX
R is complex real ext-real Element of REAL
p is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative V35() V36() V47() V48() V49() V50() V51() V52() V53() Element of NAT
n1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
s . n1 is complex Element of COMPLEX
(s . n1) - s1 is complex Element of COMPLEX
|.((s . n1) - s1).| is complex real ext-real Element of REAL
sc is Relation-like NAT -defined COMPLEX -valued Function-like non empty total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
s is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
sc . s is complex Element of COMPLEX
s is Relation-like NAT -defined COMPLEX -valued Function-like non empty total V18( NAT , COMPLEX ) complex-valued () Element of K19(K20(NAT,COMPLEX))
(NAT,s) is Relation-like NAT -defined COMPLEX -valued Function-like non empty total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
s1 is Relation-like NAT -defined COMPLEX -valued Function-like non empty total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
R is complex Element of COMPLEX
R *' is complex Element of COMPLEX
n1 is complex Element of COMPLEX
n is complex real ext-real Element of REAL
m is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
s1 . m is complex set
(s1 . m) - n1 is complex set
|.((s1 . m) - n1).| is complex real ext-real Element of REAL
(NAT,s) . m is complex Element of COMPLEX
((NAT,s) . m) - n1 is complex Element of COMPLEX
|.(((NAT,s) . m) - n1).| is complex real ext-real Element of REAL
s . m is complex Element of COMPLEX
(s . m) *' is complex Element of COMPLEX
((s . m) *') - (R *') is complex Element of COMPLEX
|.(((s . m) *') - (R *')).| is complex real ext-real Element of REAL
(s . m) - R is complex Element of COMPLEX
((s . m) - R) *' is complex Element of COMPLEX
|.(((s . m) - R) *').| is complex real ext-real Element of REAL
|.((s . m) - R).| is complex real ext-real Element of REAL
s is Relation-like NAT -defined COMPLEX -valued Function-like non empty total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
(NAT,s) is Relation-like NAT -defined COMPLEX -valued Function-like non empty total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
((NAT,s)) is complex Element of COMPLEX
(s) is complex Element of COMPLEX
(s) *' is complex Element of COMPLEX
p is complex real ext-real Element of REAL
n1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
(NAT,s) . m is complex Element of COMPLEX
((NAT,s) . m) - ((s) *') is complex Element of COMPLEX
|.(((NAT,s) . m) - ((s) *')).| is complex real ext-real Element of REAL
s . m is complex Element of COMPLEX
(s . m) *' is complex Element of COMPLEX
((s . m) *') - ((s) *') is complex Element of COMPLEX
|.(((s . m) *') - ((s) *')).| is complex real ext-real Element of REAL
(s . m) - (s) is complex Element of COMPLEX
((s . m) - (s)) *' is complex Element of COMPLEX
|.(((s . m) - (s)) *').| is complex real ext-real Element of REAL
|.((s . m) - (s)).| is complex real ext-real Element of REAL
R is Relation-like NAT -defined COMPLEX -valued Function-like non empty total V18( NAT , COMPLEX ) complex-valued () Element of K19(K20(NAT,COMPLEX))
(NAT,R) is Relation-like NAT -defined COMPLEX -valued Function-like non empty total V18( NAT , COMPLEX ) complex-valued () Element of K19(K20(NAT,COMPLEX))
s is Relation-like NAT -defined COMPLEX -valued Function-like non empty total V18( NAT , COMPLEX ) complex-valued () Element of K19(K20(NAT,COMPLEX))
s1 is Relation-like NAT -defined COMPLEX -valued Function-like non empty total V18( NAT , COMPLEX ) complex-valued () Element of K19(K20(NAT,COMPLEX))
s + s1 is Relation-like NAT -defined COMPLEX -valued Function-like non empty total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
R is Relation-like NAT -defined COMPLEX -valued Function-like non empty total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
p is complex Element of COMPLEX
n1 is complex Element of COMPLEX
p + n1 is complex Element of COMPLEX
n is complex Element of COMPLEX
m is complex real ext-real Element of REAL
2 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
m / 2 is complex real ext-real Element of REAL
m is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
n1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
max (m,n1) is complex real ext-real set
n2 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
R . n is complex set
(R . n) - n is complex set
|.((R . n) - n).| is complex real ext-real Element of REAL
n2 + n1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
n2 + n is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
s1 . n is complex Element of COMPLEX
(s1 . n) - n1 is complex Element of COMPLEX
|.((s1 . n) - n1).| is complex real ext-real Element of REAL
(s + s1) . n is complex Element of COMPLEX
((s + s1) . n) - n is complex Element of COMPLEX
|.(((s + s1) . n) - n).| is complex real ext-real Element of REAL
s . n is complex Element of COMPLEX
(s . n) + (s1 . n) is complex Element of COMPLEX
((s . n) + (s1 . n)) - (p + n1) is complex Element of COMPLEX
|.(((s . n) + (s1 . n)) - (p + n1)).| is complex real ext-real Element of REAL
(s . n) - p is complex Element of COMPLEX
((s . n) - p) + ((s1 . n) - n1) is complex Element of COMPLEX
|.(((s . n) - p) + ((s1 . n) - n1)).| is complex real ext-real Element of REAL
n2 + m is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
|.((s . n) - p).| is complex real ext-real Element of REAL
(m / 2) + (m / 2) is complex real ext-real Element of REAL
|.((s . n) - p).| + |.((s1 . n) - n1).| is complex real ext-real Element of REAL
m + (|.((s . n) - p).| + |.((s1 . n) - n1).|) is complex real ext-real Element of REAL
(|.((s . n) - p).| + |.((s1 . n) - n1).|) + |.(((s + s1) . n) - n).| is complex real ext-real Element of REAL
s is Relation-like NAT -defined COMPLEX -valued Function-like non empty total V18( NAT , COMPLEX ) complex-valued () Element of K19(K20(NAT,COMPLEX))
s1 is Relation-like NAT -defined COMPLEX -valued Function-like non empty total V18( NAT , COMPLEX ) complex-valued () Element of K19(K20(NAT,COMPLEX))
s + s1 is Relation-like NAT -defined COMPLEX -valued Function-like non empty total V18( NAT , COMPLEX ) complex-valued () Element of K19(K20(NAT,COMPLEX))
((s + s1)) is complex Element of COMPLEX
(s) is complex Element of COMPLEX
(s1) is complex Element of COMPLEX
(s) + (s1) is complex Element of COMPLEX
R is complex real ext-real Element of REAL
2 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
R / 2 is complex real ext-real Element of REAL
p is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
n1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
max (p,n1) is complex real ext-real set
n is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
(s + s1) . m is complex Element of COMPLEX
((s + s1) . m) - ((s) + (s1)) is complex Element of COMPLEX
|.(((s + s1) . m) - ((s) + (s1))).| is complex real ext-real Element of REAL
n + n1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
n + m is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
s1 . m is complex Element of COMPLEX
(s1 . m) - (s1) is complex Element of COMPLEX
|.((s1 . m) - (s1)).| is complex real ext-real Element of REAL
s . m is complex Element of COMPLEX
(s . m) + (s1 . m) is complex Element of COMPLEX
((s . m) + (s1 . m)) - ((s) + (s1)) is complex Element of COMPLEX
|.(((s . m) + (s1 . m)) - ((s) + (s1))).| is complex real ext-real Element of REAL
(s . m) - (s) is complex Element of COMPLEX
((s . m) - (s)) + ((s1 . m) - (s1)) is complex Element of COMPLEX
|.(((s . m) - (s)) + ((s1 . m) - (s1))).| is complex real ext-real Element of REAL
n + p is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
|.((s . m) - (s)).| is complex real ext-real Element of REAL
(R / 2) + (R / 2) is complex real ext-real Element of REAL
|.((s . m) - (s)).| + |.((s1 . m) - (s1)).| is complex real ext-real Element of REAL
R + (|.((s . m) - (s)).| + |.((s1 . m) - (s1)).|) is complex real ext-real Element of REAL
(|.((s . m) - (s)).| + |.((s1 . m) - (s1)).|) + |.(((s + s1) . m) - ((s) + (s1))).| is complex real ext-real Element of REAL
s is Relation-like NAT -defined COMPLEX -valued Function-like non empty total V18( NAT , COMPLEX ) complex-valued () Element of K19(K20(NAT,COMPLEX))
s1 is Relation-like NAT -defined COMPLEX -valued Function-like non empty total V18( NAT , COMPLEX ) complex-valued () Element of K19(K20(NAT,COMPLEX))
s + s1 is Relation-like NAT -defined COMPLEX -valued Function-like non empty total V18( NAT , COMPLEX ) complex-valued () Element of K19(K20(NAT,COMPLEX))
(NAT,(s + s1)) is Relation-like NAT -defined COMPLEX -valued Function-like non empty total V18( NAT , COMPLEX ) complex-valued () Element of K19(K20(NAT,COMPLEX))
((NAT,(s + s1))) is complex Element of COMPLEX
(s) is complex Element of COMPLEX
(s) *' is complex Element of COMPLEX
(s1) is complex Element of COMPLEX
(s1) *' is complex Element of COMPLEX
((s) *') + ((s1) *') is complex Element of COMPLEX
((s + s1)) is complex Element of COMPLEX
((s + s1)) *' is complex Element of COMPLEX
(s) + (s1) is complex Element of COMPLEX
((s) + (s1)) *' is complex Element of COMPLEX
s is Relation-like NAT -defined COMPLEX -valued Function-like non empty total V18( NAT , COMPLEX ) complex-valued () Element of K19(K20(NAT,COMPLEX))
s1 is complex set
s1 (#) s is Relation-like NAT -defined COMPLEX -valued Function-like non empty total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
R is complex Element of COMPLEX
R (#) s is Relation-like NAT -defined COMPLEX -valued Function-like non empty total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
p is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
(R (#) s) . p is complex Element of COMPLEX
s . p is complex Element of COMPLEX
0c * (s . p) is complex Element of COMPLEX
R is complex Element of COMPLEX
R (#) s is Relation-like NAT -defined COMPLEX -valued Function-like non empty total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
p is complex Element of COMPLEX
R * p is complex Element of COMPLEX
n1 is complex Element of COMPLEX
n is complex real ext-real Element of REAL
|.R.| is complex real ext-real Element of REAL
n / |.R.| is complex real ext-real Element of REAL
m is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
(R (#) s) . m is complex set
((R (#) s) . m) - n1 is complex set
|.(((R (#) s) . m) - n1).| is complex real ext-real Element of REAL
s . m is complex Element of COMPLEX
(s . m) - p is complex Element of COMPLEX
|.((s . m) - p).| is complex real ext-real Element of REAL
(n / |.R.|) * |.R.| is complex real ext-real Element of REAL
|.((s . m) - p).| * |.R.| is complex real ext-real Element of REAL
|.R.| " is complex real ext-real Element of REAL
n * (|.R.| ") is complex real ext-real Element of REAL
(n * (|.R.| ")) * |.R.| is complex real ext-real Element of REAL
(|.R.| ") * |.R.| is complex real ext-real Element of REAL
n * ((|.R.| ") * |.R.|) is complex real ext-real Element of REAL
n * 1 is complex real ext-real Element of REAL
(R (#) s) . m is complex Element of COMPLEX
((R (#) s) . m) - n1 is complex Element of COMPLEX
|.(((R (#) s) . m) - n1).| is complex real ext-real Element of REAL
R * (s . m) is complex Element of COMPLEX
(R * (s . m)) - (R * p) is complex Element of COMPLEX
|.((R * (s . m)) - (R * p)).| is complex real ext-real Element of REAL
R * ((s . m) - p) is complex Element of COMPLEX
|.(R * ((s . m) - p)).| is complex real ext-real Element of REAL
R is complex Element of COMPLEX
R is Relation-like NAT -defined COMPLEX -valued Function-like non empty total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
s is Relation-like NAT -defined COMPLEX -valued Function-like non empty total V18( NAT , COMPLEX ) complex-valued () Element of K19(K20(NAT,COMPLEX))
(s) is complex Element of COMPLEX
s1 is complex set
s1 (#) s is Relation-like NAT -defined COMPLEX -valued Function-like non empty total V18( NAT , COMPLEX ) complex-valued () Element of K19(K20(NAT,COMPLEX))
((s1 (#) s)) is complex Element of COMPLEX
s1 * (s) is complex set
R is complex Element of COMPLEX
R (#) s is Relation-like NAT -defined COMPLEX -valued Function-like non empty total V18( NAT , COMPLEX ) complex-valued () Element of K19(K20(NAT,COMPLEX))
R * (s) is complex Element of COMPLEX
p is complex real ext-real Element of REAL
|.R.| is complex real ext-real Element of REAL
p / |.R.| is complex real ext-real Element of REAL
n1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
(R (#) s) . n is complex Element of COMPLEX
((R (#) s) . n) - (R * (s)) is complex Element of COMPLEX
|.(((R (#) s) . n) - (R * (s))).| is complex real ext-real Element of REAL
s . n is complex Element of COMPLEX
(s . n) - (s) is complex Element of COMPLEX
|.((s . n) - (s)).| is complex real ext-real Element of REAL
(p / |.R.|) * |.R.| is complex real ext-real Element of REAL
|.((s . n) - (s)).| * |.R.| is complex real ext-real Element of REAL
|.R.| " is complex real ext-real Element of REAL
p * (|.R.| ") is complex real ext-real Element of REAL
(p * (|.R.| ")) * |.R.| is complex real ext-real Element of REAL
(|.R.| ") * |.R.| is complex real ext-real Element of REAL
p * ((|.R.| ") * |.R.|) is complex real ext-real Element of REAL
p * 1 is complex real ext-real Element of REAL
R * (s . n) is complex Element of COMPLEX
(R * (s . n)) - (R * (s)) is complex Element of COMPLEX
|.((R * (s . n)) - (R * (s))).| is complex real ext-real Element of REAL
R * ((s . n) - (s)) is complex Element of COMPLEX
|.(R * ((s . n) - (s))).| is complex real ext-real Element of REAL
R is complex Element of COMPLEX
R (#) s is Relation-like NAT -defined COMPLEX -valued Function-like non empty total V18( NAT , COMPLEX ) complex-valued () Element of K19(K20(NAT,COMPLEX))
p is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
(R (#) s) . p is complex Element of COMPLEX
s . p is complex Element of COMPLEX
0c * (s . p) is complex Element of COMPLEX
R is complex Element of COMPLEX
s is complex Element of COMPLEX
s *' is complex Element of COMPLEX
s1 is Relation-like NAT -defined COMPLEX -valued Function-like non empty total V18( NAT , COMPLEX ) complex-valued () Element of K19(K20(NAT,COMPLEX))
s (#) s1 is Relation-like NAT -defined COMPLEX -valued Function-like non empty total V18( NAT , COMPLEX ) complex-valued () Element of K19(K20(NAT,COMPLEX))
(NAT,(s (#) s1)) is Relation-like NAT -defined COMPLEX -valued Function-like non empty total V18( NAT , COMPLEX ) complex-valued () Element of K19(K20(NAT,COMPLEX))
((NAT,(s (#) s1))) is complex Element of COMPLEX
(s1) is complex Element of COMPLEX
(s1) *' is complex Element of COMPLEX
(s *') * ((s1) *') is complex Element of COMPLEX
((s (#) s1)) is complex Element of COMPLEX
((s (#) s1)) *' is complex Element of COMPLEX
s * (s1) is complex Element of COMPLEX
(s * (s1)) *' is complex Element of COMPLEX
s is Relation-like NAT -defined COMPLEX -valued Function-like non empty total V18( NAT , COMPLEX ) complex-valued () Element of K19(K20(NAT,COMPLEX))
- s is Relation-like NAT -defined COMPLEX -valued Function-like non empty total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
- 1 is non empty complex real ext-real non positive negative set
(- 1) (#) s is Relation-like NAT -defined Function-like non empty total complex-valued set
s1 is Relation-like NAT -defined COMPLEX -valued Function-like non empty total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
s is Relation-like NAT -defined COMPLEX -valued Function-like non empty total V18( NAT , COMPLEX ) complex-valued () Element of K19(K20(NAT,COMPLEX))
- s is Relation-like NAT -defined COMPLEX -valued Function-like non empty total V18( NAT , COMPLEX ) complex-valued () Element of K19(K20(NAT,COMPLEX))
(- 1) (#) s is Relation-like NAT -defined Function-like non empty total complex-valued set
((- s)) is complex Element of COMPLEX
(s) is complex Element of COMPLEX
- (s) is complex Element of COMPLEX
- 1 is non empty complex real ext-real non positive negative Element of REAL
(- 1) * (s) is complex set
1r * (s) is complex Element of COMPLEX
- (1r * (s)) is complex Element of COMPLEX
s is Relation-like NAT -defined COMPLEX -valued Function-like non empty total V18( NAT , COMPLEX ) complex-valued () Element of K19(K20(NAT,COMPLEX))
- s is Relation-like NAT -defined COMPLEX -valued Function-like non empty total V18( NAT , COMPLEX ) complex-valued () Element of K19(K20(NAT,COMPLEX))
(- 1) (#) s is Relation-like NAT -defined Function-like non empty total complex-valued set
(NAT,(- s)) is Relation-like NAT -defined COMPLEX -valued Function-like non empty total V18( NAT , COMPLEX ) complex-valued () Element of K19(K20(NAT,COMPLEX))
((NAT,(- s))) is complex Element of COMPLEX
(s) is complex Element of COMPLEX
(s) *' is complex Element of COMPLEX
- ((s) *') is complex Element of COMPLEX
((- s)) is complex Element of COMPLEX
((- s)) *' is complex Element of COMPLEX
- (s) is complex Element of COMPLEX
(- (s)) *' is complex Element of COMPLEX
s is Relation-like NAT -defined COMPLEX -valued Function-like non empty total V18( NAT , COMPLEX ) complex-valued () Element of K19(K20(NAT,COMPLEX))
s1 is Relation-like NAT -defined COMPLEX -valued Function-like non empty total V18( NAT , COMPLEX ) complex-valued () Element of K19(K20(NAT,COMPLEX))
s - s1 is Relation-like NAT -defined COMPLEX -valued Function-like non empty total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
- s1 is Relation-like NAT -defined Function-like non empty total complex-valued set
(- 1) (#) s1 is Relation-like NAT -defined Function-like non empty total complex-valued set
s + (- s1) is Relation-like NAT -defined Function-like non empty total complex-valued set
- s1 is Relation-like NAT -defined COMPLEX -valued Function-like non empty total V18( NAT , COMPLEX ) complex-valued () Element of K19(K20(NAT,COMPLEX))
R is Relation-like NAT -defined COMPLEX -valued Function-like non empty total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
s is Relation-like NAT -defined COMPLEX -valued Function-like non empty total V18( NAT , COMPLEX ) complex-valued () Element of K19(K20(NAT,COMPLEX))
s1 is Relation-like NAT -defined COMPLEX -valued Function-like non empty total V18( NAT , COMPLEX ) complex-valued () Element of K19(K20(NAT,COMPLEX))
s - s1 is Relation-like NAT -defined COMPLEX -valued Function-like non empty total V18( NAT , COMPLEX ) complex-valued () Element of K19(K20(NAT,COMPLEX))
- s1 is Relation-like NAT -defined Function-like non empty total complex-valued set
(- 1) (#) s1 is Relation-like NAT -defined Function-like non empty total complex-valued set
s + (- s1) is Relation-like NAT -defined Function-like non empty total complex-valued set
((s - s1)) is complex Element of COMPLEX
(s) is complex Element of COMPLEX
(s1) is complex Element of COMPLEX
(s) - (s1) is complex Element of COMPLEX
- s1 is Relation-like NAT -defined COMPLEX -valued Function-like non empty total V18( NAT , COMPLEX ) complex-valued () Element of K19(K20(NAT,COMPLEX))
((- s1)) is complex Element of COMPLEX
(s) + ((- s1)) is complex Element of COMPLEX
- (s1) is complex Element of COMPLEX
(s) + (- (s1)) is complex Element of COMPLEX
s is Relation-like NAT -defined COMPLEX -valued Function-like non empty total V18( NAT , COMPLEX ) complex-valued () Element of K19(K20(NAT,COMPLEX))
s1 is Relation-like NAT -defined COMPLEX -valued Function-like non empty total V18( NAT , COMPLEX ) complex-valued () Element of K19(K20(NAT,COMPLEX))
s - s1 is Relation-like NAT -defined COMPLEX -valued Function-like non empty total V18( NAT , COMPLEX ) complex-valued () Element of K19(K20(NAT,COMPLEX))
- s1 is Relation-like NAT -defined Function-like non empty total complex-valued set
(- 1) (#) s1 is Relation-like NAT -defined Function-like non empty total complex-valued set
s + (- s1) is Relation-like NAT -defined Function-like non empty total complex-valued set
(NAT,(s - s1)) is Relation-like NAT -defined COMPLEX -valued Function-like non empty total V18( NAT , COMPLEX ) complex-valued () Element of K19(K20(NAT,COMPLEX))
((NAT,(s - s1))) is complex Element of COMPLEX
(s) is complex Element of COMPLEX
(s) *' is complex Element of COMPLEX
(s1) is complex Element of COMPLEX
(s1) *' is complex Element of COMPLEX
((s) *') - ((s1) *') is complex Element of COMPLEX
((s - s1)) is complex Element of COMPLEX
((s - s1)) *' is complex Element of COMPLEX
(s) - (s1) is complex Element of COMPLEX
((s) - (s1)) *' is complex Element of COMPLEX
s is Relation-like NAT -defined COMPLEX -valued Function-like non empty total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
s1 is complex Element of COMPLEX
R is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
|.s1.| is complex real ext-real Element of REAL
|.s1.| + 1 is complex real ext-real Element of REAL
p is complex real ext-real Element of REAL
0 + 0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative V35() V36() V47() V48() V49() V50() V51() V52() V53() Element of NAT
n1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
s . n1 is complex Element of COMPLEX
|.(s . n1).| is complex real ext-real Element of REAL
|.(s . n1).| - |.s1.| is complex real ext-real Element of REAL
(|.(s . n1).| - |.s1.|) + |.s1.| is complex real ext-real Element of REAL
(s . n1) - s1 is complex Element of COMPLEX
|.((s . n1) - s1).| is complex real ext-real Element of REAL
p is complex real ext-real Element of REAL
p is complex real ext-real set
n1 is complex real ext-real Element of REAL
p + n1 is complex real ext-real Element of REAL
n is complex real ext-real Element of REAL
m is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
s . m is complex Element of COMPLEX
|.(s . m).| is complex real ext-real Element of REAL
n1 + 0 is complex real ext-real Element of REAL
p + 0 is complex real ext-real Element of REAL
s is Relation-like NAT -defined COMPLEX -valued Function-like non empty total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
s is Relation-like NAT -defined COMPLEX -valued Function-like non empty total V18( NAT , COMPLEX ) complex-valued () () Element of K19(K20(NAT,COMPLEX))
s1 is Relation-like NAT -defined COMPLEX -valued Function-like non empty total V18( NAT , COMPLEX ) complex-valued () () Element of K19(K20(NAT,COMPLEX))
s (#) s1 is Relation-like NAT -defined COMPLEX -valued Function-like non empty total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
R is Relation-like NAT -defined COMPLEX -valued Function-like non empty total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
p is complex Element of COMPLEX
n1 is complex Element of COMPLEX
p * n1 is complex Element of COMPLEX
n is complex Element of COMPLEX
m is complex real ext-real Element of REAL
m is complex real ext-real Element of REAL
|.n1.| is complex real ext-real Element of REAL
|.n1.| + m is complex real ext-real Element of REAL
0 + 0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative V35() V36() V47() V48() V49() V50() V51() V52() V53() Element of NAT
m / (|.n1.| + m) is complex real ext-real Element of REAL
n1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
n2 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
n1 + n2 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
R . m is complex set
(R . m) - n is complex set
|.((R . m) - n).| is complex real ext-real Element of REAL
s . m is complex Element of COMPLEX
(s . m) - p is complex Element of COMPLEX
|.((s . m) - p).| is complex real ext-real Element of REAL
((s . m) - p) * n1 is complex Element of COMPLEX
|.(((s . m) - p) * n1).| is complex real ext-real Element of REAL
|.n1.| * |.((s . m) - p).| is complex real ext-real Element of REAL
|.n1.| * (m / (|.n1.| + m)) is complex real ext-real Element of REAL
(s (#) s1) . m is complex Element of COMPLEX
((s (#) s1) . m) - n is complex Element of COMPLEX
|.(((s (#) s1) . m) - n).| is complex real ext-real Element of REAL
s1 . m is complex Element of COMPLEX
(s . m) * (s1 . m) is complex Element of COMPLEX
(s . m) * n1 is complex Element of COMPLEX
((s . m) * (s1 . m)) - ((s . m) * n1) is complex Element of COMPLEX
(((s . m) * (s1 . m)) - ((s . m) * n1)) + ((s . m) * n1) is complex Element of COMPLEX
((((s . m) * (s1 . m)) - ((s . m) * n1)) + ((s . m) * n1)) - (p * n1) is complex Element of COMPLEX
|.(((((s . m) * (s1 . m)) - ((s . m) * n1)) + ((s . m) * n1)) - (p * n1)).| is complex real ext-real Element of REAL
(s1 . m) - n1 is complex Element of COMPLEX
(s . m) * ((s1 . m) - n1) is complex Element of COMPLEX
((s . m) * ((s1 . m) - n1)) + (((s . m) - p) * n1) is complex Element of COMPLEX
|.(((s . m) * ((s1 . m) - n1)) + (((s . m) - p) * n1)).| is complex real ext-real Element of REAL
|.((s . m) * ((s1 . m) - n1)).| is complex real ext-real Element of REAL
|.((s . m) * ((s1 . m) - n1)).| + |.(((s . m) - p) * n1).| is complex real ext-real Element of REAL
|.((s1 . m) - n1).| is complex real ext-real Element of REAL
|.(s . m).| is complex real ext-real Element of REAL
m * (m / (|.n1.| + m)) is complex real ext-real Element of REAL
|.(s . m).| * |.((s1 . m) - n1).| is complex real ext-real Element of REAL
(m * (m / (|.n1.| + m))) + (|.n1.| * (m / (|.n1.| + m))) is complex real ext-real Element of REAL
(m / (|.n1.| + m)) * (|.n1.| + m) is complex real ext-real Element of REAL
s is Relation-like NAT -defined COMPLEX -valued Function-like non empty total V18( NAT , COMPLEX ) complex-valued () () Element of K19(K20(NAT,COMPLEX))
s1 is Relation-like NAT -defined COMPLEX -valued Function-like non empty total V18( NAT , COMPLEX ) complex-valued () () Element of K19(K20(NAT,COMPLEX))
s (#) s1 is Relation-like NAT -defined COMPLEX -valued Function-like non empty total V18( NAT , COMPLEX ) complex-valued () () Element of K19(K20(NAT,COMPLEX))
((s (#) s1)) is complex Element of COMPLEX
(s) is complex Element of COMPLEX
(s1) is complex Element of COMPLEX
(s) * (s1) is complex Element of COMPLEX
R is complex real ext-real Element of REAL
|.(s1).| is complex real ext-real Element of REAL
|.(s1).| + R is complex real ext-real Element of REAL
0 + 0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative V35() V36() V47() V48() V49() V50() V51() V52() V53() Element of NAT
p is complex real ext-real Element of REAL
p / (|.(s1).| + R) is complex real ext-real Element of REAL
n1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
n1 + n is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
s . m is complex Element of COMPLEX
(s . m) - (s) is complex Element of COMPLEX
|.((s . m) - (s)).| is complex real ext-real Element of REAL
((s . m) - (s)) * (s1) is complex Element of COMPLEX
|.(((s . m) - (s)) * (s1)).| is complex real ext-real Element of REAL
|.(s1).| * |.((s . m) - (s)).| is complex real ext-real Element of REAL
|.(s1).| * (p / (|.(s1).| + R)) is complex real ext-real Element of REAL
|.(s . m).| is complex real ext-real Element of REAL
s1 . m is complex Element of COMPLEX
(s1 . m) - (s1) is complex Element of COMPLEX
|.((s1 . m) - (s1)).| is complex real ext-real Element of REAL
(s (#) s1) . m is complex Element of COMPLEX
((s (#) s1) . m) - ((s) * (s1)) is complex Element of COMPLEX
|.(((s (#) s1) . m) - ((s) * (s1))).| is complex real ext-real Element of REAL
(s . m) * (s1 . m) is complex Element of COMPLEX
(s . m) * (s1) is complex Element of COMPLEX
((s . m) * (s1 . m)) - ((s . m) * (s1)) is complex Element of COMPLEX
(((s . m) * (s1 . m)) - ((s . m) * (s1))) + ((s . m) * (s1)) is complex Element of COMPLEX
((((s . m) * (s1 . m)) - ((s . m) * (s1))) + ((s . m) * (s1))) - ((s) * (s1)) is complex Element of COMPLEX
|.(((((s . m) * (s1 . m)) - ((s . m) * (s1))) + ((s . m) * (s1))) - ((s) * (s1))).| is complex real ext-real Element of REAL
(s . m) * ((s1 . m) - (s1)) is complex Element of COMPLEX
((s . m) * ((s1 . m) - (s1))) + (((s . m) - (s)) * (s1)) is complex Element of COMPLEX
|.(((s . m) * ((s1 . m) - (s1))) + (((s . m) - (s)) * (s1))).| is complex real ext-real Element of REAL
|.((s . m) * ((s1 . m) - (s1))).| is complex real ext-real Element of REAL
|.((s . m) * ((s1 . m) - (s1))).| + |.(((s . m) - (s)) * (s1)).| is complex real ext-real Element of REAL
R * (p / (|.(s1).| + R)) is complex real ext-real Element of REAL
|.(s . m).| * |.((s1 . m) - (s1)).| is complex real ext-real Element of REAL
(R * (p / (|.(s1).| + R))) + (|.(s1).| * (p / (|.(s1).| + R))) is complex real ext-real Element of REAL
(p / (|.(s1).| + R)) * (|.(s1).| + R) is complex real ext-real Element of REAL
s is Relation-like NAT -defined COMPLEX -valued Function-like non empty total V18( NAT , COMPLEX ) complex-valued () () Element of K19(K20(NAT,COMPLEX))
s1 is Relation-like NAT -defined COMPLEX -valued Function-like non empty total V18( NAT , COMPLEX ) complex-valued () () Element of K19(K20(NAT,COMPLEX))
s (#) s1 is Relation-like NAT -defined COMPLEX -valued Function-like non empty total V18( NAT , COMPLEX ) complex-valued () () Element of K19(K20(NAT,COMPLEX))
(NAT,(s (#) s1)) is Relation-like NAT -defined COMPLEX -valued Function-like non empty total V18( NAT , COMPLEX ) complex-valued () () Element of K19(K20(NAT,COMPLEX))
((NAT,(s (#) s1))) is complex Element of COMPLEX
(s) is complex Element of COMPLEX
(s) *' is complex Element of COMPLEX
(s1) is complex Element of COMPLEX
(s1) *' is complex Element of COMPLEX
((s) *') * ((s1) *') is complex Element of COMPLEX
((s (#) s1)) is complex Element of COMPLEX
((s (#) s1)) *' is complex Element of COMPLEX
(s) * (s1) is complex Element of COMPLEX
((s) * (s1)) *' is complex Element of COMPLEX
2 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
s is Relation-like NAT -defined COMPLEX -valued Function-like non empty total V18( NAT , COMPLEX ) complex-valued () () Element of K19(K20(NAT,COMPLEX))
(s) is complex Element of COMPLEX
|.(s).| is complex real ext-real Element of REAL
|.(s).| / 2 is complex real ext-real Element of REAL
s1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
R is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
p is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
s . p is complex Element of COMPLEX
|.(s . p).| is complex real ext-real Element of REAL
(s . p) - (s) is complex Element of COMPLEX
|.((s . p) - (s)).| is complex real ext-real Element of REAL
(s) - (s . p) is complex Element of COMPLEX
|.((s) - (s . p)).| is complex real ext-real Element of REAL
- ((s . p) - (s)) is complex Element of COMPLEX
|.(- ((s . p) - (s))).| is complex real ext-real Element of REAL
|.(s . p).| - (|.(s).| / 2) is complex real ext-real Element of REAL
(|.(s).| / 2) + (|.(s . p).| - (|.(s).| / 2)) is complex real ext-real Element of REAL
|.(s).| - |.(s . p).| is complex real ext-real Element of REAL
(|.(s).| - |.(s . p).|) + (|.(s . p).| - (|.(s).| / 2)) is complex real ext-real Element of REAL
s is Relation-like NAT -defined COMPLEX -valued Function-like non empty total V18( NAT , COMPLEX ) complex-valued () () Element of K19(K20(NAT,COMPLEX))
(s) is complex Element of COMPLEX
s " is Relation-like NAT -defined COMPLEX -valued Function-like non empty total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
|.(s).| is complex real ext-real Element of REAL
|.(s).| / 2 is complex real ext-real Element of REAL
s1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
(s) " is complex Element of COMPLEX
R is complex real ext-real Element of REAL
|.(s).| * |.(s).| is complex real ext-real Element of REAL
0 * 0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative V35() V36() V47() V48() V49() V50() V51() V52() V53() Element of NAT
(|.(s).| * |.(s).|) / 2 is complex real ext-real Element of REAL
R * ((|.(s).| * |.(s).|) / 2) is complex real ext-real Element of REAL
p is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
s1 + p is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
n1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
(s ") . n is complex set
((s ") . n) - ((s) ") is complex set
|.(((s ") . n) - ((s) ")).| is complex real ext-real Element of REAL
s . n is complex Element of COMPLEX
|.(s . n).| is complex real ext-real Element of REAL
R * (|.(s).| / 2) is complex real ext-real Element of REAL
(R * (|.(s).| / 2)) / (|.(s).| / 2) is complex real ext-real Element of REAL
(R * (|.(s).| / 2)) / |.(s . n).| is complex real ext-real Element of REAL
(|.(s).| / 2) " is complex real ext-real Element of REAL
(R * (|.(s).| / 2)) * ((|.(s).| / 2) ") is complex real ext-real Element of REAL
(|.(s).| / 2) * ((|.(s).| / 2) ") is complex real ext-real Element of REAL
R * ((|.(s).| / 2) * ((|.(s).| / 2) ")) is complex real ext-real Element of REAL
R * 1 is complex real ext-real Element of REAL
|.(s . n).| * |.(s).| is complex real ext-real Element of REAL
(R * ((|.(s).| * |.(s).|) / 2)) / (|.(s . n).| * |.(s).|) is complex real ext-real Element of REAL
2 " is non empty complex real ext-real positive non negative Element of REAL
(2 ") * (|.(s).| * |.(s).|) is complex real ext-real Element of REAL
R * ((2 ") * (|.(s).| * |.(s).|)) is complex real ext-real Element of REAL
(|.(s . n).| * |.(s).|) " is complex real ext-real Element of REAL
(R * ((2 ") * (|.(s).| * |.(s).|))) * ((|.(s . n).| * |.(s).|) ") is complex real ext-real Element of REAL
R * (2 ") is complex real ext-real Element of REAL
|.(s).| * |.(s . n).| is complex real ext-real Element of REAL
(|.(s).| * |.(s . n).|) " is complex real ext-real Element of REAL
(|.(s).| * |.(s).|) * ((|.(s).| * |.(s . n).|) ") is complex real ext-real Element of REAL
(R * (2 ")) * ((|.(s).| * |.(s).|) * ((|.(s).| * |.(s . n).|) ")) is complex real ext-real Element of REAL
|.(s).| " is complex real ext-real Element of REAL
|.(s . n).| " is complex real ext-real Element of REAL
(|.(s).| ") * (|.(s . n).| ") is complex real ext-real Element of REAL
(|.(s).| * |.(s).|) * ((|.(s).| ") * (|.(s . n).| ")) is complex real ext-real Element of REAL
(R * (2 ")) * ((|.(s).| * |.(s).|) * ((|.(s).| ") * (|.(s . n).| "))) is complex real ext-real Element of REAL
|.(s).| * (|.(s).| ") is complex real ext-real Element of REAL
|.(s).| * (|.(s).| * (|.(s).| ")) is complex real ext-real Element of REAL
(|.(s).| * (|.(s).| * (|.(s).| "))) * (|.(s . n).| ") is complex real ext-real Element of REAL
(R * (2 ")) * ((|.(s).| * (|.(s).| * (|.(s).| "))) * (|.(s . n).| ")) is complex real ext-real Element of REAL
|.(s).| * 1 is complex real ext-real Element of REAL
(|.(s).| * 1) * (|.(s . n).| ") is complex real ext-real Element of REAL
(R * (2 ")) * ((|.(s).| * 1) * (|.(s . n).| ")) is complex real ext-real Element of REAL
(R * (|.(s).| / 2)) * (|.(s . n).| ") is complex real ext-real Element of REAL
(s . n) * (s) is complex Element of COMPLEX
|.((s . n) * (s)).| is complex real ext-real Element of REAL
(s . n) - (s) is complex Element of COMPLEX
|.((s . n) - (s)).| is complex real ext-real Element of REAL
|.((s . n) - (s)).| / (|.(s . n).| * |.(s).|) is complex real ext-real Element of REAL
(s ") . n is complex Element of COMPLEX
((s ") . n) - ((s) ") is complex Element of COMPLEX
|.(((s ") . n) - ((s) ")).| is complex real ext-real Element of REAL
(s . n) " is complex Element of COMPLEX
((s . n) ") - ((s) ") is complex Element of COMPLEX
|.(((s . n) ") - ((s) ")).| is complex real ext-real Element of REAL
s is Relation-like NAT -defined COMPLEX -valued Function-like non empty total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
(s) is complex Element of COMPLEX
s " is Relation-like NAT -defined COMPLEX -valued Function-like non empty total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
((s ")) is complex Element of COMPLEX
(s) " is complex Element of COMPLEX
|.(s).| is complex real ext-real Element of REAL
|.(s).| / 2 is complex real ext-real Element of REAL
s1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
|.(s).| * |.(s).| is complex real ext-real Element of REAL
0 * 0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative V35() V36() V47() V48() V49() V50() V51() V52() V53() Element of NAT
(|.(s).| * |.(s).|) / 2 is complex real ext-real Element of REAL
R is complex real ext-real Element of REAL
R * (|.(s).| / 2) is complex real ext-real Element of REAL
(R * (|.(s).| / 2)) / (|.(s).| / 2) is complex real ext-real Element of REAL
(|.(s).| / 2) " is complex real ext-real Element of REAL
(R * (|.(s).| / 2)) * ((|.(s).| / 2) ") is complex real ext-real Element of REAL
(|.(s).| / 2) * ((|.(s).| / 2) ") is complex real ext-real Element of REAL
R * ((|.(s).| / 2) * ((|.(s).| / 2) ")) is complex real ext-real Element of REAL
R * 1 is complex real ext-real Element of REAL
R * ((|.(s).| * |.(s).|) / 2) is complex real ext-real Element of REAL
p is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
s1 + p is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
n1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
s . n is complex Element of COMPLEX
|.(s . n).| is complex real ext-real Element of REAL
(R * (|.(s).| / 2)) / |.(s . n).| is complex real ext-real Element of REAL
|.(s . n).| * |.(s).| is complex real ext-real Element of REAL
(R * ((|.(s).| * |.(s).|) / 2)) / (|.(s . n).| * |.(s).|) is complex real ext-real Element of REAL
2 " is non empty complex real ext-real positive non negative Element of REAL
(2 ") * (|.(s).| * |.(s).|) is complex real ext-real Element of REAL
R * ((2 ") * (|.(s).| * |.(s).|)) is complex real ext-real Element of REAL
(|.(s . n).| * |.(s).|) " is complex real ext-real Element of REAL
(R * ((2 ") * (|.(s).| * |.(s).|))) * ((|.(s . n).| * |.(s).|) ") is complex real ext-real Element of REAL
R * (2 ") is complex real ext-real Element of REAL
|.(s).| * |.(s . n).| is complex real ext-real Element of REAL
(|.(s).| * |.(s . n).|) " is complex real ext-real Element of REAL
(|.(s).| * |.(s).|) * ((|.(s).| * |.(s . n).|) ") is complex real ext-real Element of REAL
(R * (2 ")) * ((|.(s).| * |.(s).|) * ((|.(s).| * |.(s . n).|) ")) is complex real ext-real Element of REAL
|.(s).| " is complex real ext-real Element of REAL
|.(s . n).| " is complex real ext-real Element of REAL
(|.(s).| ") * (|.(s . n).| ") is complex real ext-real Element of REAL
(|.(s).| * |.(s).|) * ((|.(s).| ") * (|.(s . n).| ")) is complex real ext-real Element of REAL
(R * (2 ")) * ((|.(s).| * |.(s).|) * ((|.(s).| ") * (|.(s . n).| "))) is complex real ext-real Element of REAL
|.(s).| * (|.(s).| ") is complex real ext-real Element of REAL
|.(s).| * (|.(s).| * (|.(s).| ")) is complex real ext-real Element of REAL
(|.(s).| * (|.(s).| * (|.(s).| "))) * (|.(s . n).| ") is complex real ext-real Element of REAL
(R * (2 ")) * ((|.(s).| * (|.(s).| * (|.(s).| "))) * (|.(s . n).| ")) is complex real ext-real Element of REAL
|.(s).| * 1 is complex real ext-real Element of REAL
(|.(s).| * 1) * (|.(s . n).| ") is complex real ext-real Element of REAL
(R * (2 ")) * ((|.(s).| * 1) * (|.(s . n).| ")) is complex real ext-real Element of REAL
(R * (|.(s).| / 2)) * (|.(s . n).| ") is complex real ext-real Element of REAL
(s . n) * (s) is complex Element of COMPLEX
|.((s . n) * (s)).| is complex real ext-real Element of REAL
(s . n) - (s) is complex Element of COMPLEX
|.((s . n) - (s)).| is complex real ext-real Element of REAL
|.((s . n) - (s)).| / (|.(s . n).| * |.(s).|) is complex real ext-real Element of REAL
(s ") . n is complex Element of COMPLEX
((s ") . n) - ((s) ") is complex Element of COMPLEX
|.(((s ") . n) - ((s) ")).| is complex real ext-real Element of REAL
(s . n) " is complex Element of COMPLEX
((s . n) ") - ((s) ") is complex Element of COMPLEX
|.(((s . n) ") - ((s) ")).| is complex real ext-real Element of REAL
s is Relation-like NAT -defined COMPLEX -valued Function-like non empty total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
(s) is complex Element of COMPLEX
s " is Relation-like NAT -defined COMPLEX -valued Function-like non empty total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
(NAT,(s ")) is Relation-like NAT -defined COMPLEX -valued Function-like non empty total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
((NAT,(s "))) is complex Element of COMPLEX
(s) *' is complex Element of COMPLEX
((s) *') " is complex Element of COMPLEX
((s ")) is complex Element of COMPLEX
((s ")) *' is complex Element of COMPLEX
(s) " is complex Element of COMPLEX
((s) ") *' is complex Element of COMPLEX
s is Relation-like NAT -defined COMPLEX -valued Function-like non empty total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
s1 is Relation-like NAT -defined COMPLEX -valued Function-like non empty total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
(s1) is complex Element of COMPLEX
s /" s1 is Relation-like NAT -defined COMPLEX -valued Function-like non empty total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
s1 " is Relation-like NAT -defined Function-like non empty total complex-valued set
s (#) (s1 ") is Relation-like NAT -defined Function-like non empty total complex-valued set
s1 " is Relation-like NAT -defined COMPLEX -valued Function-like non empty total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
s is Relation-like NAT -defined COMPLEX -valued Function-like non empty total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
(s) is complex Element of COMPLEX
s1 is Relation-like NAT -defined COMPLEX -valued Function-like non empty total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
(s1) is complex Element of COMPLEX
s /" s1 is Relation-like NAT -defined COMPLEX -valued Function-like non empty total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
s1 " is Relation-like NAT -defined Function-like non empty total complex-valued set
s (#) (s1 ") is Relation-like NAT -defined Function-like non empty total complex-valued set
((s /" s1)) is complex Element of COMPLEX
(s) / (s1) is complex Element of COMPLEX
s1 " is Relation-like NAT -defined COMPLEX -valued Function-like non empty total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
s (#) (s1 ") is Relation-like NAT -defined COMPLEX -valued Function-like non empty total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
((s (#) (s1 "))) is complex Element of COMPLEX
((s1 ")) is complex Element of COMPLEX
(s) * ((s1 ")) is complex Element of COMPLEX
(s1) " is complex Element of COMPLEX
(s) * ((s1) ") is complex Element of COMPLEX
s is Relation-like NAT -defined COMPLEX -valued Function-like non empty total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
(s) is complex Element of COMPLEX
(s) *' is complex Element of COMPLEX
s1 is Relation-like NAT -defined COMPLEX -valued Function-like non empty total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
(s1) is complex Element of COMPLEX
s /" s1 is Relation-like NAT -defined COMPLEX -valued Function-like non empty total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
s1 " is Relation-like NAT -defined Function-like non empty total complex-valued set
s (#) (s1 ") is Relation-like NAT -defined Function-like non empty total complex-valued set
(NAT,(s /" s1)) is Relation-like NAT -defined COMPLEX -valued Function-like non empty total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
((NAT,(s /" s1))) is complex Element of COMPLEX
(s1) *' is complex Element of COMPLEX
((s) *') / ((s1) *') is complex Element of COMPLEX
((s /" s1)) is complex Element of COMPLEX
((s /" s1)) *' is complex Element of COMPLEX
(s) / (s1) is complex Element of COMPLEX
((s) / (s1)) *' is complex Element of COMPLEX
s is Relation-like NAT -defined COMPLEX -valued Function-like non empty total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
(s) is complex Element of COMPLEX
s1 is Relation-like NAT -defined COMPLEX -valued Function-like non empty total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
s (#) s1 is Relation-like NAT -defined COMPLEX -valued Function-like non empty total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
R is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative V47() V48() V49() V50() V51() V52() V53() Element of COMPLEX
p is complex real ext-real Element of REAL
n1 is complex real ext-real Element of REAL
n1 / p is complex real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
(s (#) s1) . m is complex set
((s (#) s1) . m) - R is complex set
|.(((s (#) s1) . m) - R).| is complex real ext-real Element of REAL
(s (#) s1) . m is complex Element of COMPLEX
((s (#) s1) . m) - R is complex Element of COMPLEX
|.(((s (#) s1) . m) - R).| is complex real ext-real Element of REAL
s . m is complex Element of COMPLEX
s1 . m is complex Element of COMPLEX
(s . m) * (s1 . m) is complex Element of COMPLEX
|.((s . m) * (s1 . m)).| is complex real ext-real Element of REAL
|.(s . m).| is complex real ext-real Element of REAL
|.(s1 . m).| is complex real ext-real Element of REAL
|.(s . m).| * |.(s1 . m).| is complex real ext-real Element of REAL
(s . m) - 0c is complex Element of COMPLEX
|.((s . m) - 0c).| is complex real ext-real Element of REAL
(n1 / p) * p is complex real ext-real Element of REAL
p " is complex real ext-real Element of REAL
n1 * (p ") is complex real ext-real Element of REAL
(n1 * (p ")) * p is complex real ext-real Element of REAL
(p ") * p is complex real ext-real Element of REAL
n1 * ((p ") * p) is complex real ext-real Element of REAL
n1 * 1 is complex real ext-real Element of REAL
(n1 / p) * |.(s1 . m).| is complex real ext-real Element of REAL
s is Relation-like NAT -defined COMPLEX -valued Function-like non empty total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
(s) is complex Element of COMPLEX
s1 is Relation-like NAT -defined COMPLEX -valued Function-like non empty total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
s (#) s1 is Relation-like NAT -defined COMPLEX -valued Function-like non empty total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
((s (#) s1)) is complex Element of COMPLEX
R is complex real ext-real Element of REAL
p is complex real ext-real Element of REAL
p / R is complex real ext-real Element of REAL
n1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
(p / R) * R is complex real ext-real Element of REAL
R " is complex real ext-real Element of REAL
p * (R ") is complex real ext-real Element of REAL
(p * (R ")) * R is complex real ext-real Element of REAL
(R ") * R is complex real ext-real Element of REAL
p * ((R ") * R) is complex real ext-real Element of REAL
p * 1 is complex real ext-real Element of REAL
m is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
s1 . m is complex Element of COMPLEX
|.(s1 . m).| is complex real ext-real Element of REAL
(p / R) * |.(s1 . m).| is complex real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
s . m is complex Element of COMPLEX
(s . m) - 0c is complex Element of COMPLEX
|.((s . m) - 0c).| is complex real ext-real Element of REAL
(s (#) s1) . m is complex Element of COMPLEX
((s (#) s1) . m) - 0c is complex Element of COMPLEX
|.(((s (#) s1) . m) - 0c).| is complex real ext-real Element of REAL
(s . m) * (s1 . m) is complex Element of COMPLEX
|.((s . m) * (s1 . m)).| is complex real ext-real Element of REAL
|.(s . m).| is complex real ext-real Element of REAL
|.(s . m).| * |.(s1 . m).| is complex real ext-real Element of REAL
s is Relation-like NAT -defined COMPLEX -valued Function-like non empty total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
(s) is complex Element of COMPLEX
s1 is Relation-like NAT -defined COMPLEX -valued Function-like non empty total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
s (#) s1 is Relation-like NAT -defined COMPLEX -valued Function-like non empty total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
(NAT,(s (#) s1)) is Relation-like NAT -defined COMPLEX -valued Function-like non empty total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
((NAT,(s (#) s1))) is complex Element of COMPLEX
((s (#) s1)) is complex Element of COMPLEX
((s (#) s1)) *' is complex Element of COMPLEX