:: CSSPACE2 semantic presentation

REAL is non zero V52() V64() V65() V66() V70() set
NAT is non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() Element of bool REAL
bool REAL is non zero set
COMPLEX is non zero V52() V64() V70() set
NAT is non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() set
bool NAT is non zero set
bool NAT is non zero set
RAT is non zero V52() V64() V65() V66() V67() V70() set
INT is non zero V52() V64() V65() V66() V67() V68() V70() set
[:NAT,REAL:] is non zero V38() V39() V40() set
bool [:NAT,REAL:] is non zero set
[:NAT,COMPLEX:] is non zero V38() set
bool [:NAT,COMPLEX:] is non zero set
the_set_of_ComplexSequences is non zero set
[:the_set_of_ComplexSequences,the_set_of_ComplexSequences:] is non zero set
[:[:the_set_of_ComplexSequences,the_set_of_ComplexSequences:],the_set_of_ComplexSequences:] is non zero set
bool [:[:the_set_of_ComplexSequences,the_set_of_ComplexSequences:],the_set_of_ComplexSequences:] is non zero set
[:COMPLEX,the_set_of_ComplexSequences:] is non zero set
[:[:COMPLEX,the_set_of_ComplexSequences:],the_set_of_ComplexSequences:] is non zero set
bool [:[:COMPLEX,the_set_of_ComplexSequences:],the_set_of_ComplexSequences:] is non zero set
Linear_Space_of_ComplexSequences is V80() right_complementable V131() V132() V133() strict vector-distributive scalar-distributive scalar-associative scalar-unital L16()
the carrier of Linear_Space_of_ComplexSequences is non zero set
bool the carrier of Linear_Space_of_ComplexSequences is non zero set
the_set_of_l2ComplexSequences is Element of bool the carrier of Linear_Space_of_ComplexSequences
[:the_set_of_l2ComplexSequences,the_set_of_l2ComplexSequences:] is set
[:[:the_set_of_l2ComplexSequences,the_set_of_l2ComplexSequences:],COMPLEX:] is V38() set
bool [:[:the_set_of_l2ComplexSequences,the_set_of_l2ComplexSequences:],COMPLEX:] is non zero set
0 is zero V26() V27() V28() V30() V31() V32() complex ext-real non positive non negative V64() V65() V66() V67() V68() V69() V70() set
1 is non zero V26() V27() V28() V32() complex V34() ext-real positive non negative V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
0 is zero V26() V27() V28() V30() V31() V32() complex V34() ext-real non positive non negative V50() V63() V64() V65() V66() V67() V68() V69() V70() Element of NAT
CZeroseq is Element of the_set_of_ComplexSequences
0c is zero V26() V27() V28() V30() V31() V32() complex ext-real non positive non negative V64() V65() V66() V67() V68() V69() V70() Element of COMPLEX
l_add is Relation-like [:the_set_of_ComplexSequences,the_set_of_ComplexSequences:] -defined the_set_of_ComplexSequences -valued Function-like non zero V14([:the_set_of_ComplexSequences,the_set_of_ComplexSequences:]) V18([:the_set_of_ComplexSequences,the_set_of_ComplexSequences:], the_set_of_ComplexSequences ) Element of bool [:[:the_set_of_ComplexSequences,the_set_of_ComplexSequences:],the_set_of_ComplexSequences:]
l_mult is Relation-like [:COMPLEX,the_set_of_ComplexSequences:] -defined the_set_of_ComplexSequences -valued Function-like non zero V14([:COMPLEX,the_set_of_ComplexSequences:]) V18([:COMPLEX,the_set_of_ComplexSequences:], the_set_of_ComplexSequences ) Element of bool [:[:COMPLEX,the_set_of_ComplexSequences:],the_set_of_ComplexSequences:]
G16(the_set_of_ComplexSequences,CZeroseq,l_add,l_mult) is V131() strict L16()
Zero_ (the_set_of_l2ComplexSequences,Linear_Space_of_ComplexSequences) is Element of the_set_of_l2ComplexSequences
Add_ (the_set_of_l2ComplexSequences,Linear_Space_of_ComplexSequences) is Relation-like [:the_set_of_l2ComplexSequences,the_set_of_l2ComplexSequences:] -defined the_set_of_l2ComplexSequences -valued Function-like V18([:the_set_of_l2ComplexSequences,the_set_of_l2ComplexSequences:], the_set_of_l2ComplexSequences ) Element of bool [:[:the_set_of_l2ComplexSequences,the_set_of_l2ComplexSequences:],the_set_of_l2ComplexSequences:]
[:[:the_set_of_l2ComplexSequences,the_set_of_l2ComplexSequences:],the_set_of_l2ComplexSequences:] is set
bool [:[:the_set_of_l2ComplexSequences,the_set_of_l2ComplexSequences:],the_set_of_l2ComplexSequences:] is non zero set
Mult_ (the_set_of_l2ComplexSequences,Linear_Space_of_ComplexSequences) is Relation-like [:COMPLEX,the_set_of_l2ComplexSequences:] -defined the_set_of_l2ComplexSequences -valued Function-like V18([:COMPLEX,the_set_of_l2ComplexSequences:], the_set_of_l2ComplexSequences ) Element of bool [:[:COMPLEX,the_set_of_l2ComplexSequences:],the_set_of_l2ComplexSequences:]
[:COMPLEX,the_set_of_l2ComplexSequences:] is set
[:[:COMPLEX,the_set_of_l2ComplexSequences:],the_set_of_l2ComplexSequences:] is set
bool [:[:COMPLEX,the_set_of_l2ComplexSequences:],the_set_of_l2ComplexSequences:] is non zero set
G16(the_set_of_l2ComplexSequences,(Zero_ (the_set_of_l2ComplexSequences,Linear_Space_of_ComplexSequences)),(Add_ (the_set_of_l2ComplexSequences,Linear_Space_of_ComplexSequences)),(Mult_ (the_set_of_l2ComplexSequences,Linear_Space_of_ComplexSequences))) is strict L16()
cl_scalar is Relation-like [:the_set_of_l2ComplexSequences,the_set_of_l2ComplexSequences:] -defined COMPLEX -valued Function-like V14([:the_set_of_l2ComplexSequences,the_set_of_l2ComplexSequences:]) V18([:the_set_of_l2ComplexSequences,the_set_of_l2ComplexSequences:], COMPLEX ) V38() Element of bool [:[:the_set_of_l2ComplexSequences,the_set_of_l2ComplexSequences:],COMPLEX:]
Complex_l2_Space is V80() right_complementable V131() V132() V133() vector-distributive scalar-distributive scalar-associative scalar-unital CUNITSTR
CUNITSTR(# the_set_of_l2ComplexSequences,(Zero_ (the_set_of_l2ComplexSequences,Linear_Space_of_ComplexSequences)),(Add_ (the_set_of_l2ComplexSequences,Linear_Space_of_ComplexSequences)),(Mult_ (the_set_of_l2ComplexSequences,Linear_Space_of_ComplexSequences)),cl_scalar #) is V80() strict CUNITSTR
1r is complex Element of COMPLEX
- 1r is complex Element of COMPLEX
<i> is complex Element of COMPLEX
Re 0 is complex V34() ext-real Element of REAL
Im 0 is complex V34() ext-real Element of REAL
2 is non zero V26() V27() V28() V32() complex V34() ext-real positive non negative V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
seq is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
seq *' is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
Partial_Sums (seq *') is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
Partial_Sums seq is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
(Partial_Sums seq) *' is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
n is V26() V27() V28() V32() complex V34() ext-real V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
(Partial_Sums (seq *')) . n is complex Element of COMPLEX
((Partial_Sums seq) *') . n is complex Element of COMPLEX
n + 1 is V26() V27() V28() V32() complex V34() ext-real V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
(Partial_Sums (seq *')) . (n + 1) is complex Element of COMPLEX
(seq *') . (n + 1) is complex Element of COMPLEX
((Partial_Sums (seq *')) . n) + ((seq *') . (n + 1)) is complex Element of COMPLEX
seq . (n + 1) is complex Element of COMPLEX
(seq . (n + 1)) *' is complex Element of COMPLEX
(((Partial_Sums seq) *') . n) + ((seq . (n + 1)) *') is complex Element of COMPLEX
(Partial_Sums seq) . n is complex Element of COMPLEX
((Partial_Sums seq) . n) *' is complex Element of COMPLEX
(((Partial_Sums seq) . n) *') + ((seq . (n + 1)) *') is complex Element of COMPLEX
((Partial_Sums seq) . n) + (seq . (n + 1)) is complex Element of COMPLEX
(((Partial_Sums seq) . n) + (seq . (n + 1))) *' is complex Element of COMPLEX
(Partial_Sums seq) . (n + 1) is complex Element of COMPLEX
((Partial_Sums seq) . (n + 1)) *' is complex Element of COMPLEX
((Partial_Sums seq) *') . (n + 1) is complex Element of COMPLEX
(Partial_Sums (seq *')) . 0 is complex Element of COMPLEX
(seq *') . 0 is complex Element of COMPLEX
seq . 0 is complex Element of COMPLEX
(seq . 0) *' is complex Element of COMPLEX
(Partial_Sums seq) . 0 is complex Element of COMPLEX
((Partial_Sums seq) . 0) *' is complex Element of COMPLEX
((Partial_Sums seq) *') . 0 is complex Element of COMPLEX
seq is complex V34() ext-real Element of REAL
seq ^2 is complex V34() ext-real Element of REAL
seq * seq is complex set
n is complex V34() ext-real Element of REAL
n ^2 is complex V34() ext-real Element of REAL
n * n is complex set
(seq ^2) + (n ^2) is complex V34() ext-real Element of REAL
0 + 0 is V26() V27() V28() V32() complex V34() ext-real V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
seq is complex set
Re seq is complex V34() ext-real Element of REAL
n is complex set
Im n is complex V34() ext-real Element of REAL
(Re seq) * (Im n) is complex V34() ext-real Element of REAL
Re n is complex V34() ext-real Element of REAL
Im seq is complex V34() ext-real Element of REAL
(Re n) * (Im seq) is complex V34() ext-real Element of REAL
(Re seq) * (Re n) is complex V34() ext-real Element of REAL
(Im seq) * (Im n) is complex V34() ext-real Element of REAL
((Re seq) * (Re n)) + ((Im seq) * (Im n)) is complex V34() ext-real Element of REAL
seq + n is complex set
|.(seq + n).| is complex V34() ext-real Element of REAL
|.seq.| is complex V34() ext-real Element of REAL
|.n.| is complex V34() ext-real Element of REAL
|.seq.| + |.n.| is complex V34() ext-real Element of REAL
Re (seq + n) is complex V34() ext-real Element of REAL
(Re (seq + n)) ^2 is complex V34() ext-real Element of REAL
(Re (seq + n)) * (Re (seq + n)) is complex set
(Re seq) + (Re n) is complex V34() ext-real Element of REAL
((Re seq) + (Re n)) ^2 is complex V34() ext-real Element of REAL
((Re seq) + (Re n)) * ((Re seq) + (Re n)) is complex set
(Re seq) ^2 is complex V34() ext-real Element of REAL
(Re seq) * (Re seq) is complex set
2 * (Re seq) is complex V34() ext-real Element of REAL
(2 * (Re seq)) * (Re n) is complex V34() ext-real Element of REAL
((Re seq) ^2) + ((2 * (Re seq)) * (Re n)) is complex V34() ext-real Element of REAL
(Re n) ^2 is complex V34() ext-real Element of REAL
(Re n) * (Re n) is complex set
(((Re seq) ^2) + ((2 * (Re seq)) * (Re n))) + ((Re n) ^2) is complex V34() ext-real Element of REAL
abs (((Re seq) * (Re n)) + ((Im seq) * (Im n))) is complex V34() ext-real Element of REAL
(((Re seq) * (Re n)) + ((Im seq) * (Im n))) ^2 is complex V34() ext-real Element of REAL
(((Re seq) * (Re n)) + ((Im seq) * (Im n))) * (((Re seq) * (Re n)) + ((Im seq) * (Im n))) is complex set
sqrt ((((Re seq) * (Re n)) + ((Im seq) * (Im n))) ^2) is complex V34() ext-real Element of REAL
Im (seq + n) is complex V34() ext-real Element of REAL
(Im (seq + n)) ^2 is complex V34() ext-real Element of REAL
(Im (seq + n)) * (Im (seq + n)) is complex set
(Im seq) + (Im n) is complex V34() ext-real Element of REAL
((Im seq) + (Im n)) ^2 is complex V34() ext-real Element of REAL
((Im seq) + (Im n)) * ((Im seq) + (Im n)) is complex set
(Im seq) ^2 is complex V34() ext-real Element of REAL
(Im seq) * (Im seq) is complex set
2 * (Im seq) is complex V34() ext-real Element of REAL
(2 * (Im seq)) * (Im n) is complex V34() ext-real Element of REAL
((Im seq) ^2) + ((2 * (Im seq)) * (Im n)) is complex V34() ext-real Element of REAL
(Im n) ^2 is complex V34() ext-real Element of REAL
(Im n) * (Im n) is complex set
(((Im seq) ^2) + ((2 * (Im seq)) * (Im n))) + ((Im n) ^2) is complex V34() ext-real Element of REAL
((Re n) ^2) + ((Im n) ^2) is complex V34() ext-real Element of REAL
sqrt (((Re n) ^2) + ((Im n) ^2)) is complex V34() ext-real Element of REAL
(sqrt (((Re n) ^2) + ((Im n) ^2))) ^2 is complex V34() ext-real Element of REAL
(sqrt (((Re n) ^2) + ((Im n) ^2))) * (sqrt (((Re n) ^2) + ((Im n) ^2))) is complex set
((Re seq) ^2) + ((Im seq) ^2) is complex V34() ext-real Element of REAL
sqrt (((Re seq) ^2) + ((Im seq) ^2)) is complex V34() ext-real Element of REAL
0 + 0 is V26() V27() V28() V32() complex V34() ext-real V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
(sqrt (((Re seq) ^2) + ((Im seq) ^2))) + (sqrt (((Re n) ^2) + ((Im n) ^2))) is complex V34() ext-real Element of REAL
(((Re seq) ^2) + ((Im seq) ^2)) * (((Re n) ^2) + ((Im n) ^2)) is complex V34() ext-real Element of REAL
((((Re seq) ^2) + ((Im seq) ^2)) * (((Re n) ^2) + ((Im n) ^2))) - ((((Re seq) * (Re n)) + ((Im seq) * (Im n))) ^2) is complex V34() ext-real Element of REAL
(Im seq) * (Re n) is complex V34() ext-real Element of REAL
((Re seq) * (Im n)) - ((Im seq) * (Re n)) is complex V34() ext-real Element of REAL
(((Re seq) * (Im n)) - ((Im seq) * (Re n))) ^2 is complex V34() ext-real Element of REAL
(((Re seq) * (Im n)) - ((Im seq) * (Re n))) * (((Re seq) * (Im n)) - ((Im seq) * (Re n))) is complex set
sqrt ((((Re seq) ^2) + ((Im seq) ^2)) * (((Re n) ^2) + ((Im n) ^2))) is complex V34() ext-real Element of REAL
(sqrt (((Re seq) ^2) + ((Im seq) ^2))) * (sqrt (((Re n) ^2) + ((Im n) ^2))) is complex V34() ext-real Element of REAL
(sqrt (((Re seq) ^2) + ((Im seq) ^2))) ^2 is complex V34() ext-real Element of REAL
(sqrt (((Re seq) ^2) + ((Im seq) ^2))) * (sqrt (((Re seq) ^2) + ((Im seq) ^2))) is complex set
((Re (seq + n)) ^2) + ((Im (seq + n)) ^2) is complex V34() ext-real Element of REAL
sqrt (((Re (seq + n)) ^2) + ((Im (seq + n)) ^2)) is complex V34() ext-real Element of REAL
((sqrt (((Re seq) ^2) + ((Im seq) ^2))) + (sqrt (((Re n) ^2) + ((Im n) ^2)))) ^2 is complex V34() ext-real Element of REAL
((sqrt (((Re seq) ^2) + ((Im seq) ^2))) + (sqrt (((Re n) ^2) + ((Im n) ^2)))) * ((sqrt (((Re seq) ^2) + ((Im seq) ^2))) + (sqrt (((Re n) ^2) + ((Im n) ^2)))) is complex set
sqrt (((sqrt (((Re seq) ^2) + ((Im seq) ^2))) + (sqrt (((Re n) ^2) + ((Im n) ^2)))) ^2) is complex V34() ext-real Element of REAL
(sqrt (((Re seq) ^2) + ((Im seq) ^2))) + |.n.| is complex V34() ext-real Element of REAL
seq is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
Re seq is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
Im seq is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
Partial_Sums seq is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
|.(Partial_Sums seq).| is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
|.seq.| is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
Partial_Sums |.seq.| is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() V44() Element of bool [:NAT,REAL:]
n is V26() V27() V28() V32() complex V34() ext-real V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
|.(Partial_Sums seq).| . n is complex V34() ext-real Element of REAL
(Partial_Sums |.seq.|) . n is complex V34() ext-real Element of REAL
nn is V26() V27() V28() V32() complex V34() ext-real V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
|.(Partial_Sums seq).| . nn is complex V34() ext-real Element of REAL
(Partial_Sums |.seq.|) . nn is complex V34() ext-real Element of REAL
nn + 1 is V26() V27() V28() V32() complex V34() ext-real V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
|.(Partial_Sums seq).| . (nn + 1) is complex V34() ext-real Element of REAL
(Partial_Sums |.seq.|) . (nn + 1) is complex V34() ext-real Element of REAL
Partial_Sums (Re seq) is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
seqt is V26() V27() V28() V32() complex V34() ext-real V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
(Partial_Sums (Re seq)) . seqt is complex V34() ext-real Element of REAL
tv is V26() V27() V28() V32() complex V34() ext-real V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
(Partial_Sums (Re seq)) . tv is complex V34() ext-real Element of REAL
tv + 1 is V26() V27() V28() V32() complex V34() ext-real V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
(Partial_Sums (Re seq)) . (tv + 1) is complex V34() ext-real Element of REAL
(Re seq) . (tv + 1) is complex V34() ext-real Element of REAL
((Partial_Sums (Re seq)) . tv) + ((Re seq) . (tv + 1)) is complex V34() ext-real Element of REAL
0 + 0 is V26() V27() V28() V32() complex V34() ext-real V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
(Partial_Sums (Re seq)) . 0 is complex V34() ext-real Element of REAL
(Re seq) . 0 is complex V34() ext-real Element of REAL
(Partial_Sums (Re seq)) . nn is complex V34() ext-real Element of REAL
Re (Partial_Sums seq) is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
(Re (Partial_Sums seq)) . nn is complex V34() ext-real Element of REAL
(Partial_Sums seq) . nn is complex Element of COMPLEX
Re ((Partial_Sums seq) . nn) is complex V34() ext-real Element of REAL
seq . (nn + 1) is complex Element of COMPLEX
(Partial_Sums seq) . (nn + 1) is complex Element of COMPLEX
|.((Partial_Sums seq) . (nn + 1)).| is complex V34() ext-real Element of REAL
((Partial_Sums seq) . nn) + (seq . (nn + 1)) is complex Element of COMPLEX
|.(((Partial_Sums seq) . nn) + (seq . (nn + 1))).| is complex V34() ext-real Element of REAL
Partial_Sums (Im seq) is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
e is V26() V27() V28() V32() complex V34() ext-real V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
(Partial_Sums (Im seq)) . e is complex V34() ext-real Element of REAL
m is V26() V27() V28() V32() complex V34() ext-real V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
m + 1 is V26() V27() V28() V32() complex V34() ext-real V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
(Partial_Sums (Im seq)) . (m + 1) is complex V34() ext-real Element of REAL
(Partial_Sums (Im seq)) . m is complex V34() ext-real Element of REAL
(Im seq) . (m + 1) is complex V34() ext-real Element of REAL
((Partial_Sums (Im seq)) . m) + ((Im seq) . (m + 1)) is complex V34() ext-real Element of REAL
(Partial_Sums (Im seq)) . 0 is complex V34() ext-real Element of REAL
(Im seq) . 0 is complex V34() ext-real Element of REAL
(Partial_Sums (Im seq)) . nn is complex V34() ext-real Element of REAL
Im (Partial_Sums seq) is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
(Im (Partial_Sums seq)) . nn is complex V34() ext-real Element of REAL
Im ((Partial_Sums seq) . nn) is complex V34() ext-real Element of REAL
(Im seq) . (nn + 1) is complex V34() ext-real Element of REAL
Im (seq . (nn + 1)) is complex V34() ext-real Element of REAL
(Re ((Partial_Sums seq) . nn)) * (Im (seq . (nn + 1))) is complex V34() ext-real Element of REAL
Re (seq . (nn + 1)) is complex V34() ext-real Element of REAL
(Re (seq . (nn + 1))) * (Im ((Partial_Sums seq) . nn)) is complex V34() ext-real Element of REAL
(Re seq) . (nn + 1) is complex V34() ext-real Element of REAL
(Re ((Partial_Sums seq) . nn)) * (Re (seq . (nn + 1))) is complex V34() ext-real Element of REAL
(Im ((Partial_Sums seq) . nn)) * (Im (seq . (nn + 1))) is complex V34() ext-real Element of REAL
((Re ((Partial_Sums seq) . nn)) * (Re (seq . (nn + 1)))) + ((Im ((Partial_Sums seq) . nn)) * (Im (seq . (nn + 1)))) is complex V34() ext-real Element of REAL
|.((Partial_Sums seq) . nn).| is complex V34() ext-real Element of REAL
|.(seq . (nn + 1)).| is complex V34() ext-real Element of REAL
|.((Partial_Sums seq) . nn).| + |.(seq . (nn + 1)).| is complex V34() ext-real Element of REAL
(|.(Partial_Sums seq).| . nn) + |.(seq . (nn + 1)).| is complex V34() ext-real Element of REAL
|.seq.| . (nn + 1) is complex V34() ext-real Element of REAL
((Partial_Sums |.seq.|) . nn) + (|.seq.| . (nn + 1)) is complex V34() ext-real Element of REAL
|.(Partial_Sums seq).| . 0 is complex V34() ext-real Element of REAL
(Partial_Sums seq) . 0 is complex Element of COMPLEX
|.((Partial_Sums seq) . 0).| is complex V34() ext-real Element of REAL
seq . 0 is complex Element of COMPLEX
|.(seq . 0).| is complex V34() ext-real Element of REAL
|.seq.| . 0 is complex V34() ext-real Element of REAL
(Partial_Sums |.seq.|) . 0 is complex V34() ext-real Element of REAL
seq is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
seq *' is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
Sum (seq *') is complex Element of COMPLEX
Sum seq is complex Element of COMPLEX
(Sum seq) *' is complex Element of COMPLEX
Partial_Sums (seq *') is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
lim (Partial_Sums (seq *')) is complex Element of COMPLEX
Partial_Sums seq is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
(Partial_Sums seq) *' is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
lim ((Partial_Sums seq) *') is complex Element of COMPLEX
lim (Partial_Sums seq) is complex Element of COMPLEX
(lim (Partial_Sums seq)) *' is complex Element of COMPLEX
seq is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
Sum seq is complex Element of COMPLEX
|.(Sum seq).| is complex V34() ext-real Element of REAL
|.seq.| is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
Sum |.seq.| is complex V34() ext-real Element of REAL
Partial_Sums seq is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
|.(Partial_Sums seq).| is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
Partial_Sums |.seq.| is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() V44() Element of bool [:NAT,REAL:]
n is V26() V27() V28() V32() complex V34() ext-real V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
|.(Partial_Sums seq).| . n is complex V34() ext-real Element of REAL
(Partial_Sums |.seq.|) . n is complex V34() ext-real Element of REAL
(Partial_Sums seq) . n is complex Element of COMPLEX
|.((Partial_Sums seq) . n).| is complex V34() ext-real Element of REAL
lim (Partial_Sums seq) is complex Element of COMPLEX
|.(lim (Partial_Sums seq)).| is complex V34() ext-real Element of REAL
lim |.(Partial_Sums seq).| is complex V34() ext-real Element of REAL
n is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() bounded convergent Element of bool [:NAT,COMPLEX:]
|.n.| is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() bounded convergent bounded_above bounded_below Element of bool [:NAT,REAL:]
lim (Partial_Sums |.seq.|) is complex V34() ext-real Element of REAL
seq is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
Re seq is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
Im seq is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
Sum seq is complex Element of COMPLEX
|.(Sum seq).| is complex V34() ext-real Element of REAL
|.seq.| is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
Sum |.seq.| is complex V34() ext-real Element of REAL
Partial_Sums seq is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
|.(Partial_Sums seq).| is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
Partial_Sums |.seq.| is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() V44() Element of bool [:NAT,REAL:]
n is set
|.(Partial_Sums seq).| . n is complex V34() ext-real Element of REAL
(Partial_Sums |.seq.|) . n is complex V34() ext-real Element of REAL
lim |.(Partial_Sums seq).| is complex V34() ext-real Element of REAL
lim (Partial_Sums seq) is complex Element of COMPLEX
|.(lim (Partial_Sums seq)).| is complex V34() ext-real Element of REAL
seq is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
seq *' is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
seq (#) (seq *') is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
Re (seq (#) (seq *')) is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
Im (seq (#) (seq *')) is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
n is V26() V27() V28() V32() complex V34() ext-real V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
(Re (seq (#) (seq *'))) . n is complex V34() ext-real Element of REAL
(Im (seq (#) (seq *'))) . n is complex V34() ext-real Element of REAL
seq . n is complex Element of COMPLEX
nn is complex Element of COMPLEX
Re nn is complex V34() ext-real Element of REAL
(Re nn) ^2 is complex V34() ext-real Element of REAL
(Re nn) * (Re nn) is complex set
Im nn is complex V34() ext-real Element of REAL
(Im nn) ^2 is complex V34() ext-real Element of REAL
(Im nn) * (Im nn) is complex set
(seq (#) (seq *')) . n is complex Element of COMPLEX
Re ((seq (#) (seq *')) . n) is complex V34() ext-real Element of REAL
(seq *') . n is complex Element of COMPLEX
(seq . n) * ((seq *') . n) is complex Element of COMPLEX
Re ((seq . n) * ((seq *') . n)) is complex V34() ext-real Element of REAL
(seq . n) *' is complex Element of COMPLEX
(seq . n) * ((seq . n) *') is complex Element of COMPLEX
Re ((seq . n) * ((seq . n) *')) is complex V34() ext-real Element of REAL
((Re nn) ^2) + ((Im nn) ^2) is complex V34() ext-real Element of REAL
0 + 0 is V26() V27() V28() V32() complex V34() ext-real V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
Im ((seq (#) (seq *')) . n) is complex V34() ext-real Element of REAL
Im ((seq . n) * ((seq *') . n)) is complex V34() ext-real Element of REAL
Im ((seq . n) * ((seq . n) *')) is complex V34() ext-real Element of REAL
the carrier of Complex_l2_Space is non zero set
seq is set
seq_id seq is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
|.(seq_id seq).| is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
|.(seq_id seq).| (#) |.(seq_id seq).| is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
seq is set
seq_id seq is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
|.(seq_id seq).| is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
|.(seq_id seq).| (#) |.(seq_id seq).| is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
n is set
seq_id n is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
|.(seq_id n).| is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
|.(seq_id n).| (#) |.(seq_id n).| is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
0. Complex_l2_Space is zero Element of the carrier of Complex_l2_Space
the ZeroF of Complex_l2_Space is Element of the carrier of Complex_l2_Space
0. Linear_Space_of_ComplexSequences is zero Element of the carrier of Linear_Space_of_ComplexSequences
the ZeroF of Linear_Space_of_ComplexSequences is Element of the carrier of Linear_Space_of_ComplexSequences
seq is Element of the carrier of Complex_l2_Space
seq_id seq is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
nn is Element of the carrier of Complex_l2_Space
seqt is Element of the carrier of Complex_l2_Space
nn + seqt is Element of the carrier of Complex_l2_Space
the addF of Complex_l2_Space is Relation-like [: the carrier of Complex_l2_Space, the carrier of Complex_l2_Space:] -defined the carrier of Complex_l2_Space -valued Function-like non zero V14([: the carrier of Complex_l2_Space, the carrier of Complex_l2_Space:]) V18([: the carrier of Complex_l2_Space, the carrier of Complex_l2_Space:], the carrier of Complex_l2_Space) Element of bool [:[: the carrier of Complex_l2_Space, the carrier of Complex_l2_Space:], the carrier of Complex_l2_Space:]
[: the carrier of Complex_l2_Space, the carrier of Complex_l2_Space:] is non zero set
[:[: the carrier of Complex_l2_Space, the carrier of Complex_l2_Space:], the carrier of Complex_l2_Space:] is non zero set
bool [:[: the carrier of Complex_l2_Space, the carrier of Complex_l2_Space:], the carrier of Complex_l2_Space:] is non zero set
the addF of Complex_l2_Space . (nn,seqt) is Element of the carrier of Complex_l2_Space
K88(nn,seqt) is set
the addF of Complex_l2_Space . K88(nn,seqt) is set
seq_id nn is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
seq_id seqt is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
(seq_id nn) + (seq_id seqt) is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
the addF of Linear_Space_of_ComplexSequences is Relation-like [: the carrier of Linear_Space_of_ComplexSequences, the carrier of Linear_Space_of_ComplexSequences:] -defined the carrier of Linear_Space_of_ComplexSequences -valued Function-like non zero V14([: the carrier of Linear_Space_of_ComplexSequences, the carrier of Linear_Space_of_ComplexSequences:]) V18([: the carrier of Linear_Space_of_ComplexSequences, the carrier of Linear_Space_of_ComplexSequences:], the carrier of Linear_Space_of_ComplexSequences) Element of bool [:[: the carrier of Linear_Space_of_ComplexSequences, the carrier of Linear_Space_of_ComplexSequences:], the carrier of Linear_Space_of_ComplexSequences:]
[: the carrier of Linear_Space_of_ComplexSequences, the carrier of Linear_Space_of_ComplexSequences:] is non zero set
[:[: the carrier of Linear_Space_of_ComplexSequences, the carrier of Linear_Space_of_ComplexSequences:], the carrier of Linear_Space_of_ComplexSequences:] is non zero set
bool [:[: the carrier of Linear_Space_of_ComplexSequences, the carrier of Linear_Space_of_ComplexSequences:], the carrier of Linear_Space_of_ComplexSequences:] is non zero set
dom the addF of Linear_Space_of_ComplexSequences is Relation-like set
the addF of Linear_Space_of_ComplexSequences || the_set_of_l2ComplexSequences is Relation-like Function-like set
the addF of Linear_Space_of_ComplexSequences | [:the_set_of_l2ComplexSequences,the_set_of_l2ComplexSequences:] is Relation-like set
dom ( the addF of Linear_Space_of_ComplexSequences || the_set_of_l2ComplexSequences) is set
[nn,seqt] is Element of [: the carrier of Complex_l2_Space, the carrier of Complex_l2_Space:]
( the addF of Linear_Space_of_ComplexSequences || the_set_of_l2ComplexSequences) . [nn,seqt] is set
tv is Element of the carrier of Linear_Space_of_ComplexSequences
e is Element of the carrier of Linear_Space_of_ComplexSequences
tv + e is Element of the carrier of Linear_Space_of_ComplexSequences
the addF of Linear_Space_of_ComplexSequences . (tv,e) is Element of the carrier of Linear_Space_of_ComplexSequences
K88(tv,e) is set
the addF of Linear_Space_of_ComplexSequences . K88(tv,e) is set
nn is complex set
seqt is Element of the carrier of Complex_l2_Space
nn * seqt is Element of the carrier of Complex_l2_Space
seq_id seqt is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
nn (#) (seq_id seqt) is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
the Mult of Linear_Space_of_ComplexSequences is Relation-like [:COMPLEX, the carrier of Linear_Space_of_ComplexSequences:] -defined the carrier of Linear_Space_of_ComplexSequences -valued Function-like non zero V14([:COMPLEX, the carrier of Linear_Space_of_ComplexSequences:]) V18([:COMPLEX, the carrier of Linear_Space_of_ComplexSequences:], the carrier of Linear_Space_of_ComplexSequences) Element of bool [:[:COMPLEX, the carrier of Linear_Space_of_ComplexSequences:], the carrier of Linear_Space_of_ComplexSequences:]
[:COMPLEX, the carrier of Linear_Space_of_ComplexSequences:] is non zero set
[:[:COMPLEX, the carrier of Linear_Space_of_ComplexSequences:], the carrier of Linear_Space_of_ComplexSequences:] is non zero set
bool [:[:COMPLEX, the carrier of Linear_Space_of_ComplexSequences:], the carrier of Linear_Space_of_ComplexSequences:] is non zero set
dom the Mult of Linear_Space_of_ComplexSequences is Relation-like set
the Mult of Linear_Space_of_ComplexSequences | [:COMPLEX,the_set_of_l2ComplexSequences:] is Relation-like [:COMPLEX, the carrier of Linear_Space_of_ComplexSequences:] -defined the carrier of Linear_Space_of_ComplexSequences -valued Function-like Element of bool [:[:COMPLEX, the carrier of Linear_Space_of_ComplexSequences:], the carrier of Linear_Space_of_ComplexSequences:]
dom ( the Mult of Linear_Space_of_ComplexSequences | [:COMPLEX,the_set_of_l2ComplexSequences:]) is Relation-like set
e is complex Element of COMPLEX
e * seqt is Element of the carrier of Complex_l2_Space
[:COMPLEX, the carrier of Complex_l2_Space:] is non zero set
the Mult of Complex_l2_Space is Relation-like [:COMPLEX, the carrier of Complex_l2_Space:] -defined the carrier of Complex_l2_Space -valued Function-like non zero V14([:COMPLEX, the carrier of Complex_l2_Space:]) V18([:COMPLEX, the carrier of Complex_l2_Space:], the carrier of Complex_l2_Space) Element of bool [:[:COMPLEX, the carrier of Complex_l2_Space:], the carrier of Complex_l2_Space:]
[:[:COMPLEX, the carrier of Complex_l2_Space:], the carrier of Complex_l2_Space:] is non zero set
bool [:[:COMPLEX, the carrier of Complex_l2_Space:], the carrier of Complex_l2_Space:] is non zero set
[e,seqt] is Element of [:COMPLEX, the carrier of Complex_l2_Space:]
the Mult of Complex_l2_Space . [e,seqt] is Element of the carrier of Complex_l2_Space
( the Mult of Linear_Space_of_ComplexSequences | [:COMPLEX,the_set_of_l2ComplexSequences:]) . [e,seqt] is set
the Mult of Linear_Space_of_ComplexSequences . [e,seqt] is set
tv is Element of the carrier of Linear_Space_of_ComplexSequences
e * tv is Element of the carrier of Linear_Space_of_ComplexSequences
seq is Element of the carrier of Complex_l2_Space
- seq is Element of the carrier of Complex_l2_Space
seq_id seq is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
- (seq_id seq) is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
- 1 is non zero complex set
(- 1) (#) (seq_id seq) is Relation-like NAT -defined Function-like V14( NAT ) V38() set
seq_id (- seq) is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
(- 1r) * seq is Element of the carrier of Complex_l2_Space
(- 1r) (#) (seq_id seq) is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
seq is Element of the carrier of Complex_l2_Space
n is Element of the carrier of Complex_l2_Space
seq - n is Element of the carrier of Complex_l2_Space
- n is Element of the carrier of Complex_l2_Space
seq + (- n) is Element of the carrier of Complex_l2_Space
the addF of Complex_l2_Space is Relation-like [: the carrier of Complex_l2_Space, the carrier of Complex_l2_Space:] -defined the carrier of Complex_l2_Space -valued Function-like non zero V14([: the carrier of Complex_l2_Space, the carrier of Complex_l2_Space:]) V18([: the carrier of Complex_l2_Space, the carrier of Complex_l2_Space:], the carrier of Complex_l2_Space) Element of bool [:[: the carrier of Complex_l2_Space, the carrier of Complex_l2_Space:], the carrier of Complex_l2_Space:]
[: the carrier of Complex_l2_Space, the carrier of Complex_l2_Space:] is non zero set
[:[: the carrier of Complex_l2_Space, the carrier of Complex_l2_Space:], the carrier of Complex_l2_Space:] is non zero set
bool [:[: the carrier of Complex_l2_Space, the carrier of Complex_l2_Space:], the carrier of Complex_l2_Space:] is non zero set
the addF of Complex_l2_Space . (seq,(- n)) is Element of the carrier of Complex_l2_Space
K88(seq,(- n)) is set
the addF of Complex_l2_Space . K88(seq,(- n)) is set
seq_id seq is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
seq_id n is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
(seq_id seq) - (seq_id n) is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
- (seq_id n) is Relation-like NAT -defined Function-like V14( NAT ) V38() set
- 1 is non zero complex set
(- 1) (#) (seq_id n) is Relation-like NAT -defined Function-like V14( NAT ) V38() set
(seq_id seq) + (- (seq_id n)) is Relation-like NAT -defined Function-like V14( NAT ) V38() set
seq_id (- n) is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
(seq_id seq) + (seq_id (- n)) is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
1 / 2 is non zero complex V34() ext-real Element of REAL
n is Element of the carrier of Complex_l2_Space
seq_id n is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
|.(seq_id n).| is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
nn is Element of the carrier of Complex_l2_Space
seq_id nn is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
|.(seq_id nn).| is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
|.(seq_id n).| (#) |.(seq_id nn).| is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
|.(seq_id nn).| (#) |.(seq_id nn).| is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
|.(seq_id n).| (#) |.(seq_id n).| is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
abs (|.(seq_id n).| (#) |.(seq_id nn).|) is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
2 (#) (abs (|.(seq_id n).| (#) |.(seq_id nn).|)) is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
u is V26() V27() V28() V32() complex V34() ext-real V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
(2 (#) (abs (|.(seq_id n).| (#) |.(seq_id nn).|))) . u is complex V34() ext-real Element of REAL
(|.(seq_id n).| (#) |.(seq_id nn).|) . u is complex V34() ext-real Element of REAL
abs ((|.(seq_id n).| (#) |.(seq_id nn).|) . u) is complex V34() ext-real Element of REAL
n is complex V34() ext-real Element of REAL
(abs (|.(seq_id n).| (#) |.(seq_id nn).|)) . u is complex V34() ext-real Element of REAL
2 * ((abs (|.(seq_id n).| (#) |.(seq_id nn).|)) . u) is complex V34() ext-real Element of REAL
2 * (abs ((|.(seq_id n).| (#) |.(seq_id nn).|) . u)) is complex V34() ext-real Element of REAL
(|.(seq_id nn).| (#) |.(seq_id nn).|) + (|.(seq_id n).| (#) |.(seq_id n).|) is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
n is V26() V27() V28() V32() complex V34() ext-real V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
(2 (#) (abs (|.(seq_id n).| (#) |.(seq_id nn).|))) . n is complex V34() ext-real Element of REAL
((|.(seq_id nn).| (#) |.(seq_id nn).|) + (|.(seq_id n).| (#) |.(seq_id n).|)) . n is complex V34() ext-real Element of REAL
(seq_id nn) . n is complex Element of COMPLEX
|.((seq_id nn) . n).| is complex V34() ext-real Element of REAL
(seq_id n) . n is complex Element of COMPLEX
|.((seq_id n) . n).| is complex V34() ext-real Element of REAL
v is complex V34() ext-real Element of REAL
abs v is complex V34() ext-real Element of REAL
seqvn is complex V34() ext-real Element of REAL
abs seqvn is complex V34() ext-real Element of REAL
(|.(seq_id nn).| (#) |.(seq_id nn).|) . n is complex V34() ext-real Element of REAL
(|.(seq_id n).| (#) |.(seq_id n).|) . n is complex V34() ext-real Element of REAL
((|.(seq_id nn).| (#) |.(seq_id nn).|) . n) + ((|.(seq_id n).| (#) |.(seq_id n).|) . n) is complex V34() ext-real Element of REAL
|.(seq_id nn).| . n is complex V34() ext-real Element of REAL
(|.(seq_id nn).| . n) * (|.(seq_id nn).| . n) is complex V34() ext-real Element of REAL
((|.(seq_id nn).| . n) * (|.(seq_id nn).| . n)) + ((|.(seq_id n).| (#) |.(seq_id n).|) . n) is complex V34() ext-real Element of REAL
|.(seq_id n).| . n is complex V34() ext-real Element of REAL
(|.(seq_id n).| . n) * (|.(seq_id n).| . n) is complex V34() ext-real Element of REAL
((|.(seq_id nn).| . n) * (|.(seq_id nn).| . n)) + ((|.(seq_id n).| . n) * (|.(seq_id n).| . n)) is complex V34() ext-real Element of REAL
|.((seq_id nn) . n).| * (|.(seq_id nn).| . n) is complex V34() ext-real Element of REAL
(|.((seq_id nn) . n).| * (|.(seq_id nn).| . n)) + ((|.(seq_id n).| . n) * (|.(seq_id n).| . n)) is complex V34() ext-real Element of REAL
v ^2 is complex V34() ext-real Element of REAL
v * v is complex set
(v ^2) + ((|.(seq_id n).| . n) * (|.(seq_id n).| . n)) is complex V34() ext-real Element of REAL
|.((seq_id n) . n).| * (|.(seq_id n).| . n) is complex V34() ext-real Element of REAL
(v ^2) + (|.((seq_id n) . n).| * (|.(seq_id n).| . n)) is complex V34() ext-real Element of REAL
(abs v) ^2 is complex V34() ext-real Element of REAL
(abs v) * (abs v) is complex set
(abs seqvn) ^2 is complex V34() ext-real Element of REAL
(abs seqvn) * (abs seqvn) is complex set
((abs v) ^2) + ((abs seqvn) ^2) is complex V34() ext-real Element of REAL
(abs v) - (abs seqvn) is complex V34() ext-real Element of REAL
((abs v) - (abs seqvn)) ^2 is complex V34() ext-real Element of REAL
((abs v) - (abs seqvn)) * ((abs v) - (abs seqvn)) is complex set
(abs (|.(seq_id n).| (#) |.(seq_id nn).|)) . n is complex V34() ext-real Element of REAL
2 * ((abs (|.(seq_id n).| (#) |.(seq_id nn).|)) . n) is complex V34() ext-real Element of REAL
(|.(seq_id n).| (#) |.(seq_id nn).|) . n is complex V34() ext-real Element of REAL
abs ((|.(seq_id n).| (#) |.(seq_id nn).|) . n) is complex V34() ext-real Element of REAL
2 * (abs ((|.(seq_id n).| (#) |.(seq_id nn).|) . n)) is complex V34() ext-real Element of REAL
(|.(seq_id n).| . n) * (|.(seq_id nn).| . n) is complex V34() ext-real Element of REAL
abs ((|.(seq_id n).| . n) * (|.(seq_id nn).| . n)) is complex V34() ext-real Element of REAL
2 * (abs ((|.(seq_id n).| . n) * (|.(seq_id nn).| . n))) is complex V34() ext-real Element of REAL
abs (|.(seq_id n).| . n) is complex V34() ext-real Element of REAL
abs (|.(seq_id nn).| . n) is complex V34() ext-real Element of REAL
(abs (|.(seq_id n).| . n)) * (abs (|.(seq_id nn).| . n)) is complex V34() ext-real Element of REAL
2 * ((abs (|.(seq_id n).| . n)) * (abs (|.(seq_id nn).| . n))) is complex V34() ext-real Element of REAL
abs |.((seq_id n) . n).| is complex V34() ext-real Element of REAL
(abs |.((seq_id n) . n).|) * (abs (|.(seq_id nn).| . n)) is complex V34() ext-real Element of REAL
2 * ((abs |.((seq_id n) . n).|) * (abs (|.(seq_id nn).| . n))) is complex V34() ext-real Element of REAL
rseq is complex V34() ext-real Element of REAL
m is complex V34() ext-real Element of REAL
rseq * m is complex V34() ext-real Element of REAL
2 * (rseq * m) is complex V34() ext-real Element of REAL
2 * (abs v) is complex V34() ext-real Element of REAL
(2 * (abs v)) * (abs seqvn) is complex V34() ext-real Element of REAL
0 + ((2 (#) (abs (|.(seq_id n).| (#) |.(seq_id nn).|))) . n) is complex V34() ext-real Element of REAL
(((|.(seq_id nn).| (#) |.(seq_id nn).|) + (|.(seq_id n).| (#) |.(seq_id n).|)) . n) - ((2 (#) (abs (|.(seq_id n).| (#) |.(seq_id nn).|))) . n) is complex V34() ext-real Element of REAL
((((|.(seq_id nn).| (#) |.(seq_id nn).|) + (|.(seq_id n).| (#) |.(seq_id n).|)) . n) - ((2 (#) (abs (|.(seq_id n).| (#) |.(seq_id nn).|))) . n)) + ((2 (#) (abs (|.(seq_id n).| (#) |.(seq_id nn).|))) . n) is complex V34() ext-real Element of REAL
(1 / 2) (#) (2 (#) (abs (|.(seq_id n).| (#) |.(seq_id nn).|))) is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
(1 / 2) * 2 is non zero complex V34() ext-real Element of REAL
((1 / 2) * 2) (#) (abs (|.(seq_id n).| (#) |.(seq_id nn).|)) is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
seq is Element of the carrier of Complex_l2_Space
n is Element of the carrier of Complex_l2_Space
seq .|. n is complex set
seq_id seq is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
seq_id n is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
(seq_id n) *' is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
(seq_id seq) (#) ((seq_id n) *') is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
Sum ((seq_id seq) (#) ((seq_id n) *')) is complex Element of COMPLEX
the scalar of Complex_l2_Space is Relation-like [: the carrier of Complex_l2_Space, the carrier of Complex_l2_Space:] -defined COMPLEX -valued Function-like non zero V14([: the carrier of Complex_l2_Space, the carrier of Complex_l2_Space:]) V18([: the carrier of Complex_l2_Space, the carrier of Complex_l2_Space:], COMPLEX ) V38() Element of bool [:[: the carrier of Complex_l2_Space, the carrier of Complex_l2_Space:],COMPLEX:]
[: the carrier of Complex_l2_Space, the carrier of Complex_l2_Space:] is non zero set
[:[: the carrier of Complex_l2_Space, the carrier of Complex_l2_Space:],COMPLEX:] is non zero V38() set
bool [:[: the carrier of Complex_l2_Space, the carrier of Complex_l2_Space:],COMPLEX:] is non zero set
the scalar of Complex_l2_Space . (seq,n) is complex Element of COMPLEX
K88(seq,n) is set
the scalar of Complex_l2_Space . K88(seq,n) is complex set
seq is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
|.seq.| is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
seq *' is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
|.(seq *').| is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
seqt is V26() V27() V28() V32() complex V34() ext-real V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
|.seq.| . seqt is complex V34() ext-real Element of REAL
|.(seq *').| . seqt is complex V34() ext-real Element of REAL
(seq *') . seqt is complex Element of COMPLEX
|.((seq *') . seqt).| is complex V34() ext-real Element of REAL
seq . seqt is complex Element of COMPLEX
(seq . seqt) *' is complex Element of COMPLEX
|.((seq . seqt) *').| is complex V34() ext-real Element of REAL
|.(seq . seqt).| is complex V34() ext-real Element of REAL
n is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
nn is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
seqt is set
n . seqt is complex V34() ext-real Element of REAL
nn . seqt is complex V34() ext-real Element of REAL
seq is set
seq_id seq is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
(seq_id seq) *' is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
(seq_id seq) (#) ((seq_id seq) *') is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
|.(seq_id seq).| is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
|.((seq_id seq) *').| is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
|.(seq_id seq).| (#) |.(seq_id seq).| is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
|.((seq_id seq) (#) ((seq_id seq) *')).| is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
seq is set
seq_id seq is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
(seq_id seq) *' is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
(seq_id seq) (#) ((seq_id seq) *') is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
|.((seq_id seq) (#) ((seq_id seq) *')).| is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
|.(seq_id seq).| is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
|.((seq_id seq) *').| is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
|.(seq_id seq).| (#) |.((seq_id seq) *').| is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
|.(seq_id seq).| (#) |.(seq_id seq).| is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
seq is set
seq_id seq is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
(seq_id seq) *' is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
(seq_id seq) (#) ((seq_id seq) *') is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
n is set
seq_id n is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
(seq_id n) *' is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
(seq_id n) (#) ((seq_id n) *') is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
seq is set
seq_id seq is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
|.(seq_id seq).| is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
|.(seq_id seq).| (#) |.(seq_id seq).| is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
n is set
seq_id n is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
|.(seq_id n).| is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
|.(seq_id n).| (#) |.(seq_id n).| is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
nn is set
seq_id nn is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
(seq_id nn) *' is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
(seq_id nn) (#) ((seq_id nn) *') is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
seqt is set
seq_id seqt is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
(seq_id seqt) *' is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
(seq_id seqt) (#) ((seq_id seqt) *') is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
tv is Element of the carrier of Complex_l2_Space
seq_id tv is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
e is Element of the carrier of Complex_l2_Space
m is Element of the carrier of Complex_l2_Space
e + m is Element of the carrier of Complex_l2_Space
the addF of Complex_l2_Space is Relation-like [: the carrier of Complex_l2_Space, the carrier of Complex_l2_Space:] -defined the carrier of Complex_l2_Space -valued Function-like non zero V14([: the carrier of Complex_l2_Space, the carrier of Complex_l2_Space:]) V18([: the carrier of Complex_l2_Space, the carrier of Complex_l2_Space:], the carrier of Complex_l2_Space) Element of bool [:[: the carrier of Complex_l2_Space, the carrier of Complex_l2_Space:], the carrier of Complex_l2_Space:]
[: the carrier of Complex_l2_Space, the carrier of Complex_l2_Space:] is non zero set
[:[: the carrier of Complex_l2_Space, the carrier of Complex_l2_Space:], the carrier of Complex_l2_Space:] is non zero set
bool [:[: the carrier of Complex_l2_Space, the carrier of Complex_l2_Space:], the carrier of Complex_l2_Space:] is non zero set
the addF of Complex_l2_Space . (e,m) is Element of the carrier of Complex_l2_Space
K88(e,m) is set
the addF of Complex_l2_Space . K88(e,m) is set
seq_id e is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
seq_id m is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
(seq_id e) + (seq_id m) is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
n is Element of the carrier of Complex_l2_Space
u is complex set
u * n is Element of the carrier of Complex_l2_Space
seq_id n is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
u (#) (seq_id n) is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
v is Element of the carrier of Complex_l2_Space
- v is Element of the carrier of Complex_l2_Space
seq_id v is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
- (seq_id v) is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
- 1 is non zero complex set
(- 1) (#) (seq_id v) is Relation-like NAT -defined Function-like V14( NAT ) V38() set
seqvn is Element of the carrier of Complex_l2_Space
- seqvn is Element of the carrier of Complex_l2_Space
seq_id (- seqvn) is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
seq_id seqvn is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
- (seq_id seqvn) is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
(- 1) (#) (seq_id seqvn) is Relation-like NAT -defined Function-like V14( NAT ) V38() set
rseq is Element of the carrier of Complex_l2_Space
m is Element of the carrier of Complex_l2_Space
rseq - m is Element of the carrier of Complex_l2_Space
- m is Element of the carrier of Complex_l2_Space
rseq + (- m) is Element of the carrier of Complex_l2_Space
the addF of Complex_l2_Space . (rseq,(- m)) is Element of the carrier of Complex_l2_Space
K88(rseq,(- m)) is set
the addF of Complex_l2_Space . K88(rseq,(- m)) is set
seq_id rseq is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
seq_id m is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
(seq_id rseq) - (seq_id m) is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
- (seq_id m) is Relation-like NAT -defined Function-like V14( NAT ) V38() set
(- 1) (#) (seq_id m) is Relation-like NAT -defined Function-like V14( NAT ) V38() set
(seq_id rseq) + (- (seq_id m)) is Relation-like NAT -defined Function-like V14( NAT ) V38() set
c₁₄ is Element of the carrier of Complex_l2_Space
seq_id c₁₄ is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
|.(seq_id c₁₄).| is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
c₁₅ is Element of the carrier of Complex_l2_Space
seq_id c₁₅ is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
|.(seq_id c₁₅).| is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
|.(seq_id c₁₄).| (#) |.(seq_id c₁₅).| is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
c₁₆ is Element of the carrier of Complex_l2_Space
c₁₇ is Element of the carrier of Complex_l2_Space
c₁₆ .|. c₁₇ is complex set
seq_id c₁₆ is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
seq_id c₁₇ is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
(seq_id c₁₇) *' is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
(seq_id c₁₆) (#) ((seq_id c₁₇) *') is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
Sum ((seq_id c₁₆) (#) ((seq_id c₁₇) *')) is complex Element of COMPLEX
seq is Element of the carrier of Complex_l2_Space
seq .|. seq is complex set
Re (seq .|. seq) is complex V34() ext-real Element of REAL
Im (seq .|. seq) is complex V34() ext-real Element of REAL
n is Element of the carrier of Complex_l2_Space
seq .|. n is complex set
n .|. seq is complex set
(n .|. seq) *' is complex Element of COMPLEX
seq + n is Element of the carrier of Complex_l2_Space
the addF of Complex_l2_Space is Relation-like [: the carrier of Complex_l2_Space, the carrier of Complex_l2_Space:] -defined the carrier of Complex_l2_Space -valued Function-like non zero V14([: the carrier of Complex_l2_Space, the carrier of Complex_l2_Space:]) V18([: the carrier of Complex_l2_Space, the carrier of Complex_l2_Space:], the carrier of Complex_l2_Space) Element of bool [:[: the carrier of Complex_l2_Space, the carrier of Complex_l2_Space:], the carrier of Complex_l2_Space:]
[: the carrier of Complex_l2_Space, the carrier of Complex_l2_Space:] is non zero set
[:[: the carrier of Complex_l2_Space, the carrier of Complex_l2_Space:], the carrier of Complex_l2_Space:] is non zero set
bool [:[: the carrier of Complex_l2_Space, the carrier of Complex_l2_Space:], the carrier of Complex_l2_Space:] is non zero set
the addF of Complex_l2_Space . (seq,n) is Element of the carrier of Complex_l2_Space
K88(seq,n) is set
the addF of Complex_l2_Space . K88(seq,n) is set
nn is Element of the carrier of Complex_l2_Space
(seq + n) .|. nn is complex set
seq .|. nn is complex set
n .|. nn is complex set
(seq .|. nn) + (n .|. nn) is complex set
seqt is complex set
seqt * seq is Element of the carrier of Complex_l2_Space
(seqt * seq) .|. n is complex set
seqt * (seq .|. n) is complex set
seq_id seq is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
the scalar of Complex_l2_Space is Relation-like [: the carrier of Complex_l2_Space, the carrier of Complex_l2_Space:] -defined COMPLEX -valued Function-like non zero V14([: the carrier of Complex_l2_Space, the carrier of Complex_l2_Space:]) V18([: the carrier of Complex_l2_Space, the carrier of Complex_l2_Space:], COMPLEX ) V38() Element of bool [:[: the carrier of Complex_l2_Space, the carrier of Complex_l2_Space:],COMPLEX:]
[:[: the carrier of Complex_l2_Space, the carrier of Complex_l2_Space:],COMPLEX:] is non zero V38() set
bool [:[: the carrier of Complex_l2_Space, the carrier of Complex_l2_Space:],COMPLEX:] is non zero set
the scalar of Complex_l2_Space . (seq,seq) is complex Element of COMPLEX
K88(seq,seq) is set
the scalar of Complex_l2_Space . K88(seq,seq) is complex set
(seq_id seq) *' is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
(seq_id seq) (#) ((seq_id seq) *') is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
Sum ((seq_id seq) (#) ((seq_id seq) *')) is complex Element of COMPLEX
Re ((seq_id seq) (#) ((seq_id seq) *')) is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
Sum (Re ((seq_id seq) (#) ((seq_id seq) *'))) is complex V34() ext-real Element of REAL
Im ((seq_id seq) (#) ((seq_id seq) *')) is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
Sum (Im ((seq_id seq) (#) ((seq_id seq) *'))) is complex V34() ext-real Element of REAL
(Sum (Im ((seq_id seq) (#) ((seq_id seq) *')))) * <i> is complex set
(Sum (Re ((seq_id seq) (#) ((seq_id seq) *')))) + ((Sum (Im ((seq_id seq) (#) ((seq_id seq) *')))) * <i>) is complex set
u is V26() V27() V28() V32() complex V34() ext-real V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
(Re ((seq_id seq) (#) ((seq_id seq) *'))) . u is complex V34() ext-real Element of REAL
(seq_id seq) . u is complex Element of COMPLEX
Re ((seq_id seq) . u) is complex V34() ext-real Element of REAL
(Re ((seq_id seq) . u)) ^2 is complex V34() ext-real Element of REAL
(Re ((seq_id seq) . u)) * (Re ((seq_id seq) . u)) is complex set
Im ((seq_id seq) . u) is complex V34() ext-real Element of REAL
(Im ((seq_id seq) . u)) ^2 is complex V34() ext-real Element of REAL
(Im ((seq_id seq) . u)) * (Im ((seq_id seq) . u)) is complex set
((Re ((seq_id seq) . u)) ^2) + ((Im ((seq_id seq) . u)) ^2) is complex V34() ext-real Element of REAL
Re (seq_id seq) is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
Re ((seq_id seq) *') is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
(Re (seq_id seq)) (#) (Re ((seq_id seq) *')) is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
Im (seq_id seq) is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
Im ((seq_id seq) *') is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
(Im (seq_id seq)) (#) (Im ((seq_id seq) *')) is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
((Re (seq_id seq)) (#) (Re ((seq_id seq) *'))) - ((Im (seq_id seq)) (#) (Im ((seq_id seq) *'))) is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
- ((Im (seq_id seq)) (#) (Im ((seq_id seq) *'))) is Relation-like NAT -defined Function-like V14( NAT ) V38() V39() V40() set
- 1 is non zero complex set
(- 1) (#) ((Im (seq_id seq)) (#) (Im ((seq_id seq) *'))) is Relation-like NAT -defined Function-like V14( NAT ) V38() set
((Re (seq_id seq)) (#) (Re ((seq_id seq) *'))) + (- ((Im (seq_id seq)) (#) (Im ((seq_id seq) *')))) is Relation-like NAT -defined Function-like V14( NAT ) V38() V39() V40() set
(((Re (seq_id seq)) (#) (Re ((seq_id seq) *'))) - ((Im (seq_id seq)) (#) (Im ((seq_id seq) *')))) . u is complex V34() ext-real Element of REAL
((Re (seq_id seq)) (#) (Re ((seq_id seq) *'))) . u is complex V34() ext-real Element of REAL
- ((Im (seq_id seq)) (#) (Im ((seq_id seq) *'))) is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
(- ((Im (seq_id seq)) (#) (Im ((seq_id seq) *')))) . u is complex V34() ext-real Element of REAL
(((Re (seq_id seq)) (#) (Re ((seq_id seq) *'))) . u) + ((- ((Im (seq_id seq)) (#) (Im ((seq_id seq) *')))) . u) is complex V34() ext-real Element of REAL
((Im (seq_id seq)) (#) (Im ((seq_id seq) *'))) . u is complex V34() ext-real Element of REAL
- (((Im (seq_id seq)) (#) (Im ((seq_id seq) *'))) . u) is complex V34() ext-real Element of REAL
(((Re (seq_id seq)) (#) (Re ((seq_id seq) *'))) . u) + (- (((Im (seq_id seq)) (#) (Im ((seq_id seq) *'))) . u)) is complex V34() ext-real Element of REAL
(((Re (seq_id seq)) (#) (Re ((seq_id seq) *'))) . u) - (((Im (seq_id seq)) (#) (Im ((seq_id seq) *'))) . u) is complex V34() ext-real Element of REAL
(Re (seq_id seq)) . u is complex V34() ext-real Element of REAL
(Re ((seq_id seq) *')) . u is complex V34() ext-real Element of REAL
((Re (seq_id seq)) . u) * ((Re ((seq_id seq) *')) . u) is complex V34() ext-real Element of REAL
(((Re (seq_id seq)) . u) * ((Re ((seq_id seq) *')) . u)) - (((Im (seq_id seq)) (#) (Im ((seq_id seq) *'))) . u) is complex V34() ext-real Element of REAL
(Im (seq_id seq)) . u is complex V34() ext-real Element of REAL
(Im ((seq_id seq) *')) . u is complex V34() ext-real Element of REAL
((Im (seq_id seq)) . u) * ((Im ((seq_id seq) *')) . u) is complex V34() ext-real Element of REAL
(((Re (seq_id seq)) . u) * ((Re ((seq_id seq) *')) . u)) - (((Im (seq_id seq)) . u) * ((Im ((seq_id seq) *')) . u)) is complex V34() ext-real Element of REAL
(Re ((seq_id seq) . u)) * ((Re ((seq_id seq) *')) . u) is complex V34() ext-real Element of REAL
((Re ((seq_id seq) . u)) * ((Re ((seq_id seq) *')) . u)) - (((Im (seq_id seq)) . u) * ((Im ((seq_id seq) *')) . u)) is complex V34() ext-real Element of REAL
((seq_id seq) *') . u is complex Element of COMPLEX
Re (((seq_id seq) *') . u) is complex V34() ext-real Element of REAL
(Re ((seq_id seq) . u)) * (Re (((seq_id seq) *') . u)) is complex V34() ext-real Element of REAL
((Re ((seq_id seq) . u)) * (Re (((seq_id seq) *') . u))) - (((Im (seq_id seq)) . u) * ((Im ((seq_id seq) *')) . u)) is complex V34() ext-real Element of REAL
(Im ((seq_id seq) . u)) * ((Im ((seq_id seq) *')) . u) is complex V34() ext-real Element of REAL
((Re ((seq_id seq) . u)) * (Re (((seq_id seq) *') . u))) - ((Im ((seq_id seq) . u)) * ((Im ((seq_id seq) *')) . u)) is complex V34() ext-real Element of REAL
Im (((seq_id seq) *') . u) is complex V34() ext-real Element of REAL
(Im ((seq_id seq) . u)) * (Im (((seq_id seq) *') . u)) is complex V34() ext-real Element of REAL
((Re ((seq_id seq) . u)) * (Re (((seq_id seq) *') . u))) - ((Im ((seq_id seq) . u)) * (Im (((seq_id seq) *') . u))) is complex V34() ext-real Element of REAL
((seq_id seq) . u) *' is complex Element of COMPLEX
Re (((seq_id seq) . u) *') is complex V34() ext-real Element of REAL
(Re ((seq_id seq) . u)) * (Re (((seq_id seq) . u) *')) is complex V34() ext-real Element of REAL
((Re ((seq_id seq) . u)) * (Re (((seq_id seq) . u) *'))) - ((Im ((seq_id seq) . u)) * (Im (((seq_id seq) *') . u))) is complex V34() ext-real Element of REAL
Im (((seq_id seq) . u) *') is complex V34() ext-real Element of REAL
(Im ((seq_id seq) . u)) * (Im (((seq_id seq) . u) *')) is complex V34() ext-real Element of REAL
((Re ((seq_id seq) . u)) * (Re (((seq_id seq) . u) *'))) - ((Im ((seq_id seq) . u)) * (Im (((seq_id seq) . u) *'))) is complex V34() ext-real Element of REAL
(Re ((seq_id seq) . u)) * (Re ((seq_id seq) . u)) is complex V34() ext-real Element of REAL
((Re ((seq_id seq) . u)) * (Re ((seq_id seq) . u))) - ((Im ((seq_id seq) . u)) * (Im (((seq_id seq) . u) *'))) is complex V34() ext-real Element of REAL
- (Im ((seq_id seq) . u)) is complex V34() ext-real Element of REAL
(Im ((seq_id seq) . u)) * (- (Im ((seq_id seq) . u))) is complex V34() ext-real Element of REAL
((Re ((seq_id seq) . u)) * (Re ((seq_id seq) . u))) - ((Im ((seq_id seq) . u)) * (- (Im ((seq_id seq) . u)))) is complex V34() ext-real Element of REAL
(Im ((seq_id seq) . u)) * (Im ((seq_id seq) . u)) is complex V34() ext-real Element of REAL
((Re ((seq_id seq) . u)) ^2) + ((Im ((seq_id seq) . u)) * (Im ((seq_id seq) . u))) is complex V34() ext-real Element of REAL
u is V26() V27() V28() V32() complex V34() ext-real V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
(Re ((seq_id seq) (#) ((seq_id seq) *'))) . u is complex V34() ext-real Element of REAL
(seq_id seq) . u is complex Element of COMPLEX
Im ((seq_id seq) . u) is complex V34() ext-real Element of REAL
(Im ((seq_id seq) . u)) ^2 is complex V34() ext-real Element of REAL
(Im ((seq_id seq) . u)) * (Im ((seq_id seq) . u)) is complex set
Re ((seq_id seq) . u) is complex V34() ext-real Element of REAL
(Re ((seq_id seq) . u)) ^2 is complex V34() ext-real Element of REAL
(Re ((seq_id seq) . u)) * (Re ((seq_id seq) . u)) is complex set
((Re ((seq_id seq) . u)) ^2) + ((Im ((seq_id seq) . u)) ^2) is complex V34() ext-real Element of REAL
0 + 0 is V26() V27() V28() V32() complex V34() ext-real V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
u is V26() V27() V28() V32() complex V34() ext-real V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
(seq_id seq) . u is complex Element of COMPLEX
(Re ((seq_id seq) (#) ((seq_id seq) *'))) . u is complex V34() ext-real Element of REAL
Re ((seq_id seq) . u) is complex V34() ext-real Element of REAL
(Re ((seq_id seq) . u)) ^2 is complex V34() ext-real Element of REAL
(Re ((seq_id seq) . u)) * (Re ((seq_id seq) . u)) is complex set
Im ((seq_id seq) . u) is complex V34() ext-real Element of REAL
(Im ((seq_id seq) . u)) ^2 is complex V34() ext-real Element of REAL
(Im ((seq_id seq) . u)) * (Im ((seq_id seq) . u)) is complex set
((Re ((seq_id seq) . u)) ^2) + ((Im ((seq_id seq) . u)) ^2) is complex V34() ext-real Element of REAL
e is V26() V27() V28() V32() complex V34() ext-real V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
((seq_id seq) (#) ((seq_id seq) *')) . e is complex Element of COMPLEX
(seq_id seq) . e is complex Element of COMPLEX
((seq_id seq) *') . e is complex Element of COMPLEX
((seq_id seq) . e) * (((seq_id seq) *') . e) is complex Element of COMPLEX
0c * (((seq_id seq) *') . e) is complex Element of COMPLEX
seq_id n is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
m is V26() V27() V28() V32() complex V34() ext-real V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
(Re ((seq_id seq) (#) ((seq_id seq) *'))) . m is complex V34() ext-real Element of REAL
(seq_id seq) . m is complex Element of COMPLEX
Re ((seq_id seq) . m) is complex V34() ext-real Element of REAL
(Re ((seq_id seq) . m)) ^2 is complex V34() ext-real Element of REAL
(Re ((seq_id seq) . m)) * (Re ((seq_id seq) . m)) is complex set
Im ((seq_id seq) . m) is complex V34() ext-real Element of REAL
(Im ((seq_id seq) . m)) ^2 is complex V34() ext-real Element of REAL
(Im ((seq_id seq) . m)) * (Im ((seq_id seq) . m)) is complex set
((seq_id seq) (#) ((seq_id seq) *')) . m is complex Element of COMPLEX
Re (((seq_id seq) (#) ((seq_id seq) *')) . m) is complex V34() ext-real Element of REAL
((seq_id seq) *') . m is complex Element of COMPLEX
((seq_id seq) . m) * (((seq_id seq) *') . m) is complex Element of COMPLEX
Re (((seq_id seq) . m) * (((seq_id seq) *') . m)) is complex V34() ext-real Element of REAL
((seq_id seq) . m) *' is complex Element of COMPLEX
((seq_id seq) . m) * (((seq_id seq) . m) *') is complex Element of COMPLEX
Re (((seq_id seq) . m) * (((seq_id seq) . m) *')) is complex V34() ext-real Element of REAL
((Re ((seq_id seq) . m)) ^2) + ((Im ((seq_id seq) . m)) ^2) is complex V34() ext-real Element of REAL
0 + 0 is V26() V27() V28() V32() complex V34() ext-real V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
|.(seq_id seq).| is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
|.(seq_id n).| is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
|.(seq_id seq).| (#) |.(seq_id n).| is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
|.((seq_id seq) *').| is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
|.((seq_id seq) *').| (#) |.(seq_id n).| is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
((seq_id seq) *') (#) (seq_id n) is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
|.(((seq_id seq) *') (#) (seq_id n)).| is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
seq_id nn is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
u is V26() V27() V28() V32() complex V34() ext-real V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
(Im ((seq_id seq) (#) ((seq_id seq) *'))) . u is complex V34() ext-real Element of REAL
((seq_id seq) (#) ((seq_id seq) *')) . u is complex Element of COMPLEX
Im (((seq_id seq) (#) ((seq_id seq) *')) . u) is complex V34() ext-real Element of REAL
(seq_id seq) . u is complex Element of COMPLEX
((seq_id seq) *') . u is complex Element of COMPLEX
((seq_id seq) . u) * (((seq_id seq) *') . u) is complex Element of COMPLEX
Im (((seq_id seq) . u) * (((seq_id seq) *') . u)) is complex V34() ext-real Element of REAL
((seq_id seq) . u) *' is complex Element of COMPLEX
((seq_id seq) . u) * (((seq_id seq) . u) *') is complex Element of COMPLEX
Im (((seq_id seq) . u) * (((seq_id seq) . u) *')) is complex V34() ext-real Element of REAL
|.(seq_id nn).| is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
|.(seq_id seq).| (#) |.(seq_id nn).| is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
(seq_id nn) *' is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
|.((seq_id nn) *').| is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
|.(seq_id seq).| (#) |.((seq_id nn) *').| is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
(seq_id seq) (#) ((seq_id nn) *') is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
|.((seq_id seq) (#) ((seq_id nn) *')).| is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
|.(seq_id n).| (#) |.(seq_id nn).| is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
|.(seq_id n).| (#) |.((seq_id nn) *').| is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
(seq_id n) (#) ((seq_id nn) *') is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
|.((seq_id n) (#) ((seq_id nn) *')).| is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
the scalar of Complex_l2_Space . ((seq + n),nn) is complex Element of COMPLEX
K88((seq + n),nn) is set
the scalar of Complex_l2_Space . K88((seq + n),nn) is complex set
seq_id (seq + n) is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
(seq_id (seq + n)) (#) ((seq_id nn) *') is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
Sum ((seq_id (seq + n)) (#) ((seq_id nn) *')) is complex Element of COMPLEX
(seq_id seq) + (seq_id n) is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
seq_id ((seq_id seq) + (seq_id n)) is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
(seq_id ((seq_id seq) + (seq_id n))) (#) ((seq_id nn) *') is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
Sum ((seq_id ((seq_id seq) + (seq_id n))) (#) ((seq_id nn) *')) is complex Element of COMPLEX
((seq_id seq) + (seq_id n)) (#) ((seq_id nn) *') is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
Sum (((seq_id seq) + (seq_id n)) (#) ((seq_id nn) *')) is complex Element of COMPLEX
((seq_id seq) (#) ((seq_id nn) *')) + ((seq_id n) (#) ((seq_id nn) *')) is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
Sum (((seq_id seq) (#) ((seq_id nn) *')) + ((seq_id n) (#) ((seq_id nn) *'))) is complex Element of COMPLEX
Sum ((seq_id seq) (#) ((seq_id nn) *')) is complex Element of COMPLEX
Sum ((seq_id n) (#) ((seq_id nn) *')) is complex Element of COMPLEX
(Sum ((seq_id seq) (#) ((seq_id nn) *'))) + (Sum ((seq_id n) (#) ((seq_id nn) *'))) is complex Element of COMPLEX
the scalar of Complex_l2_Space . (seq,nn) is complex Element of COMPLEX
K88(seq,nn) is set
the scalar of Complex_l2_Space . K88(seq,nn) is complex set
( the scalar of Complex_l2_Space . (seq,nn)) + (Sum ((seq_id n) (#) ((seq_id nn) *'))) is complex Element of COMPLEX
the scalar of Complex_l2_Space . (n,nn) is complex Element of COMPLEX
K88(n,nn) is set
the scalar of Complex_l2_Space . K88(n,nn) is complex set
( the scalar of Complex_l2_Space . (seq,nn)) + ( the scalar of Complex_l2_Space . (n,nn)) is complex Element of COMPLEX
(seq .|. nn) + ( the scalar of Complex_l2_Space . (n,nn)) is complex set
(seq_id n) *' is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
|.((seq_id n) *').| is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
|.(seq_id seq).| (#) |.((seq_id n) *').| is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
(seq_id seq) (#) ((seq_id n) *') is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
|.((seq_id seq) (#) ((seq_id n) *')).| is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
the scalar of Complex_l2_Space . ((seqt * seq),n) is complex Element of COMPLEX
K88((seqt * seq),n) is set
the scalar of Complex_l2_Space . K88((seqt * seq),n) is complex set
seq_id (seqt * seq) is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
(seq_id (seqt * seq)) (#) ((seq_id n) *') is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
Sum ((seq_id (seqt * seq)) (#) ((seq_id n) *')) is complex Element of COMPLEX
seqt (#) (seq_id seq) is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
seq_id (seqt (#) (seq_id seq)) is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
(seq_id (seqt (#) (seq_id seq))) (#) ((seq_id n) *') is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
Sum ((seq_id (seqt (#) (seq_id seq))) (#) ((seq_id n) *')) is complex Element of COMPLEX
(seqt (#) (seq_id seq)) (#) ((seq_id n) *') is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
Sum ((seqt (#) (seq_id seq)) (#) ((seq_id n) *')) is complex Element of COMPLEX
seqt (#) ((seq_id seq) (#) ((seq_id n) *')) is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
Sum (seqt (#) ((seq_id seq) (#) ((seq_id n) *'))) is complex Element of COMPLEX
Sum ((seq_id seq) (#) ((seq_id n) *')) is complex Element of COMPLEX
seqt * (Sum ((seq_id seq) (#) ((seq_id n) *'))) is complex set
the scalar of Complex_l2_Space . (seq,n) is complex Element of COMPLEX
the scalar of Complex_l2_Space . K88(seq,n) is complex set
seqt * ( the scalar of Complex_l2_Space . (seq,n)) is complex set
((seq_id seq) *') *' is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
(((seq_id seq) *') *') (#) ((seq_id n) *') is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
Sum ((((seq_id seq) *') *') (#) ((seq_id n) *')) is complex Element of COMPLEX
(((seq_id seq) *') (#) (seq_id n)) *' is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
Sum ((((seq_id seq) *') (#) (seq_id n)) *') is complex Element of COMPLEX
Sum (((seq_id seq) *') (#) (seq_id n)) is complex Element of COMPLEX
(Sum (((seq_id seq) *') (#) (seq_id n))) *' is complex Element of COMPLEX
the scalar of Complex_l2_Space . (n,seq) is complex Element of COMPLEX
K88(n,seq) is set
the scalar of Complex_l2_Space . K88(n,seq) is complex set
( the scalar of Complex_l2_Space . (n,seq)) *' is complex Element of COMPLEX
seq is complex set
n is complex set
seq * n is complex set
|.(seq * n).| is complex V34() ext-real Element of REAL
2 * |.(seq * n).| is complex V34() ext-real Element of REAL
|.seq.| is complex V34() ext-real Element of REAL
|.seq.| ^2 is complex V34() ext-real Element of REAL
|.seq.| * |.seq.| is complex set
|.n.| is complex V34() ext-real Element of REAL
|.n.| ^2 is complex V34() ext-real Element of REAL
|.n.| * |.n.| is complex set
(|.seq.| ^2) + (|.n.| ^2) is complex V34() ext-real Element of REAL
|.seq.| - |.n.| is complex V34() ext-real Element of REAL
(|.seq.| - |.n.|) ^2 is complex V34() ext-real Element of REAL
(|.seq.| - |.n.|) * (|.seq.| - |.n.|) is complex set
|.seq.| * |.seq.| is complex V34() ext-real Element of REAL
|.seq.| * |.n.| is complex V34() ext-real Element of REAL
(|.seq.| * |.n.|) + (|.seq.| * |.n.|) is complex V34() ext-real Element of REAL
(|.seq.| * |.seq.|) - ((|.seq.| * |.n.|) + (|.seq.| * |.n.|)) is complex V34() ext-real Element of REAL
|.n.| * |.n.| is complex V34() ext-real Element of REAL
((|.seq.| * |.seq.|) - ((|.seq.| * |.n.|) + (|.seq.| * |.n.|))) + (|.n.| * |.n.|) is complex V34() ext-real Element of REAL
(|.seq.| * |.seq.|) + (|.n.| * |.n.|) is complex V34() ext-real Element of REAL
((|.seq.| * |.seq.|) + (|.n.| * |.n.|)) - ((|.seq.| * |.n.|) + (|.seq.| * |.n.|)) is complex V34() ext-real Element of REAL
seq is complex set
seq * seq is complex set
|.(seq * seq).| is complex V34() ext-real Element of REAL
|.seq.| is complex V34() ext-real Element of REAL
|.seq.| * |.seq.| is complex V34() ext-real Element of REAL
n is complex set
n * n is complex set
|.(n * n).| is complex V34() ext-real Element of REAL
|.n.| is complex V34() ext-real Element of REAL
|.n.| * |.n.| is complex V34() ext-real Element of REAL
seq * n is complex set
(seq * seq) + (seq * n) is complex set
((seq * seq) + (seq * n)) + (seq * n) is complex set
(((seq * seq) + (seq * n)) + (seq * n)) + (n * n) is complex set
|.((((seq * seq) + (seq * n)) + (seq * n)) + (n * n)).| is complex V34() ext-real Element of REAL
|.(((seq * seq) + (seq * n)) + (seq * n)).| is complex V34() ext-real Element of REAL
|.(((seq * seq) + (seq * n)) + (seq * n)).| + |.(n * n).| is complex V34() ext-real Element of REAL
|.((((seq * seq) + (seq * n)) + (seq * n)) + (n * n)).| - |.(n * n).| is complex V34() ext-real Element of REAL
|.((seq * seq) + (seq * n)).| is complex V34() ext-real Element of REAL
|.(seq * n).| is complex V34() ext-real Element of REAL
|.((seq * seq) + (seq * n)).| + |.(seq * n).| is complex V34() ext-real Element of REAL
|.(seq * seq).| + |.(seq * n).| is complex V34() ext-real Element of REAL
|.(((seq * seq) + (seq * n)) + (seq * n)).| - |.(seq * n).| is complex V34() ext-real Element of REAL
(|.(seq * seq).| + |.(seq * n).|) + |.(seq * n).| is complex V34() ext-real Element of REAL
seq + n is complex set
|.(seq + n).| is complex V34() ext-real Element of REAL
|.(seq + n).| * |.(seq + n).| is complex V34() ext-real Element of REAL
(seq + n) * (seq + n) is complex set
|.((seq + n) * (seq + n)).| is complex V34() ext-real Element of REAL
(|.(seq + n).| * |.(seq + n).|) - |.(n * n).| is complex V34() ext-real Element of REAL
2 * |.(seq * n).| is complex V34() ext-real Element of REAL
|.(seq * seq).| + (2 * |.(seq * n).|) is complex V34() ext-real Element of REAL
((|.(seq + n).| * |.(seq + n).|) - |.(n * n).|) - |.(seq * seq).| is complex V34() ext-real Element of REAL
|.seq.| ^2 is complex V34() ext-real Element of REAL
|.seq.| * |.seq.| is complex set
|.n.| ^2 is complex V34() ext-real Element of REAL
|.n.| * |.n.| is complex set
(|.seq.| ^2) + (|.n.| ^2) is complex V34() ext-real Element of REAL
(|.(seq + n).| * |.(seq + n).|) - (|.n.| * |.n.|) is complex V34() ext-real Element of REAL
(|.seq.| * |.seq.|) + (|.n.| * |.n.|) is complex V34() ext-real Element of REAL
((|.seq.| * |.seq.|) + (|.n.| * |.n.|)) + (|.seq.| * |.seq.|) is complex V34() ext-real Element of REAL
2 * (|.seq.| * |.seq.|) is complex V34() ext-real Element of REAL
(2 * (|.seq.| * |.seq.|)) + (|.n.| * |.n.|) is complex V34() ext-real Element of REAL
((2 * (|.seq.| * |.seq.|)) + (|.n.| * |.n.|)) + (|.n.| * |.n.|) is complex V34() ext-real Element of REAL
2 * |.seq.| is complex V34() ext-real Element of REAL
(2 * |.seq.|) * |.seq.| is complex V34() ext-real Element of REAL
2 * |.n.| is complex V34() ext-real Element of REAL
(2 * |.n.|) * |.n.| is complex V34() ext-real Element of REAL
((2 * |.seq.|) * |.seq.|) + ((2 * |.n.|) * |.n.|) is complex V34() ext-real Element of REAL
seq is complex set
n is complex set
seq - n is complex set
(seq - n) + n is complex set
|.((seq - n) + n).| is complex V34() ext-real Element of REAL
|.seq.| is complex V34() ext-real Element of REAL
|.seq.| * |.seq.| is complex V34() ext-real Element of REAL
|.(seq - n).| is complex V34() ext-real Element of REAL
2 * |.(seq - n).| is complex V34() ext-real Element of REAL
(2 * |.(seq - n).|) * |.(seq - n).| is complex V34() ext-real Element of REAL
|.n.| is complex V34() ext-real Element of REAL
2 * |.n.| is complex V34() ext-real Element of REAL
(2 * |.n.|) * |.n.| is complex V34() ext-real Element of REAL
((2 * |.(seq - n).|) * |.(seq - n).|) + ((2 * |.n.|) * |.n.|) is complex V34() ext-real Element of REAL
seq is complex set
n is complex set
seq + n is complex set
|.(seq + n).| is complex V34() ext-real Element of REAL
|.(seq + n).| * |.(seq + n).| is complex V34() ext-real Element of REAL
|.seq.| is complex V34() ext-real Element of REAL
2 * |.seq.| is complex V34() ext-real Element of REAL
(2 * |.seq.|) * |.seq.| is complex V34() ext-real Element of REAL
|.n.| is complex V34() ext-real Element of REAL
2 * |.n.| is complex V34() ext-real Element of REAL
(2 * |.n.|) * |.n.| is complex V34() ext-real Element of REAL
((2 * |.seq.|) * |.seq.|) + ((2 * |.n.|) * |.n.|) is complex V34() ext-real Element of REAL
nn is complex set
|.nn.| is complex V34() ext-real Element of REAL
|.nn.| * |.nn.| is complex V34() ext-real Element of REAL
seqt is complex set
nn - seqt is complex set
|.(nn - seqt).| is complex V34() ext-real Element of REAL
2 * |.(nn - seqt).| is complex V34() ext-real Element of REAL
(2 * |.(nn - seqt).|) * |.(nn - seqt).| is complex V34() ext-real Element of REAL
|.seqt.| is complex V34() ext-real Element of REAL
2 * |.seqt.| is complex V34() ext-real Element of REAL
(2 * |.seqt.|) * |.seqt.| is complex V34() ext-real Element of REAL
((2 * |.(nn - seqt).|) * |.(nn - seqt).|) + ((2 * |.seqt.|) * |.seqt.|) is complex V34() ext-real Element of REAL
seq is complex set
n is complex Element of COMPLEX
NAT --> n is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
nn is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
seqt is V26() V27() V28() V32() complex V34() ext-real V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
nn . seqt is complex Element of COMPLEX
seqt is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
lim seqt is complex Element of COMPLEX
(lim seqt) - seq is complex set
|.((lim seqt) - seq).| is complex V34() ext-real Element of REAL
|.((lim seqt) - seq).| * |.((lim seqt) - seq).| is complex V34() ext-real Element of REAL
seqt - nn is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
- nn is Relation-like NAT -defined Function-like V14( NAT ) V38() set
- 1 is non zero complex set
(- 1) (#) nn is Relation-like NAT -defined Function-like V14( NAT ) V38() set
seqt + (- nn) is Relation-like NAT -defined Function-like V14( NAT ) V38() set
tv is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() bounded convergent Element of bool [:NAT,COMPLEX:]
|.tv.| is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() bounded convergent bounded_above bounded_below Element of bool [:NAT,REAL:]
|.(seqt - nn).| is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
|.(seqt - nn).| (#) |.(seqt - nn).| is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
lim (|.(seqt - nn).| (#) |.(seqt - nn).|) is complex V34() ext-real Element of REAL
lim |.(seqt - nn).| is complex V34() ext-real Element of REAL
(lim |.(seqt - nn).|) * (lim |.(seqt - nn).|) is complex V34() ext-real Element of REAL
lim nn is complex Element of COMPLEX
(lim seqt) - (lim nn) is complex Element of COMPLEX
|.((lim seqt) - (lim nn)).| is complex V34() ext-real Element of REAL
|.((lim seqt) - (lim nn)).| * (lim |.(seqt - nn).|) is complex V34() ext-real Element of REAL
|.((lim seqt) - (lim nn)).| * |.((lim seqt) - (lim nn)).| is complex V34() ext-real Element of REAL
|.((lim seqt) - seq).| * |.((lim seqt) - (lim nn)).| is complex V34() ext-real Element of REAL
e is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
lim e is complex V34() ext-real Element of REAL
m is V26() V27() V28() V32() complex V34() ext-real V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
e . m is complex V34() ext-real Element of REAL
seqt . m is complex Element of COMPLEX
(seqt . m) - seq is complex set
|.((seqt . m) - seq).| is complex V34() ext-real Element of REAL
|.((seqt . m) - seq).| * |.((seqt . m) - seq).| is complex V34() ext-real Element of REAL
nn . m is complex Element of COMPLEX
(seqt . m) - (nn . m) is complex Element of COMPLEX
|.((seqt . m) - (nn . m)).| is complex V34() ext-real Element of REAL
|.((seqt . m) - (nn . m)).| * |.((seqt . m) - seq).| is complex V34() ext-real Element of REAL
|.((seqt . m) - (nn . m)).| * |.((seqt . m) - (nn . m)).| is complex V34() ext-real Element of REAL
- nn is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
(- nn) . m is complex Element of COMPLEX
(seqt . m) + ((- nn) . m) is complex Element of COMPLEX
|.((seqt . m) + ((- nn) . m)).| is complex V34() ext-real Element of REAL
- (nn . m) is complex Element of COMPLEX
(seqt . m) + (- (nn . m)) is complex Element of COMPLEX
|.((seqt . m) + (- (nn . m))).| is complex V34() ext-real Element of REAL
|.((seqt . m) + ((- nn) . m)).| * |.((seqt . m) + (- (nn . m))).| is complex V34() ext-real Element of REAL
|.((seqt . m) + ((- nn) . m)).| * |.((seqt . m) + ((- nn) . m)).| is complex V34() ext-real Element of REAL
seqt + (- nn) is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
(seqt + (- nn)) . m is complex Element of COMPLEX
|.((seqt + (- nn)) . m).| is complex V34() ext-real Element of REAL
|.((seqt + (- nn)) . m).| * |.((seqt . m) + ((- nn) . m)).| is complex V34() ext-real Element of REAL
(seqt - nn) . m is complex Element of COMPLEX
|.((seqt - nn) . m).| is complex V34() ext-real Element of REAL
|.((seqt - nn) . m).| * |.((seqt + (- nn)) . m).| is complex V34() ext-real Element of REAL
|.(seqt - nn).| . m is complex V34() ext-real Element of REAL
(|.(seqt - nn).| . m) * |.((seqt - nn) . m).| is complex V34() ext-real Element of REAL
(|.(seqt - nn).| . m) * (|.(seqt - nn).| . m) is complex V34() ext-real Element of REAL
(|.(seqt - nn).| (#) |.(seqt - nn).|) . m is complex V34() ext-real Element of REAL
m is set
e . m is complex V34() ext-real Element of REAL
(|.(seqt - nn).| (#) |.(seqt - nn).|) . m is complex V34() ext-real Element of REAL
|.tv.| (#) |.tv.| is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() bounded convergent bounded_above bounded_below Element of bool [:NAT,REAL:]
seq is complex set
n is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
lim n is complex V34() ext-real Element of REAL
nn is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
lim nn is complex Element of COMPLEX
(lim nn) - seq is complex set
|.((lim nn) - seq).| is complex V34() ext-real Element of REAL
|.((lim nn) - seq).| * |.((lim nn) - seq).| is complex V34() ext-real Element of REAL
(|.((lim nn) - seq).| * |.((lim nn) - seq).|) + (lim n) is complex V34() ext-real Element of REAL
seqt is complex Element of COMPLEX
NAT --> seqt is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
tv is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
e is V26() V27() V28() V32() complex V34() ext-real V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
tv . e is complex Element of COMPLEX
nn - tv is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
- tv is Relation-like NAT -defined Function-like V14( NAT ) V38() set
- 1 is non zero complex set
(- 1) (#) tv is Relation-like NAT -defined Function-like V14( NAT ) V38() set
nn + (- tv) is Relation-like NAT -defined Function-like V14( NAT ) V38() set
e is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() bounded convergent Element of bool [:NAT,COMPLEX:]
|.e.| is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() bounded convergent bounded_above bounded_below Element of bool [:NAT,REAL:]
|.(nn - tv).| is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
|.(nn - tv).| (#) |.(nn - tv).| is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
m is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
lim m is complex V34() ext-real Element of REAL
u is V26() V27() V28() V32() complex V34() ext-real V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
m . u is complex V34() ext-real Element of REAL
nn . u is complex Element of COMPLEX
(nn . u) - seq is complex set
|.((nn . u) - seq).| is complex V34() ext-real Element of REAL
|.((nn . u) - seq).| * |.((nn . u) - seq).| is complex V34() ext-real Element of REAL
n . u is complex V34() ext-real Element of REAL
(|.((nn . u) - seq).| * |.((nn . u) - seq).|) + (n . u) is complex V34() ext-real Element of REAL
tv . u is complex Element of COMPLEX
(nn . u) - (tv . u) is complex Element of COMPLEX
|.((nn . u) - (tv . u)).| is complex V34() ext-real Element of REAL
|.((nn . u) - (tv . u)).| * |.((nn . u) - seq).| is complex V34() ext-real Element of REAL
(|.((nn . u) - (tv . u)).| * |.((nn . u) - seq).|) + (n . u) is complex V34() ext-real Element of REAL
|.((nn . u) - (tv . u)).| * |.((nn . u) - (tv . u)).| is complex V34() ext-real Element of REAL
(|.((nn . u) - (tv . u)).| * |.((nn . u) - (tv . u)).|) + (n . u) is complex V34() ext-real Element of REAL
- tv is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
(- tv) . u is complex Element of COMPLEX
(nn . u) + ((- tv) . u) is complex Element of COMPLEX
|.((nn . u) + ((- tv) . u)).| is complex V34() ext-real Element of REAL
- (tv . u) is complex Element of COMPLEX
(nn . u) + (- (tv . u)) is complex Element of COMPLEX
|.((nn . u) + (- (tv . u))).| is complex V34() ext-real Element of REAL
|.((nn . u) + ((- tv) . u)).| * |.((nn . u) + (- (tv . u))).| is complex V34() ext-real Element of REAL
(|.((nn . u) + ((- tv) . u)).| * |.((nn . u) + (- (tv . u))).|) + (n . u) is complex V34() ext-real Element of REAL
|.((nn . u) + ((- tv) . u)).| * |.((nn . u) + ((- tv) . u)).| is complex V34() ext-real Element of REAL
(|.((nn . u) + ((- tv) . u)).| * |.((nn . u) + ((- tv) . u)).|) + (n . u) is complex V34() ext-real Element of REAL
nn + (- tv) is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
(nn + (- tv)) . u is complex Element of COMPLEX
|.((nn + (- tv)) . u).| is complex V34() ext-real Element of REAL
|.((nn + (- tv)) . u).| * |.((nn . u) + ((- tv) . u)).| is complex V34() ext-real Element of REAL
(|.((nn + (- tv)) . u).| * |.((nn . u) + ((- tv) . u)).|) + (n . u) is complex V34() ext-real Element of REAL
(nn - tv) . u is complex Element of COMPLEX
|.((nn - tv) . u).| is complex V34() ext-real Element of REAL
|.((nn - tv) . u).| * |.((nn + (- tv)) . u).| is complex V34() ext-real Element of REAL
(|.((nn - tv) . u).| * |.((nn + (- tv)) . u).|) + (n . u) is complex V34() ext-real Element of REAL
|.(nn - tv).| . u is complex V34() ext-real Element of REAL
(|.(nn - tv).| . u) * |.((nn - tv) . u).| is complex V34() ext-real Element of REAL
((|.(nn - tv).| . u) * |.((nn - tv) . u).|) + (n . u) is complex V34() ext-real Element of REAL
(|.(nn - tv).| . u) * (|.(nn - tv).| . u) is complex V34() ext-real Element of REAL
((|.(nn - tv).| . u) * (|.(nn - tv).| . u)) + (n . u) is complex V34() ext-real Element of REAL
(|.(nn - tv).| (#) |.(nn - tv).|) . u is complex V34() ext-real Element of REAL
((|.(nn - tv).| (#) |.(nn - tv).|) . u) + (n . u) is complex V34() ext-real Element of REAL
(|.(nn - tv).| (#) |.(nn - tv).|) + n is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
((|.(nn - tv).| (#) |.(nn - tv).|) + n) . u is complex V34() ext-real Element of REAL
lim (|.(nn - tv).| (#) |.(nn - tv).|) is complex V34() ext-real Element of REAL
lim |.(nn - tv).| is complex V34() ext-real Element of REAL
(lim |.(nn - tv).|) * (lim |.(nn - tv).|) is complex V34() ext-real Element of REAL
lim tv is complex Element of COMPLEX
(lim nn) - (lim tv) is complex Element of COMPLEX
|.((lim nn) - (lim tv)).| is complex V34() ext-real Element of REAL
|.((lim nn) - (lim tv)).| * (lim |.(nn - tv).|) is complex V34() ext-real Element of REAL
|.((lim nn) - (lim tv)).| * |.((lim nn) - (lim tv)).| is complex V34() ext-real Element of REAL
|.((lim nn) - seq).| * |.((lim nn) - (lim tv)).| is complex V34() ext-real Element of REAL
[:NAT, the carrier of Complex_l2_Space:] is non zero set
bool [:NAT, the carrier of Complex_l2_Space:] is non zero set
seq is Relation-like NAT -defined the carrier of Complex_l2_Space -valued Function-like non zero V14( NAT ) V18( NAT , the carrier of Complex_l2_Space) Element of bool [:NAT, the carrier of Complex_l2_Space:]
n is set
nn is V26() V27() V28() V32() complex V34() ext-real V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
seqt is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
lim seqt is complex Element of COMPLEX
tv is complex V34() ext-real Element of REAL
e is V26() V27() V28() V32() complex V34() ext-real V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
seq . e is Element of the carrier of Complex_l2_Space
n is V26() V27() V28() V32() complex V34() ext-real V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
seq . n is Element of the carrier of Complex_l2_Space
(seq . n) - (seq . e) is Element of the carrier of Complex_l2_Space
- (seq . e) is Element of the carrier of Complex_l2_Space
(seq . n) + (- (seq . e)) is Element of the carrier of Complex_l2_Space
the addF of Complex_l2_Space is Relation-like [: the carrier of Complex_l2_Space, the carrier of Complex_l2_Space:] -defined the carrier of Complex_l2_Space -valued Function-like non zero V14([: the carrier of Complex_l2_Space, the carrier of Complex_l2_Space:]) V18([: the carrier of Complex_l2_Space, the carrier of Complex_l2_Space:], the carrier of Complex_l2_Space) Element of bool [:[: the carrier of Complex_l2_Space, the carrier of Complex_l2_Space:], the carrier of Complex_l2_Space:]
[: the carrier of Complex_l2_Space, the carrier of Complex_l2_Space:] is non zero set
[:[: the carrier of Complex_l2_Space, the carrier of Complex_l2_Space:], the carrier of Complex_l2_Space:] is non zero set
bool [:[: the carrier of Complex_l2_Space, the carrier of Complex_l2_Space:], the carrier of Complex_l2_Space:] is non zero set
the addF of Complex_l2_Space . ((seq . n),(- (seq . e))) is Element of the carrier of Complex_l2_Space
K88((seq . n),(- (seq . e))) is set
the addF of Complex_l2_Space . K88((seq . n),(- (seq . e))) is set
||.((seq . n) - (seq . e)).|| is complex V34() ext-real Element of REAL
((seq . n) - (seq . e)) .|. ((seq . n) - (seq . e)) is complex set
|.(((seq . n) - (seq . e)) .|. ((seq . n) - (seq . e))).| is complex V34() ext-real Element of REAL
sqrt |.(((seq . n) - (seq . e)) .|. ((seq . n) - (seq . e))).| is complex V34() ext-real Element of REAL
seq_id ((seq . n) - (seq . e)) is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
seqt . n is complex Element of COMPLEX
seqt . e is complex Element of COMPLEX
(seqt . n) - (seqt . e) is complex Element of COMPLEX
|.((seqt . n) - (seqt . e)).| is complex V34() ext-real Element of REAL
|.((seqt . n) - (seqt . e)).| * |.((seqt . n) - (seqt . e)).| is complex V34() ext-real Element of REAL
sqrt (|.((seqt . n) - (seqt . e)).| * |.((seqt . n) - (seqt . e)).|) is complex V34() ext-real Element of REAL
|.((seqt . n) - (seqt . e)).| ^2 is complex V34() ext-real Element of REAL
|.((seqt . n) - (seqt . e)).| * |.((seqt . n) - (seqt . e)).| is complex set
sqrt (|.((seqt . n) - (seqt . e)).| ^2) is complex V34() ext-real Element of REAL
seq_id (seq . n) is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
seq_id (seq . e) is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
(seq_id (seq . n)) - (seq_id (seq . e)) is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
- (seq_id (seq . e)) is Relation-like NAT -defined Function-like V14( NAT ) V38() set
- 1 is non zero complex set
(- 1) (#) (seq_id (seq . e)) is Relation-like NAT -defined Function-like V14( NAT ) V38() set
(seq_id (seq . n)) + (- (seq_id (seq . e))) is Relation-like NAT -defined Function-like V14( NAT ) V38() set
seq_id ((seq_id (seq . n)) - (seq_id (seq . e))) is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
- (seq_id (seq . e)) is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
(seq_id (seq . n)) + (- (seq_id (seq . e))) is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
(seq_id ((seq . n) - (seq . e))) . nn is complex Element of COMPLEX
(seq_id (seq . n)) . nn is complex Element of COMPLEX
(- (seq_id (seq . e))) . nn is complex Element of COMPLEX
((seq_id (seq . n)) . nn) + ((- (seq_id (seq . e))) . nn) is complex Element of COMPLEX
(seq_id (seq . e)) . nn is complex Element of COMPLEX
- ((seq_id (seq . e)) . nn) is complex Element of COMPLEX
((seq_id (seq . n)) . nn) + (- ((seq_id (seq . e)) . nn)) is complex Element of COMPLEX
((seq_id (seq . n)) . nn) - ((seq_id (seq . e)) . nn) is complex Element of COMPLEX
(seqt . n) - ((seq_id (seq . e)) . nn) is complex Element of COMPLEX
|.(seq_id ((seq . n) - (seq . e))).| is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
|.(seq_id ((seq . n) - (seq . e))).| . nn is complex V34() ext-real Element of REAL
|.((seq_id ((seq . n) - (seq . e))) . nn).| is complex V34() ext-real Element of REAL
(|.(seq_id ((seq . n) - (seq . e))).| . nn) * |.((seq_id ((seq . n) - (seq . e))) . nn).| is complex V34() ext-real Element of REAL
(|.(seq_id ((seq . n) - (seq . e))).| . nn) * (|.(seq_id ((seq . n) - (seq . e))).| . nn) is complex V34() ext-real Element of REAL
(seq_id ((seq . n) - (seq . e))) *' is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
|.((seq_id ((seq . n) - (seq . e))) *').| is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
|.((seq_id ((seq . n) - (seq . e))) *').| . nn is complex V34() ext-real Element of REAL
(|.(seq_id ((seq . n) - (seq . e))).| . nn) * (|.((seq_id ((seq . n) - (seq . e))) *').| . nn) is complex V34() ext-real Element of REAL
|.(seq_id ((seq . n) - (seq . e))).| (#) |.((seq_id ((seq . n) - (seq . e))) *').| is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
(|.(seq_id ((seq . n) - (seq . e))).| (#) |.((seq_id ((seq . n) - (seq . e))) *').|) . nn is complex V34() ext-real Element of REAL
(seq_id ((seq . n) - (seq . e))) (#) ((seq_id ((seq . n) - (seq . e))) *') is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
Re ((seq_id ((seq . n) - (seq . e))) (#) ((seq_id ((seq . n) - (seq . e))) *')) is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
Im ((seq_id ((seq . n) - (seq . e))) (#) ((seq_id ((seq . n) - (seq . e))) *')) is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
rseq is V26() V27() V28() V32() complex V34() ext-real V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
(Re ((seq_id ((seq . n) - (seq . e))) (#) ((seq_id ((seq . n) - (seq . e))) *'))) . rseq is complex V34() ext-real Element of REAL
m is V26() V27() V28() V32() complex V34() ext-real V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
(Im ((seq_id ((seq . n) - (seq . e))) (#) ((seq_id ((seq . n) - (seq . e))) *'))) . m is complex V34() ext-real Element of REAL
Sum ((seq_id ((seq . n) - (seq . e))) (#) ((seq_id ((seq . n) - (seq . e))) *')) is complex Element of COMPLEX
|.(Sum ((seq_id ((seq . n) - (seq . e))) (#) ((seq_id ((seq . n) - (seq . e))) *'))).| is complex V34() ext-real Element of REAL
|.((seq_id ((seq . n) - (seq . e))) (#) ((seq_id ((seq . n) - (seq . e))) *')).| is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
Sum |.((seq_id ((seq . n) - (seq . e))) (#) ((seq_id ((seq . n) - (seq . e))) *')).| is complex V34() ext-real Element of REAL
Sum (|.(seq_id ((seq . n) - (seq . e))).| (#) |.((seq_id ((seq . n) - (seq . e))) *').|) is complex V34() ext-real Element of REAL
sqrt (Sum (|.(seq_id ((seq . n) - (seq . e))).| (#) |.((seq_id ((seq . n) - (seq . e))) *').|)) is complex V34() ext-real Element of REAL
rseq is V26() V27() V28() V32() complex V34() ext-real V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
(|.(seq_id ((seq . n) - (seq . e))).| (#) |.((seq_id ((seq . n) - (seq . e))) *').|) . rseq is complex V34() ext-real Element of REAL
|.(seq_id ((seq . n) - (seq . e))).| . rseq is complex V34() ext-real Element of REAL
|.((seq_id ((seq . n) - (seq . e))) *').| . rseq is complex V34() ext-real Element of REAL
(|.(seq_id ((seq . n) - (seq . e))).| . rseq) * (|.((seq_id ((seq . n) - (seq . e))) *').| . rseq) is complex V34() ext-real Element of REAL
(|.(seq_id ((seq . n) - (seq . e))).| . rseq) * (|.(seq_id ((seq . n) - (seq . e))).| . rseq) is complex V34() ext-real Element of REAL
|.(seq_id ((seq . n) - (seq . e))).| (#) |.(seq_id ((seq . n) - (seq . e))).| is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
m is complex V34() ext-real Element of REAL
m ^2 is complex V34() ext-real Element of REAL
m * m is complex set
(sqrt (Sum (|.(seq_id ((seq . n) - (seq . e))).| (#) |.((seq_id ((seq . n) - (seq . e))) *').|))) ^2 is complex V34() ext-real Element of REAL
(sqrt (Sum (|.(seq_id ((seq . n) - (seq . e))).| (#) |.((seq_id ((seq . n) - (seq . e))) *').|))) * (sqrt (Sum (|.(seq_id ((seq . n) - (seq . e))).| (#) |.((seq_id ((seq . n) - (seq . e))) *').|))) is complex set
tv * tv is complex V34() ext-real Element of REAL
sqrt (tv * tv) is complex V34() ext-real Element of REAL
sqrt (m ^2) is complex V34() ext-real Element of REAL
n is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
nn is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
seq_id nn is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
tv is V26() V27() V28() V32() complex V34() ext-real V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
e is set
n . e is complex set
nn . tv is complex Element of COMPLEX
m is V26() V27() V28() V32() complex V34() ext-real V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
u is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
lim u is complex Element of COMPLEX
tv is complex V34() ext-real Element of REAL
tv * tv is complex V34() ext-real Element of REAL
tv / 2 is complex V34() ext-real Element of REAL
m is V26() V27() V28() V32() complex V34() ext-real V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
(tv / 2) * (tv / 2) is complex V34() ext-real Element of REAL
n is V26() V27() V28() V32() complex V34() ext-real V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
u is V26() V27() V28() V32() complex V34() ext-real V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
seq . n is Element of the carrier of Complex_l2_Space
seq . u is Element of the carrier of Complex_l2_Space
(seq . n) - (seq . u) is Element of the carrier of Complex_l2_Space
- (seq . u) is Element of the carrier of Complex_l2_Space
(seq . n) + (- (seq . u)) is Element of the carrier of Complex_l2_Space
the addF of Complex_l2_Space is Relation-like [: the carrier of Complex_l2_Space, the carrier of Complex_l2_Space:] -defined the carrier of Complex_l2_Space -valued Function-like non zero V14([: the carrier of Complex_l2_Space, the carrier of Complex_l2_Space:]) V18([: the carrier of Complex_l2_Space, the carrier of Complex_l2_Space:], the carrier of Complex_l2_Space) Element of bool [:[: the carrier of Complex_l2_Space, the carrier of Complex_l2_Space:], the carrier of Complex_l2_Space:]
[: the carrier of Complex_l2_Space, the carrier of Complex_l2_Space:] is non zero set
[:[: the carrier of Complex_l2_Space, the carrier of Complex_l2_Space:], the carrier of Complex_l2_Space:] is non zero set
bool [:[: the carrier of Complex_l2_Space, the carrier of Complex_l2_Space:], the carrier of Complex_l2_Space:] is non zero set
the addF of Complex_l2_Space . ((seq . n),(- (seq . u))) is Element of the carrier of Complex_l2_Space
K88((seq . n),(- (seq . u))) is set
the addF of Complex_l2_Space . K88((seq . n),(- (seq . u))) is set
seq_id ((seq . n) - (seq . u)) is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
|.(seq_id ((seq . n) - (seq . u))).| is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
|.(seq_id ((seq . n) - (seq . u))).| (#) |.(seq_id ((seq . n) - (seq . u))).| is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
Sum (|.(seq_id ((seq . n) - (seq . u))).| (#) |.(seq_id ((seq . n) - (seq . u))).|) is complex V34() ext-real Element of REAL
||.((seq . n) - (seq . u)).|| is complex V34() ext-real Element of REAL
((seq . n) - (seq . u)) .|. ((seq . n) - (seq . u)) is complex set
|.(((seq . n) - (seq . u)) .|. ((seq . n) - (seq . u))).| is complex V34() ext-real Element of REAL
sqrt |.(((seq . n) - (seq . u)) .|. ((seq . n) - (seq . u))).| is complex V34() ext-real Element of REAL
(seq_id ((seq . n) - (seq . u))) *' is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
(seq_id ((seq . n) - (seq . u))) (#) ((seq_id ((seq . n) - (seq . u))) *') is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
Re ((seq_id ((seq . n) - (seq . u))) (#) ((seq_id ((seq . n) - (seq . u))) *')) is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
Im ((seq_id ((seq . n) - (seq . u))) (#) ((seq_id ((seq . n) - (seq . u))) *')) is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
v is V26() V27() V28() V32() complex V34() ext-real V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
(Re ((seq_id ((seq . n) - (seq . u))) (#) ((seq_id ((seq . n) - (seq . u))) *'))) . v is complex V34() ext-real Element of REAL
seqvn is V26() V27() V28() V32() complex V34() ext-real V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
(Im ((seq_id ((seq . n) - (seq . u))) (#) ((seq_id ((seq . n) - (seq . u))) *'))) . seqvn is complex V34() ext-real Element of REAL
Sum ((seq_id ((seq . n) - (seq . u))) (#) ((seq_id ((seq . n) - (seq . u))) *')) is complex Element of COMPLEX
|.(Sum ((seq_id ((seq . n) - (seq . u))) (#) ((seq_id ((seq . n) - (seq . u))) *'))).| is complex V34() ext-real Element of REAL
|.((seq_id ((seq . n) - (seq . u))) (#) ((seq_id ((seq . n) - (seq . u))) *')).| is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
Sum |.((seq_id ((seq . n) - (seq . u))) (#) ((seq_id ((seq . n) - (seq . u))) *')).| is complex V34() ext-real Element of REAL
|.((seq_id ((seq . n) - (seq . u))) *').| is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
|.(seq_id ((seq . n) - (seq . u))).| (#) |.((seq_id ((seq . n) - (seq . u))) *').| is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
Sum (|.(seq_id ((seq . n) - (seq . u))).| (#) |.((seq_id ((seq . n) - (seq . u))) *').|) is complex V34() ext-real Element of REAL
(seq_id ((seq . n) - (seq . u))) (#) (seq_id ((seq . n) - (seq . u))) is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
|.((seq_id ((seq . n) - (seq . u))) (#) (seq_id ((seq . n) - (seq . u)))).| is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
Sum |.((seq_id ((seq . n) - (seq . u))) (#) (seq_id ((seq . n) - (seq . u)))).| is complex V34() ext-real Element of REAL
sqrt (Sum |.((seq_id ((seq . n) - (seq . u))) (#) (seq_id ((seq . n) - (seq . u)))).|) is complex V34() ext-real Element of REAL
v is V26() V27() V28() V32() complex V34() ext-real V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
(|.(seq_id ((seq . n) - (seq . u))).| (#) |.(seq_id ((seq . n) - (seq . u))).|) . v is complex V34() ext-real Element of REAL
|.((seq_id ((seq . n) - (seq . u))) (#) (seq_id ((seq . n) - (seq . u)))).| . v is complex V34() ext-real Element of REAL
((seq_id ((seq . n) - (seq . u))) (#) (seq_id ((seq . n) - (seq . u)))) . v is complex Element of COMPLEX
|.(((seq_id ((seq . n) - (seq . u))) (#) (seq_id ((seq . n) - (seq . u)))) . v).| is complex V34() ext-real Element of REAL
(tv / 2) ^2 is complex V34() ext-real Element of REAL
(tv / 2) * (tv / 2) is complex set
(sqrt (Sum |.((seq_id ((seq . n) - (seq . u))) (#) (seq_id ((seq . n) - (seq . u)))).|)) ^2 is complex V34() ext-real Element of REAL
(sqrt (Sum |.((seq_id ((seq . n) - (seq . u))) (#) (seq_id ((seq . n) - (seq . u)))).|)) * (sqrt (Sum |.((seq_id ((seq . n) - (seq . u))) (#) (seq_id ((seq . n) - (seq . u)))).|)) is complex set
v is V26() V27() V28() V32() complex V34() ext-real V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
(|.(seq_id ((seq . n) - (seq . u))).| (#) |.(seq_id ((seq . n) - (seq . u))).|) . v is complex V34() ext-real Element of REAL
u is V26() V27() V28() V32() complex V34() ext-real V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
seq . u is Element of the carrier of Complex_l2_Space
seq_id (seq . u) is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
(seq_id nn) - (seq_id (seq . u)) is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
- (seq_id (seq . u)) is Relation-like NAT -defined Function-like V14( NAT ) V38() set
- 1 is non zero complex set
(- 1) (#) (seq_id (seq . u)) is Relation-like NAT -defined Function-like V14( NAT ) V38() set
(seq_id nn) + (- (seq_id (seq . u))) is Relation-like NAT -defined Function-like V14( NAT ) V38() set
|.((seq_id nn) - (seq_id (seq . u))).| is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
|.((seq_id nn) - (seq_id (seq . u))).| (#) |.((seq_id nn) - (seq_id (seq . u))).| is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
Partial_Sums (|.((seq_id nn) - (seq_id (seq . u))).| (#) |.((seq_id nn) - (seq_id (seq . u))).|) is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
n is V26() V27() V28() V32() complex V34() ext-real V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
seq . n is Element of the carrier of Complex_l2_Space
v is V26() V27() V28() V32() complex V34() ext-real V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
seq . v is Element of the carrier of Complex_l2_Space
(seq . n) - (seq . v) is Element of the carrier of Complex_l2_Space
- (seq . v) is Element of the carrier of Complex_l2_Space
(seq . n) + (- (seq . v)) is Element of the carrier of Complex_l2_Space
the addF of Complex_l2_Space is Relation-like [: the carrier of Complex_l2_Space, the carrier of Complex_l2_Space:] -defined the carrier of Complex_l2_Space -valued Function-like non zero V14([: the carrier of Complex_l2_Space, the carrier of Complex_l2_Space:]) V18([: the carrier of Complex_l2_Space, the carrier of Complex_l2_Space:], the carrier of Complex_l2_Space) Element of bool [:[: the carrier of Complex_l2_Space, the carrier of Complex_l2_Space:], the carrier of Complex_l2_Space:]
[: the carrier of Complex_l2_Space, the carrier of Complex_l2_Space:] is non zero set
[:[: the carrier of Complex_l2_Space, the carrier of Complex_l2_Space:], the carrier of Complex_l2_Space:] is non zero set
bool [:[: the carrier of Complex_l2_Space, the carrier of Complex_l2_Space:], the carrier of Complex_l2_Space:] is non zero set
the addF of Complex_l2_Space . ((seq . n),(- (seq . v))) is Element of the carrier of Complex_l2_Space
K88((seq . n),(- (seq . v))) is set
the addF of Complex_l2_Space . K88((seq . n),(- (seq . v))) is set
seq_id ((seq . n) - (seq . v)) is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
seq_id (seq . n) is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
seq_id (seq . v) is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
(seq_id (seq . n)) - (seq_id (seq . v)) is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
- (seq_id (seq . v)) is Relation-like NAT -defined Function-like V14( NAT ) V38() set
(- 1) (#) (seq_id (seq . v)) is Relation-like NAT -defined Function-like V14( NAT ) V38() set
(seq_id (seq . n)) + (- (seq_id (seq . v))) is Relation-like NAT -defined Function-like V14( NAT ) V38() set
seq_id ((seq_id (seq . n)) - (seq_id (seq . v))) is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
n is V26() V27() V28() V32() complex V34() ext-real V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
(Partial_Sums (|.((seq_id nn) - (seq_id (seq . u))).| (#) |.((seq_id nn) - (seq_id (seq . u))).|)) . n is complex V34() ext-real Element of REAL
n + 1 is V26() V27() V28() V32() complex V34() ext-real V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
(Partial_Sums (|.((seq_id nn) - (seq_id (seq . u))).| (#) |.((seq_id nn) - (seq_id (seq . u))).|)) . (n + 1) is complex V34() ext-real Element of REAL
v is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
nn . (n + 1) is complex Element of COMPLEX
seqvn is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
lim seqvn is complex Element of COMPLEX
rseq is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
lim rseq is complex V34() ext-real Element of REAL
m is V26() V27() V28() V32() complex V34() ext-real V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
rseq . m is complex V34() ext-real Element of REAL
seq . m is Element of the carrier of Complex_l2_Space
(seq . m) - (seq . u) is Element of the carrier of Complex_l2_Space
- (seq . u) is Element of the carrier of Complex_l2_Space
(seq . m) + (- (seq . u)) is Element of the carrier of Complex_l2_Space
the addF of Complex_l2_Space is Relation-like [: the carrier of Complex_l2_Space, the carrier of Complex_l2_Space:] -defined the carrier of Complex_l2_Space -valued Function-like non zero V14([: the carrier of Complex_l2_Space, the carrier of Complex_l2_Space:]) V18([: the carrier of Complex_l2_Space, the carrier of Complex_l2_Space:], the carrier of Complex_l2_Space) Element of bool [:[: the carrier of Complex_l2_Space, the carrier of Complex_l2_Space:], the carrier of Complex_l2_Space:]
[: the carrier of Complex_l2_Space, the carrier of Complex_l2_Space:] is non zero set
[:[: the carrier of Complex_l2_Space, the carrier of Complex_l2_Space:], the carrier of Complex_l2_Space:] is non zero set
bool [:[: the carrier of Complex_l2_Space, the carrier of Complex_l2_Space:], the carrier of Complex_l2_Space:] is non zero set
the addF of Complex_l2_Space . ((seq . m),(- (seq . u))) is Element of the carrier of Complex_l2_Space
K88((seq . m),(- (seq . u))) is set
the addF of Complex_l2_Space . K88((seq . m),(- (seq . u))) is set
seq_id ((seq . m) - (seq . u)) is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
|.(seq_id ((seq . m) - (seq . u))).| is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
|.(seq_id ((seq . m) - (seq . u))).| (#) |.(seq_id ((seq . m) - (seq . u))).| is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
Partial_Sums (|.(seq_id ((seq . m) - (seq . u))).| (#) |.(seq_id ((seq . m) - (seq . u))).|) is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
(Partial_Sums (|.(seq_id ((seq . m) - (seq . u))).| (#) |.(seq_id ((seq . m) - (seq . u))).|)) . (n + 1) is complex V34() ext-real Element of REAL
(|.(seq_id ((seq . m) - (seq . u))).| (#) |.(seq_id ((seq . m) - (seq . u))).|) . (n + 1) is complex V34() ext-real Element of REAL
(Partial_Sums (|.(seq_id ((seq . m) - (seq . u))).| (#) |.(seq_id ((seq . m) - (seq . u))).|)) . n is complex V34() ext-real Element of REAL
((|.(seq_id ((seq . m) - (seq . u))).| (#) |.(seq_id ((seq . m) - (seq . u))).|) . (n + 1)) + ((Partial_Sums (|.(seq_id ((seq . m) - (seq . u))).| (#) |.(seq_id ((seq . m) - (seq . u))).|)) . n) is complex V34() ext-real Element of REAL
seq_id (seq . m) is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
(seq_id (seq . m)) - (seq_id (seq . u)) is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
(seq_id (seq . m)) + (- (seq_id (seq . u))) is Relation-like NAT -defined Function-like V14( NAT ) V38() set
|.((seq_id (seq . m)) - (seq_id (seq . u))).| is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
|.((seq_id (seq . m)) - (seq_id (seq . u))).| (#) |.(seq_id ((seq . m) - (seq . u))).| is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
(|.((seq_id (seq . m)) - (seq_id (seq . u))).| (#) |.(seq_id ((seq . m) - (seq . u))).|) . (n + 1) is complex V34() ext-real Element of REAL
((|.((seq_id (seq . m)) - (seq_id (seq . u))).| (#) |.(seq_id ((seq . m) - (seq . u))).|) . (n + 1)) + ((Partial_Sums (|.(seq_id ((seq . m) - (seq . u))).| (#) |.(seq_id ((seq . m) - (seq . u))).|)) . n) is complex V34() ext-real Element of REAL
v . m is complex V34() ext-real Element of REAL
((|.((seq_id (seq . m)) - (seq_id (seq . u))).| (#) |.(seq_id ((seq . m) - (seq . u))).|) . (n + 1)) + (v . m) is complex V34() ext-real Element of REAL
|.((seq_id (seq . m)) - (seq_id (seq . u))).| (#) |.((seq_id (seq . m)) - (seq_id (seq . u))).| is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
(|.((seq_id (seq . m)) - (seq_id (seq . u))).| (#) |.((seq_id (seq . m)) - (seq_id (seq . u))).|) . (n + 1) is complex V34() ext-real Element of REAL
((|.((seq_id (seq . m)) - (seq_id (seq . u))).| (#) |.((seq_id (seq . m)) - (seq_id (seq . u))).|) . (n + 1)) + (v . m) is complex V34() ext-real Element of REAL
- (seq_id (seq . u)) is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
(seq_id (seq . m)) + (- (seq_id (seq . u))) is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
|.((seq_id (seq . m)) + (- (seq_id (seq . u)))).| is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
|.((seq_id (seq . m)) + (- (seq_id (seq . u)))).| . (n + 1) is complex V34() ext-real Element of REAL
|.((seq_id (seq . m)) - (seq_id (seq . u))).| . (n + 1) is complex V34() ext-real Element of REAL
(|.((seq_id (seq . m)) + (- (seq_id (seq . u)))).| . (n + 1)) * (|.((seq_id (seq . m)) - (seq_id (seq . u))).| . (n + 1)) is complex V34() ext-real Element of REAL
((|.((seq_id (seq . m)) + (- (seq_id (seq . u)))).| . (n + 1)) * (|.((seq_id (seq . m)) - (seq_id (seq . u))).| . (n + 1))) + (v . m) is complex V34() ext-real Element of REAL
((seq_id (seq . m)) + (- (seq_id (seq . u)))) . (n + 1) is complex Element of COMPLEX
|.(((seq_id (seq . m)) + (- (seq_id (seq . u)))) . (n + 1)).| is complex V34() ext-real Element of REAL
|.(((seq_id (seq . m)) + (- (seq_id (seq . u)))) . (n + 1)).| * (|.((seq_id (seq . m)) + (- (seq_id (seq . u)))).| . (n + 1)) is complex V34() ext-real Element of REAL
(|.(((seq_id (seq . m)) + (- (seq_id (seq . u)))) . (n + 1)).| * (|.((seq_id (seq . m)) + (- (seq_id (seq . u)))).| . (n + 1))) + (v . m) is complex V34() ext-real Element of REAL
|.(((seq_id (seq . m)) + (- (seq_id (seq . u)))) . (n + 1)).| * |.(((seq_id (seq . m)) + (- (seq_id (seq . u)))) . (n + 1)).| is complex V34() ext-real Element of REAL
(|.(((seq_id (seq . m)) + (- (seq_id (seq . u)))) . (n + 1)).| * |.(((seq_id (seq . m)) + (- (seq_id (seq . u)))) . (n + 1)).|) + (v . m) is complex V34() ext-real Element of REAL
(seq_id (seq . m)) . (n + 1) is complex Element of COMPLEX
(- (seq_id (seq . u))) . (n + 1) is complex Element of COMPLEX
((seq_id (seq . m)) . (n + 1)) + ((- (seq_id (seq . u))) . (n + 1)) is complex Element of COMPLEX
|.(((seq_id (seq . m)) . (n + 1)) + ((- (seq_id (seq . u))) . (n + 1))).| is complex V34() ext-real Element of REAL
|.(((seq_id (seq . m)) . (n + 1)) + ((- (seq_id (seq . u))) . (n + 1))).| * |.(((seq_id (seq . m)) + (- (seq_id (seq . u)))) . (n + 1)).| is complex V34() ext-real Element of REAL
(|.(((seq_id (seq . m)) . (n + 1)) + ((- (seq_id (seq . u))) . (n + 1))).| * |.(((seq_id (seq . m)) + (- (seq_id (seq . u)))) . (n + 1)).|) + (v . m) is complex V34() ext-real Element of REAL
|.(((seq_id (seq . m)) . (n + 1)) + ((- (seq_id (seq . u))) . (n + 1))).| * |.(((seq_id (seq . m)) . (n + 1)) + ((- (seq_id (seq . u))) . (n + 1))).| is complex V34() ext-real Element of REAL
(|.(((seq_id (seq . m)) . (n + 1)) + ((- (seq_id (seq . u))) . (n + 1))).| * |.(((seq_id (seq . m)) . (n + 1)) + ((- (seq_id (seq . u))) . (n + 1))).|) + (v . m) is complex V34() ext-real Element of REAL
(seq_id (seq . u)) . (n + 1) is complex Element of COMPLEX
- ((seq_id (seq . u)) . (n + 1)) is complex Element of COMPLEX
((seq_id (seq . m)) . (n + 1)) + (- ((seq_id (seq . u)) . (n + 1))) is complex Element of COMPLEX
|.(((seq_id (seq . m)) . (n + 1)) + (- ((seq_id (seq . u)) . (n + 1)))).| is complex V34() ext-real Element of REAL
|.(((seq_id (seq . m)) . (n + 1)) + (- ((seq_id (seq . u)) . (n + 1)))).| * |.(((seq_id (seq . m)) . (n + 1)) + ((- (seq_id (seq . u))) . (n + 1))).| is complex V34() ext-real Element of REAL
(|.(((seq_id (seq . m)) . (n + 1)) + (- ((seq_id (seq . u)) . (n + 1)))).| * |.(((seq_id (seq . m)) . (n + 1)) + ((- (seq_id (seq . u))) . (n + 1))).|) + (v . m) is complex V34() ext-real Element of REAL
((seq_id (seq . m)) . (n + 1)) - ((seq_id (seq . u)) . (n + 1)) is complex Element of COMPLEX
|.(((seq_id (seq . m)) . (n + 1)) - ((seq_id (seq . u)) . (n + 1))).| is complex V34() ext-real Element of REAL
|.(((seq_id (seq . m)) . (n + 1)) - ((seq_id (seq . u)) . (n + 1))).| * |.(((seq_id (seq . m)) . (n + 1)) + (- ((seq_id (seq . u)) . (n + 1)))).| is complex V34() ext-real Element of REAL
(|.(((seq_id (seq . m)) . (n + 1)) - ((seq_id (seq . u)) . (n + 1))).| * |.(((seq_id (seq . m)) . (n + 1)) + (- ((seq_id (seq . u)) . (n + 1)))).|) + (v . m) is complex V34() ext-real Element of REAL
seqvn . m is complex Element of COMPLEX
(seqvn . m) - ((seq_id (seq . u)) . (n + 1)) is complex Element of COMPLEX
|.((seqvn . m) - ((seq_id (seq . u)) . (n + 1))).| is complex V34() ext-real Element of REAL
|.((seqvn . m) - ((seq_id (seq . u)) . (n + 1))).| * |.(((seq_id (seq . m)) . (n + 1)) - ((seq_id (seq . u)) . (n + 1))).| is complex V34() ext-real Element of REAL
(|.((seqvn . m) - ((seq_id (seq . u)) . (n + 1))).| * |.(((seq_id (seq . m)) . (n + 1)) - ((seq_id (seq . u)) . (n + 1))).|) + (v . m) is complex V34() ext-real Element of REAL
|.((seqvn . m) - ((seq_id (seq . u)) . (n + 1))).| * |.((seqvn . m) - ((seq_id (seq . u)) . (n + 1))).| is complex V34() ext-real Element of REAL
(|.((seqvn . m) - ((seq_id (seq . u)) . (n + 1))).| * |.((seqvn . m) - ((seq_id (seq . u)) . (n + 1))).|) + (v . m) is complex V34() ext-real Element of REAL
(lim seqvn) - ((seq_id (seq . u)) . (n + 1)) is complex Element of COMPLEX
|.((lim seqvn) - ((seq_id (seq . u)) . (n + 1))).| is complex V34() ext-real Element of REAL
|.((lim seqvn) - ((seq_id (seq . u)) . (n + 1))).| * |.((lim seqvn) - ((seq_id (seq . u)) . (n + 1))).| is complex V34() ext-real Element of REAL
lim v is complex V34() ext-real Element of REAL
(|.((lim seqvn) - ((seq_id (seq . u)) . (n + 1))).| * |.((lim seqvn) - ((seq_id (seq . u)) . (n + 1))).|) + (lim v) is complex V34() ext-real Element of REAL
(nn . (n + 1)) + ((- (seq_id (seq . u))) . (n + 1)) is complex Element of COMPLEX
|.((nn . (n + 1)) + ((- (seq_id (seq . u))) . (n + 1))).| is complex V34() ext-real Element of REAL
(nn . (n + 1)) + (- ((seq_id (seq . u)) . (n + 1))) is complex Element of COMPLEX
|.((nn . (n + 1)) + (- ((seq_id (seq . u)) . (n + 1)))).| is complex V34() ext-real Element of REAL
|.((nn . (n + 1)) + ((- (seq_id (seq . u))) . (n + 1))).| * |.((nn . (n + 1)) + (- ((seq_id (seq . u)) . (n + 1)))).| is complex V34() ext-real Element of REAL
(|.((nn . (n + 1)) + ((- (seq_id (seq . u))) . (n + 1))).| * |.((nn . (n + 1)) + (- ((seq_id (seq . u)) . (n + 1)))).|) + (lim v) is complex V34() ext-real Element of REAL
|.((nn . (n + 1)) + ((- (seq_id (seq . u))) . (n + 1))).| * |.((nn . (n + 1)) + ((- (seq_id (seq . u))) . (n + 1))).| is complex V34() ext-real Element of REAL
(|.((nn . (n + 1)) + ((- (seq_id (seq . u))) . (n + 1))).| * |.((nn . (n + 1)) + ((- (seq_id (seq . u))) . (n + 1))).|) + (lim v) is complex V34() ext-real Element of REAL
nn + (- (seq_id (seq . u))) is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
(nn + (- (seq_id (seq . u)))) . (n + 1) is complex Element of COMPLEX
|.((nn + (- (seq_id (seq . u)))) . (n + 1)).| is complex V34() ext-real Element of REAL
|.((nn + (- (seq_id (seq . u)))) . (n + 1)).| * |.((nn . (n + 1)) + ((- (seq_id (seq . u))) . (n + 1))).| is complex V34() ext-real Element of REAL
(|.((nn + (- (seq_id (seq . u)))) . (n + 1)).| * |.((nn . (n + 1)) + ((- (seq_id (seq . u))) . (n + 1))).|) + (lim v) is complex V34() ext-real Element of REAL
|.((nn + (- (seq_id (seq . u)))) . (n + 1)).| * |.((nn + (- (seq_id (seq . u)))) . (n + 1)).| is complex V34() ext-real Element of REAL
(|.((nn + (- (seq_id (seq . u)))) . (n + 1)).| * |.((nn + (- (seq_id (seq . u)))) . (n + 1)).|) + (lim v) is complex V34() ext-real Element of REAL
|.(nn + (- (seq_id (seq . u)))).| is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
|.(nn + (- (seq_id (seq . u)))).| . (n + 1) is complex V34() ext-real Element of REAL
(|.(nn + (- (seq_id (seq . u)))).| . (n + 1)) * |.((nn + (- (seq_id (seq . u)))) . (n + 1)).| is complex V34() ext-real Element of REAL
((|.(nn + (- (seq_id (seq . u)))).| . (n + 1)) * |.((nn + (- (seq_id (seq . u)))) . (n + 1)).|) + (lim v) is complex V34() ext-real Element of REAL
nn - (seq_id (seq . u)) is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
nn + (- (seq_id (seq . u))) is Relation-like NAT -defined Function-like V14( NAT ) V38() set
|.(nn - (seq_id (seq . u))).| is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
|.(nn - (seq_id (seq . u))).| . (n + 1) is complex V34() ext-real Element of REAL
(|.(nn - (seq_id (seq . u))).| . (n + 1)) * (|.(nn + (- (seq_id (seq . u)))).| . (n + 1)) is complex V34() ext-real Element of REAL
((|.(nn - (seq_id (seq . u))).| . (n + 1)) * (|.(nn + (- (seq_id (seq . u)))).| . (n + 1))) + (lim v) is complex V34() ext-real Element of REAL
|.(nn - (seq_id (seq . u))).| (#) |.(nn - (seq_id (seq . u))).| is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
(|.(nn - (seq_id (seq . u))).| (#) |.(nn - (seq_id (seq . u))).|) . (n + 1) is complex V34() ext-real Element of REAL
((|.(nn - (seq_id (seq . u))).| (#) |.(nn - (seq_id (seq . u))).|) . (n + 1)) + (lim v) is complex V34() ext-real Element of REAL
((|.(nn - (seq_id (seq . u))).| (#) |.(nn - (seq_id (seq . u))).|) . (n + 1)) + ((Partial_Sums (|.((seq_id nn) - (seq_id (seq . u))).| (#) |.((seq_id nn) - (seq_id (seq . u))).|)) . n) is complex V34() ext-real Element of REAL
|.(nn - (seq_id (seq . u))).| (#) |.((seq_id nn) - (seq_id (seq . u))).| is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
(|.(nn - (seq_id (seq . u))).| (#) |.((seq_id nn) - (seq_id (seq . u))).|) . (n + 1) is complex V34() ext-real Element of REAL
((|.(nn - (seq_id (seq . u))).| (#) |.((seq_id nn) - (seq_id (seq . u))).|) . (n + 1)) + ((Partial_Sums (|.((seq_id nn) - (seq_id (seq . u))).| (#) |.((seq_id nn) - (seq_id (seq . u))).|)) . n) is complex V34() ext-real Element of REAL
(|.((seq_id nn) - (seq_id (seq . u))).| (#) |.((seq_id nn) - (seq_id (seq . u))).|) . (n + 1) is complex V34() ext-real Element of REAL
((|.((seq_id nn) - (seq_id (seq . u))).| (#) |.((seq_id nn) - (seq_id (seq . u))).|) . (n + 1)) + ((Partial_Sums (|.((seq_id nn) - (seq_id (seq . u))).| (#) |.((seq_id nn) - (seq_id (seq . u))).|)) . n) is complex V34() ext-real Element of REAL
n is V26() V27() V28() V32() complex V34() ext-real V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
(Partial_Sums (|.((seq_id nn) - (seq_id (seq . u))).| (#) |.((seq_id nn) - (seq_id (seq . u))).|)) . n is complex V34() ext-real Element of REAL
v is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
n + 1 is V26() V27() V28() V32() complex V34() ext-real V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
lim v is complex V34() ext-real Element of REAL
(Partial_Sums (|.((seq_id nn) - (seq_id (seq . u))).| (#) |.((seq_id nn) - (seq_id (seq . u))).|)) . (n + 1) is complex V34() ext-real Element of REAL
n is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
lim n is complex V34() ext-real Element of REAL
(Partial_Sums (|.((seq_id nn) - (seq_id (seq . u))).| (#) |.((seq_id nn) - (seq_id (seq . u))).|)) . 0 is complex V34() ext-real Element of REAL
nn . 0 is complex Element of COMPLEX
v is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
lim v is complex Element of COMPLEX
seqvn is V26() V27() V28() V32() complex V34() ext-real V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
n . seqvn is complex V34() ext-real Element of REAL
seq . seqvn is Element of the carrier of Complex_l2_Space
(seq . seqvn) - (seq . u) is Element of the carrier of Complex_l2_Space
- (seq . u) is Element of the carrier of Complex_l2_Space
(seq . seqvn) + (- (seq . u)) is Element of the carrier of Complex_l2_Space
the addF of Complex_l2_Space is Relation-like [: the carrier of Complex_l2_Space, the carrier of Complex_l2_Space:] -defined the carrier of Complex_l2_Space -valued Function-like non zero V14([: the carrier of Complex_l2_Space, the carrier of Complex_l2_Space:]) V18([: the carrier of Complex_l2_Space, the carrier of Complex_l2_Space:], the carrier of Complex_l2_Space) Element of bool [:[: the carrier of Complex_l2_Space, the carrier of Complex_l2_Space:], the carrier of Complex_l2_Space:]
[: the carrier of Complex_l2_Space, the carrier of Complex_l2_Space:] is non zero set
[:[: the carrier of Complex_l2_Space, the carrier of Complex_l2_Space:], the carrier of Complex_l2_Space:] is non zero set
bool [:[: the carrier of Complex_l2_Space, the carrier of Complex_l2_Space:], the carrier of Complex_l2_Space:] is non zero set
the addF of Complex_l2_Space . ((seq . seqvn),(- (seq . u))) is Element of the carrier of Complex_l2_Space
K88((seq . seqvn),(- (seq . u))) is set
the addF of Complex_l2_Space . K88((seq . seqvn),(- (seq . u))) is set
seq_id ((seq . seqvn) - (seq . u)) is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
|.(seq_id ((seq . seqvn) - (seq . u))).| is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
|.(seq_id ((seq . seqvn) - (seq . u))).| (#) |.(seq_id ((seq . seqvn) - (seq . u))).| is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
Partial_Sums (|.(seq_id ((seq . seqvn) - (seq . u))).| (#) |.(seq_id ((seq . seqvn) - (seq . u))).|) is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
(Partial_Sums (|.(seq_id ((seq . seqvn) - (seq . u))).| (#) |.(seq_id ((seq . seqvn) - (seq . u))).|)) . 0 is complex V34() ext-real Element of REAL
(|.(seq_id ((seq . seqvn) - (seq . u))).| (#) |.(seq_id ((seq . seqvn) - (seq . u))).|) . 0 is complex V34() ext-real Element of REAL
seq_id (seq . seqvn) is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
(seq_id (seq . seqvn)) - (seq_id (seq . u)) is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
(seq_id (seq . seqvn)) + (- (seq_id (seq . u))) is Relation-like NAT -defined Function-like V14( NAT ) V38() set
|.((seq_id (seq . seqvn)) - (seq_id (seq . u))).| is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
|.((seq_id (seq . seqvn)) - (seq_id (seq . u))).| (#) |.(seq_id ((seq . seqvn) - (seq . u))).| is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
(|.((seq_id (seq . seqvn)) - (seq_id (seq . u))).| (#) |.(seq_id ((seq . seqvn) - (seq . u))).|) . 0 is complex V34() ext-real Element of REAL
|.((seq_id (seq . seqvn)) - (seq_id (seq . u))).| (#) |.((seq_id (seq . seqvn)) - (seq_id (seq . u))).| is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
(|.((seq_id (seq . seqvn)) - (seq_id (seq . u))).| (#) |.((seq_id (seq . seqvn)) - (seq_id (seq . u))).|) . 0 is complex V34() ext-real Element of REAL
- (seq_id (seq . u)) is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
(seq_id (seq . seqvn)) + (- (seq_id (seq . u))) is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
|.((seq_id (seq . seqvn)) + (- (seq_id (seq . u)))).| is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
|.((seq_id (seq . seqvn)) + (- (seq_id (seq . u)))).| . 0 is complex V34() ext-real Element of REAL
|.((seq_id (seq . seqvn)) - (seq_id (seq . u))).| . 0 is complex V34() ext-real Element of REAL
(|.((seq_id (seq . seqvn)) + (- (seq_id (seq . u)))).| . 0) * (|.((seq_id (seq . seqvn)) - (seq_id (seq . u))).| . 0) is complex V34() ext-real Element of REAL
((seq_id (seq . seqvn)) + (- (seq_id (seq . u)))) . 0 is complex Element of COMPLEX
|.(((seq_id (seq . seqvn)) + (- (seq_id (seq . u)))) . 0).| is complex V34() ext-real Element of REAL
|.(((seq_id (seq . seqvn)) + (- (seq_id (seq . u)))) . 0).| * (|.((seq_id (seq . seqvn)) + (- (seq_id (seq . u)))).| . 0) is complex V34() ext-real Element of REAL
|.(((seq_id (seq . seqvn)) + (- (seq_id (seq . u)))) . 0).| * |.(((seq_id (seq . seqvn)) + (- (seq_id (seq . u)))) . 0).| is complex V34() ext-real Element of REAL
(seq_id (seq . seqvn)) . 0 is complex Element of COMPLEX
(- (seq_id (seq . u))) . 0 is complex Element of COMPLEX
((seq_id (seq . seqvn)) . 0) + ((- (seq_id (seq . u))) . 0) is complex Element of COMPLEX
|.(((seq_id (seq . seqvn)) . 0) + ((- (seq_id (seq . u))) . 0)).| is complex V34() ext-real Element of REAL
|.(((seq_id (seq . seqvn)) . 0) + ((- (seq_id (seq . u))) . 0)).| * |.(((seq_id (seq . seqvn)) + (- (seq_id (seq . u)))) . 0).| is complex V34() ext-real Element of REAL
|.(((seq_id (seq . seqvn)) . 0) + ((- (seq_id (seq . u))) . 0)).| * |.(((seq_id (seq . seqvn)) . 0) + ((- (seq_id (seq . u))) . 0)).| is complex V34() ext-real Element of REAL
(seq_id (seq . u)) . 0 is complex Element of COMPLEX
- ((seq_id (seq . u)) . 0) is complex Element of COMPLEX
((seq_id (seq . seqvn)) . 0) + (- ((seq_id (seq . u)) . 0)) is complex Element of COMPLEX
|.(((seq_id (seq . seqvn)) . 0) + (- ((seq_id (seq . u)) . 0))).| is complex V34() ext-real Element of REAL
|.(((seq_id (seq . seqvn)) . 0) + (- ((seq_id (seq . u)) . 0))).| * |.(((seq_id (seq . seqvn)) . 0) + ((- (seq_id (seq . u))) . 0)).| is complex V34() ext-real Element of REAL
|.(((seq_id (seq . seqvn)) . 0) + (- ((seq_id (seq . u)) . 0))).| * |.(((seq_id (seq . seqvn)) . 0) + (- ((seq_id (seq . u)) . 0))).| is complex V34() ext-real Element of REAL
v . seqvn is complex Element of COMPLEX
(v . seqvn) - ((seq_id (seq . u)) . 0) is complex Element of COMPLEX
|.((v . seqvn) - ((seq_id (seq . u)) . 0)).| is complex V34() ext-real Element of REAL
((seq_id (seq . seqvn)) . 0) - ((seq_id (seq . u)) . 0) is complex Element of COMPLEX
|.(((seq_id (seq . seqvn)) . 0) - ((seq_id (seq . u)) . 0)).| is complex V34() ext-real Element of REAL
|.((v . seqvn) - ((seq_id (seq . u)) . 0)).| * |.(((seq_id (seq . seqvn)) . 0) - ((seq_id (seq . u)) . 0)).| is complex V34() ext-real Element of REAL
|.((v . seqvn) - ((seq_id (seq . u)) . 0)).| * |.((v . seqvn) - ((seq_id (seq . u)) . 0)).| is complex V34() ext-real Element of REAL
(nn . 0) - ((seq_id (seq . u)) . 0) is complex Element of COMPLEX
|.((nn . 0) - ((seq_id (seq . u)) . 0)).| is complex V34() ext-real Element of REAL
|.((nn . 0) - ((seq_id (seq . u)) . 0)).| * |.((nn . 0) - ((seq_id (seq . u)) . 0)).| is complex V34() ext-real Element of REAL
(nn . 0) + ((- (seq_id (seq . u))) . 0) is complex Element of COMPLEX
|.((nn . 0) + ((- (seq_id (seq . u))) . 0)).| is complex V34() ext-real Element of REAL
(nn . 0) + (- ((seq_id (seq . u)) . 0)) is complex Element of COMPLEX
|.((nn . 0) + (- ((seq_id (seq . u)) . 0))).| is complex V34() ext-real Element of REAL
|.((nn . 0) + ((- (seq_id (seq . u))) . 0)).| * |.((nn . 0) + (- ((seq_id (seq . u)) . 0))).| is complex V34() ext-real Element of REAL
|.((nn . 0) + ((- (seq_id (seq . u))) . 0)).| * |.((nn . 0) + ((- (seq_id (seq . u))) . 0)).| is complex V34() ext-real Element of REAL
nn + (- (seq_id (seq . u))) is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
(nn + (- (seq_id (seq . u)))) . 0 is complex Element of COMPLEX
|.((nn + (- (seq_id (seq . u)))) . 0).| is complex V34() ext-real Element of REAL
|.((nn + (- (seq_id (seq . u)))) . 0).| * |.((nn . 0) + ((- (seq_id (seq . u))) . 0)).| is complex V34() ext-real Element of REAL
nn - (seq_id (seq . u)) is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
nn + (- (seq_id (seq . u))) is Relation-like NAT -defined Function-like V14( NAT ) V38() set
(nn - (seq_id (seq . u))) . 0 is complex Element of COMPLEX
|.((nn - (seq_id (seq . u))) . 0).| is complex V34() ext-real Element of REAL
|.((nn - (seq_id (seq . u))) . 0).| * |.((nn + (- (seq_id (seq . u)))) . 0).| is complex V34() ext-real Element of REAL
|.(nn - (seq_id (seq . u))).| is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
|.(nn - (seq_id (seq . u))).| . 0 is complex V34() ext-real Element of REAL
(|.(nn - (seq_id (seq . u))).| . 0) * |.((nn - (seq_id (seq . u))) . 0).| is complex V34() ext-real Element of REAL
(|.(nn - (seq_id (seq . u))).| . 0) * (|.(nn - (seq_id (seq . u))).| . 0) is complex V34() ext-real Element of REAL
|.(nn - (seq_id (seq . u))).| (#) |.(nn - (seq_id (seq . u))).| is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
(|.(nn - (seq_id (seq . u))).| (#) |.(nn - (seq_id (seq . u))).|) . 0 is complex V34() ext-real Element of REAL
Partial_Sums (|.(nn - (seq_id (seq . u))).| (#) |.(nn - (seq_id (seq . u))).|) is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
(Partial_Sums (|.(nn - (seq_id (seq . u))).| (#) |.(nn - (seq_id (seq . u))).|)) . 0 is complex V34() ext-real Element of REAL
|.((seq_id nn) - (seq_id (seq . u))).| (#) |.(nn - (seq_id (seq . u))).| is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
Partial_Sums (|.((seq_id nn) - (seq_id (seq . u))).| (#) |.(nn - (seq_id (seq . u))).|) is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
(Partial_Sums (|.((seq_id nn) - (seq_id (seq . u))).| (#) |.(nn - (seq_id (seq . u))).|)) . 0 is complex V34() ext-real Element of REAL
n is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
lim n is complex V34() ext-real Element of REAL
v is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
n is V26() V27() V28() V32() complex V34() ext-real V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
lim v is complex V34() ext-real Element of REAL
(Partial_Sums (|.((seq_id nn) - (seq_id (seq . u))).| (#) |.((seq_id nn) - (seq_id (seq . u))).|)) . n is complex V34() ext-real Element of REAL
u is V26() V27() V28() V32() complex V34() ext-real V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
seq . u is Element of the carrier of Complex_l2_Space
seq_id (seq . u) is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
(seq_id nn) - (seq_id (seq . u)) is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
- (seq_id (seq . u)) is Relation-like NAT -defined Function-like V14( NAT ) V38() set
- 1 is non zero complex set
(- 1) (#) (seq_id (seq . u)) is Relation-like NAT -defined Function-like V14( NAT ) V38() set
(seq_id nn) + (- (seq_id (seq . u))) is Relation-like NAT -defined Function-like V14( NAT ) V38() set
|.((seq_id nn) - (seq_id (seq . u))).| is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
|.((seq_id nn) - (seq_id (seq . u))).| (#) |.((seq_id nn) - (seq_id (seq . u))).| is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
((seq_id nn) - (seq_id (seq . u))) *' is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
((seq_id nn) - (seq_id (seq . u))) (#) (((seq_id nn) - (seq_id (seq . u))) *') is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
Sum (((seq_id nn) - (seq_id (seq . u))) (#) (((seq_id nn) - (seq_id (seq . u))) *')) is complex Element of COMPLEX
|.(Sum (((seq_id nn) - (seq_id (seq . u))) (#) (((seq_id nn) - (seq_id (seq . u))) *'))).| is complex V34() ext-real Element of REAL
Partial_Sums (|.((seq_id nn) - (seq_id (seq . u))).| (#) |.((seq_id nn) - (seq_id (seq . u))).|) is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
n is V26() V27() V28() V32() complex V34() ext-real V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
(Partial_Sums (|.((seq_id nn) - (seq_id (seq . u))).| (#) |.((seq_id nn) - (seq_id (seq . u))).|)) . n is complex V34() ext-real Element of REAL
v is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
seqvn is V26() V27() V28() V32() complex V34() ext-real V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
v . seqvn is complex V34() ext-real Element of REAL
seq . seqvn is Element of the carrier of Complex_l2_Space
(seq . seqvn) - (seq . u) is Element of the carrier of Complex_l2_Space
- (seq . u) is Element of the carrier of Complex_l2_Space
(seq . seqvn) + (- (seq . u)) is Element of the carrier of Complex_l2_Space
the addF of Complex_l2_Space is Relation-like [: the carrier of Complex_l2_Space, the carrier of Complex_l2_Space:] -defined the carrier of Complex_l2_Space -valued Function-like non zero V14([: the carrier of Complex_l2_Space, the carrier of Complex_l2_Space:]) V18([: the carrier of Complex_l2_Space, the carrier of Complex_l2_Space:], the carrier of Complex_l2_Space) Element of bool [:[: the carrier of Complex_l2_Space, the carrier of Complex_l2_Space:], the carrier of Complex_l2_Space:]
[: the carrier of Complex_l2_Space, the carrier of Complex_l2_Space:] is non zero set
[:[: the carrier of Complex_l2_Space, the carrier of Complex_l2_Space:], the carrier of Complex_l2_Space:] is non zero set
bool [:[: the carrier of Complex_l2_Space, the carrier of Complex_l2_Space:], the carrier of Complex_l2_Space:] is non zero set
the addF of Complex_l2_Space . ((seq . seqvn),(- (seq . u))) is Element of the carrier of Complex_l2_Space
K88((seq . seqvn),(- (seq . u))) is set
the addF of Complex_l2_Space . K88((seq . seqvn),(- (seq . u))) is set
seq_id ((seq . seqvn) - (seq . u)) is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
|.(seq_id ((seq . seqvn) - (seq . u))).| is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
|.(seq_id ((seq . seqvn) - (seq . u))).| (#) |.(seq_id ((seq . seqvn) - (seq . u))).| is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
rseq is V26() V27() V28() V32() complex V34() ext-real V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
(|.(seq_id ((seq . seqvn) - (seq . u))).| (#) |.(seq_id ((seq . seqvn) - (seq . u))).|) . rseq is complex V34() ext-real Element of REAL
Partial_Sums (|.(seq_id ((seq . seqvn) - (seq . u))).| (#) |.(seq_id ((seq . seqvn) - (seq . u))).|) is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
(Partial_Sums (|.(seq_id ((seq . seqvn) - (seq . u))).| (#) |.(seq_id ((seq . seqvn) - (seq . u))).|)) . n is complex V34() ext-real Element of REAL
Sum (|.(seq_id ((seq . seqvn) - (seq . u))).| (#) |.(seq_id ((seq . seqvn) - (seq . u))).|) is complex V34() ext-real Element of REAL
lim v is complex V34() ext-real Element of REAL
n is V26() V27() V28() V32() complex V34() ext-real V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
(Partial_Sums (|.((seq_id nn) - (seq_id (seq . u))).| (#) |.((seq_id nn) - (seq_id (seq . u))).|)) . n is complex V34() ext-real Element of REAL
n is V26() V27() V28() V32() complex V34() ext-real V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
(|.((seq_id nn) - (seq_id (seq . u))).| (#) |.((seq_id nn) - (seq_id (seq . u))).|) . n is complex V34() ext-real Element of REAL
|.((seq_id nn) - (seq_id (seq . u))).| . n is complex V34() ext-real Element of REAL
(|.((seq_id nn) - (seq_id (seq . u))).| . n) * (|.((seq_id nn) - (seq_id (seq . u))).| . n) is complex V34() ext-real Element of REAL
Sum (|.((seq_id nn) - (seq_id (seq . u))).| (#) |.((seq_id nn) - (seq_id (seq . u))).|) is complex V34() ext-real Element of REAL
lim (Partial_Sums (|.((seq_id nn) - (seq_id (seq . u))).| (#) |.((seq_id nn) - (seq_id (seq . u))).|)) is complex V34() ext-real Element of REAL
|.(((seq_id nn) - (seq_id (seq . u))) *').| is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
|.((seq_id nn) - (seq_id (seq . u))).| (#) |.(((seq_id nn) - (seq_id (seq . u))) *').| is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
|.(((seq_id nn) - (seq_id (seq . u))) (#) (((seq_id nn) - (seq_id (seq . u))) *')).| is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
Sum |.(((seq_id nn) - (seq_id (seq . u))) (#) (((seq_id nn) - (seq_id (seq . u))) *')).| is complex V34() ext-real Element of REAL
|.(seq_id nn).| is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
|.(seq_id nn).| (#) |.(seq_id nn).| is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
e is V26() V27() V28() V32() complex V34() ext-real V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
(|.(seq_id nn).| (#) |.(seq_id nn).|) . e is complex V34() ext-real Element of REAL
|.(seq_id nn).| . e is complex V34() ext-real Element of REAL
(|.(seq_id nn).| . e) * (|.(seq_id nn).| . e) is complex V34() ext-real Element of REAL
1 * 1 is non zero V26() V27() V28() V32() complex V34() ext-real V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
e is V26() V27() V28() V32() complex V34() ext-real V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
seq . e is Element of the carrier of Complex_l2_Space
seq_id (seq . e) is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
|.(seq_id (seq . e)).| is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
|.(seq_id (seq . e)).| (#) |.(seq_id (seq . e)).| is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
(seq_id nn) - (seq_id (seq . e)) is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
- (seq_id (seq . e)) is Relation-like NAT -defined Function-like V14( NAT ) V38() set
- 1 is non zero complex set
(- 1) (#) (seq_id (seq . e)) is Relation-like NAT -defined Function-like V14( NAT ) V38() set
(seq_id nn) + (- (seq_id (seq . e))) is Relation-like NAT -defined Function-like V14( NAT ) V38() set
|.((seq_id nn) - (seq_id (seq . e))).| is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
|.((seq_id nn) - (seq_id (seq . e))).| (#) |.((seq_id nn) - (seq_id (seq . e))).| is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
2 (#) (|.(seq_id (seq . e)).| (#) |.(seq_id (seq . e)).|) is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
2 (#) (|.((seq_id nn) - (seq_id (seq . e))).| (#) |.((seq_id nn) - (seq_id (seq . e))).|) is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
(2 (#) (|.((seq_id nn) - (seq_id (seq . e))).| (#) |.((seq_id nn) - (seq_id (seq . e))).|)) + (2 (#) (|.(seq_id (seq . e)).| (#) |.(seq_id (seq . e)).|)) is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
n is V26() V27() V28() V32() complex V34() ext-real V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
(|.(seq_id nn).| (#) |.(seq_id nn).|) . n is complex V34() ext-real Element of REAL
((2 (#) (|.((seq_id nn) - (seq_id (seq . e))).| (#) |.((seq_id nn) - (seq_id (seq . e))).|)) + (2 (#) (|.(seq_id (seq . e)).| (#) |.(seq_id (seq . e)).|))) . n is complex V34() ext-real Element of REAL
(2 (#) (|.((seq_id nn) - (seq_id (seq . e))).| (#) |.((seq_id nn) - (seq_id (seq . e))).|)) . n is complex V34() ext-real Element of REAL
(2 (#) (|.(seq_id (seq . e)).| (#) |.(seq_id (seq . e)).|)) . n is complex V34() ext-real Element of REAL
((2 (#) (|.((seq_id nn) - (seq_id (seq . e))).| (#) |.((seq_id nn) - (seq_id (seq . e))).|)) . n) + ((2 (#) (|.(seq_id (seq . e)).| (#) |.(seq_id (seq . e)).|)) . n) is complex V34() ext-real Element of REAL
(|.((seq_id nn) - (seq_id (seq . e))).| (#) |.((seq_id nn) - (seq_id (seq . e))).|) . n is complex V34() ext-real Element of REAL
2 * ((|.((seq_id nn) - (seq_id (seq . e))).| (#) |.((seq_id nn) - (seq_id (seq . e))).|) . n) is complex V34() ext-real Element of REAL
(2 * ((|.((seq_id nn) - (seq_id (seq . e))).| (#) |.((seq_id nn) - (seq_id (seq . e))).|) . n)) + ((2 (#) (|.(seq_id (seq . e)).| (#) |.(seq_id (seq . e)).|)) . n) is complex V34() ext-real Element of REAL
(|.(seq_id (seq . e)).| (#) |.(seq_id (seq . e)).|) . n is complex V34() ext-real Element of REAL
2 * ((|.(seq_id (seq . e)).| (#) |.(seq_id (seq . e)).|) . n) is complex V34() ext-real Element of REAL
(2 * ((|.((seq_id nn) - (seq_id (seq . e))).| (#) |.((seq_id nn) - (seq_id (seq . e))).|) . n)) + (2 * ((|.(seq_id (seq . e)).| (#) |.(seq_id (seq . e)).|) . n)) is complex V34() ext-real Element of REAL
(seq_id (seq . e)) . n is complex Element of COMPLEX
(seq_id nn) . n is complex Element of COMPLEX
|.(seq_id (seq . e)).| . n is complex V34() ext-real Element of REAL
(|.(seq_id (seq . e)).| . n) * (|.(seq_id (seq . e)).| . n) is complex V34() ext-real Element of REAL
2 * ((|.(seq_id (seq . e)).| . n) * (|.(seq_id (seq . e)).| . n)) is complex V34() ext-real Element of REAL
|.((seq_id (seq . e)) . n).| is complex V34() ext-real Element of REAL
|.((seq_id (seq . e)) . n).| * (|.(seq_id (seq . e)).| . n) is complex V34() ext-real Element of REAL
2 * (|.((seq_id (seq . e)) . n).| * (|.(seq_id (seq . e)).| . n)) is complex V34() ext-real Element of REAL
|.((seq_id (seq . e)) . n).| * |.((seq_id (seq . e)) . n).| is complex V34() ext-real Element of REAL
2 * (|.((seq_id (seq . e)) . n).| * |.((seq_id (seq . e)) . n).|) is complex V34() ext-real Element of REAL
2 * |.((seq_id (seq . e)) . n).| is complex V34() ext-real Element of REAL
(2 * |.((seq_id (seq . e)) . n).|) * |.((seq_id (seq . e)) . n).| is complex V34() ext-real Element of REAL
|.((seq_id nn) - (seq_id (seq . e))).| . n is complex V34() ext-real Element of REAL
- (seq_id (seq . e)) is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
(seq_id nn) + (- (seq_id (seq . e))) is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
((seq_id nn) + (- (seq_id (seq . e)))) . n is complex Element of COMPLEX
|.(((seq_id nn) + (- (seq_id (seq . e)))) . n).| is complex V34() ext-real Element of REAL
(- (seq_id (seq . e))) . n is complex Element of COMPLEX
((seq_id nn) . n) + ((- (seq_id (seq . e))) . n) is complex Element of COMPLEX
|.(((seq_id nn) . n) + ((- (seq_id (seq . e))) . n)).| is complex V34() ext-real Element of REAL
- ((seq_id (seq . e)) . n) is complex Element of COMPLEX
((seq_id nn) . n) + (- ((seq_id (seq . e)) . n)) is complex Element of COMPLEX
|.(((seq_id nn) . n) + (- ((seq_id (seq . e)) . n))).| is complex V34() ext-real Element of REAL
((seq_id nn) . n) - ((seq_id (seq . e)) . n) is complex Element of COMPLEX
|.(((seq_id nn) . n) - ((seq_id (seq . e)) . n)).| is complex V34() ext-real Element of REAL
|.(((seq_id nn) . n) - ((seq_id (seq . e)) . n)).| * |.(((seq_id nn) . n) - ((seq_id (seq . e)) . n)).| is complex V34() ext-real Element of REAL
2 * |.(((seq_id nn) . n) - ((seq_id (seq . e)) . n)).| is complex V34() ext-real Element of REAL
(2 * |.(((seq_id nn) . n) - ((seq_id (seq . e)) . n)).|) * |.(((seq_id nn) . n) - ((seq_id (seq . e)) . n)).| is complex V34() ext-real Element of REAL
|.(seq_id nn).| . n is complex V34() ext-real Element of REAL
(|.(seq_id nn).| . n) * (|.(seq_id nn).| . n) is complex V34() ext-real Element of REAL
|.((seq_id nn) . n).| is complex V34() ext-real Element of REAL
|.((seq_id nn) . n).| * (|.(seq_id nn).| . n) is complex V34() ext-real Element of REAL
|.((seq_id nn) . n).| * |.((seq_id nn) . n).| is complex V34() ext-real Element of REAL
tv is Element of the carrier of Complex_l2_Space
e is complex V34() ext-real Element of REAL
e * e is complex V34() ext-real Element of REAL
m is V26() V27() V28() V32() complex V34() ext-real V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
n is V26() V27() V28() V32() complex V34() ext-real V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
seq . n is Element of the carrier of Complex_l2_Space
seq_id (seq . n) is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
u is Element of the carrier of Complex_l2_Space
v is Element of the carrier of Complex_l2_Space
u - v is Element of the carrier of Complex_l2_Space
- v is Element of the carrier of Complex_l2_Space
u + (- v) is Element of the carrier of Complex_l2_Space
the addF of Complex_l2_Space is Relation-like [: the carrier of Complex_l2_Space, the carrier of Complex_l2_Space:] -defined the carrier of Complex_l2_Space -valued Function-like non zero V14([: the carrier of Complex_l2_Space, the carrier of Complex_l2_Space:]) V18([: the carrier of Complex_l2_Space, the carrier of Complex_l2_Space:], the carrier of Complex_l2_Space) Element of bool [:[: the carrier of Complex_l2_Space, the carrier of Complex_l2_Space:], the carrier of Complex_l2_Space:]
[: the carrier of Complex_l2_Space, the carrier of Complex_l2_Space:] is non zero set
[:[: the carrier of Complex_l2_Space, the carrier of Complex_l2_Space:], the carrier of Complex_l2_Space:] is non zero set
bool [:[: the carrier of Complex_l2_Space, the carrier of Complex_l2_Space:], the carrier of Complex_l2_Space:] is non zero set
the addF of Complex_l2_Space . (u,(- v)) is Element of the carrier of Complex_l2_Space
K88(u,(- v)) is set
the addF of Complex_l2_Space . K88(u,(- v)) is set
(u - v) .|. (u - v) is complex set
Re ((u - v) .|. (u - v)) is complex V34() ext-real Element of REAL
|.((u - v) .|. (u - v)).| is complex V34() ext-real Element of REAL
seq_id (u - v) is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
(seq_id nn) - (seq_id (seq . n)) is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
- (seq_id (seq . n)) is Relation-like NAT -defined Function-like V14( NAT ) V38() set
- 1 is non zero complex set
(- 1) (#) (seq_id (seq . n)) is Relation-like NAT -defined Function-like V14( NAT ) V38() set
(seq_id nn) + (- (seq_id (seq . n))) is Relation-like NAT -defined Function-like V14( NAT ) V38() set
((seq_id nn) - (seq_id (seq . n))) *' is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
((seq_id nn) - (seq_id (seq . n))) (#) (((seq_id nn) - (seq_id (seq . n))) *') is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
Sum (((seq_id nn) - (seq_id (seq . n))) (#) (((seq_id nn) - (seq_id (seq . n))) *')) is complex Element of COMPLEX
|.(Sum (((seq_id nn) - (seq_id (seq . n))) (#) (((seq_id nn) - (seq_id (seq . n))) *'))).| is complex V34() ext-real Element of REAL
e ^2 is complex V34() ext-real Element of REAL
e * e is complex set
sqrt (e ^2) is complex V34() ext-real Element of REAL
sqrt |.((u - v) .|. (u - v)).| is complex V34() ext-real Element of REAL
(seq . n) - tv is Element of the carrier of Complex_l2_Space
- tv is Element of the carrier of Complex_l2_Space
(seq . n) + (- tv) is Element of the carrier of Complex_l2_Space
the addF of Complex_l2_Space . ((seq . n),(- tv)) is Element of the carrier of Complex_l2_Space
K88((seq . n),(- tv)) is set
the addF of Complex_l2_Space . K88((seq . n),(- tv)) is set
||.((seq . n) - tv).|| is complex V34() ext-real Element of REAL
tv - (seq . n) is Element of the carrier of Complex_l2_Space
- (seq . n) is Element of the carrier of Complex_l2_Space
tv + (- (seq . n)) is Element of the carrier of Complex_l2_Space
the addF of Complex_l2_Space . (tv,(- (seq . n))) is Element of the carrier of Complex_l2_Space
K88(tv,(- (seq . n))) is set
the addF of Complex_l2_Space . K88(tv,(- (seq . n))) is set
- (tv - (seq . n)) is Element of the carrier of Complex_l2_Space
||.(- (tv - (seq . n))).|| is complex V34() ext-real Element of REAL
||.(tv - (seq . n)).|| is complex V34() ext-real Element of REAL
seq is complex set
Re seq is complex V34() ext-real Element of REAL
n is complex set
Im n is complex V34() ext-real Element of REAL
(Re seq) * (Im n) is complex V34() ext-real Element of REAL
Re n is complex V34() ext-real Element of REAL
Im seq is complex V34() ext-real Element of REAL
(Re n) * (Im seq) is complex V34() ext-real Element of REAL
(Re seq) * (Re n) is complex V34() ext-real Element of REAL
(Im seq) * (Im n) is complex V34() ext-real Element of REAL
((Re seq) * (Re n)) + ((Im seq) * (Im n)) is complex V34() ext-real Element of REAL
seq + n is complex set
|.(seq + n).| is complex V34() ext-real Element of REAL
|.seq.| is complex V34() ext-real Element of REAL
|.n.| is complex V34() ext-real Element of REAL
|.seq.| + |.n.| is complex V34() ext-real Element of REAL
seq is complex set
n is complex set
seq * n is complex set
|.(seq * n).| is complex V34() ext-real Element of REAL
2 * |.(seq * n).| is complex V34() ext-real Element of REAL
|.seq.| is complex V34() ext-real Element of REAL
|.seq.| ^2 is complex V34() ext-real Element of REAL
|.seq.| * |.seq.| is complex set
|.n.| is complex V34() ext-real Element of REAL
|.n.| ^2 is complex V34() ext-real Element of REAL
|.n.| * |.n.| is complex set
(|.seq.| ^2) + (|.n.| ^2) is complex V34() ext-real Element of REAL
seq is complex set
n is complex set
seq + n is complex set
|.(seq + n).| is complex V34() ext-real Element of REAL
|.(seq + n).| * |.(seq + n).| is complex V34() ext-real Element of REAL
|.seq.| is complex V34() ext-real Element of REAL
2 * |.seq.| is complex V34() ext-real Element of REAL
(2 * |.seq.|) * |.seq.| is complex V34() ext-real Element of REAL
|.n.| is complex V34() ext-real Element of REAL
2 * |.n.| is complex V34() ext-real Element of REAL
(2 * |.n.|) * |.n.| is complex V34() ext-real Element of REAL
((2 * |.seq.|) * |.seq.|) + ((2 * |.n.|) * |.n.|) is complex V34() ext-real Element of REAL
nn is complex set
|.nn.| is complex V34() ext-real Element of REAL
|.nn.| * |.nn.| is complex V34() ext-real Element of REAL
seqt is complex set
nn - seqt is complex set
|.(nn - seqt).| is complex V34() ext-real Element of REAL
2 * |.(nn - seqt).| is complex V34() ext-real Element of REAL
(2 * |.(nn - seqt).|) * |.(nn - seqt).| is complex V34() ext-real Element of REAL
|.seqt.| is complex V34() ext-real Element of REAL
2 * |.seqt.| is complex V34() ext-real Element of REAL
(2 * |.seqt.|) * |.seqt.| is complex V34() ext-real Element of REAL
((2 * |.(nn - seqt).|) * |.(nn - seqt).|) + ((2 * |.seqt.|) * |.seqt.|) is complex V34() ext-real Element of REAL
seq is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
seq *' is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
Partial_Sums (seq *') is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
Partial_Sums seq is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
(Partial_Sums seq) *' is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
seq is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
Re seq is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
Im seq is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
Partial_Sums seq is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
|.(Partial_Sums seq).| is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
n is V26() V27() V28() V32() complex V34() ext-real V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
|.(Partial_Sums seq).| . n is complex V34() ext-real Element of REAL
|.seq.| is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
Partial_Sums |.seq.| is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() V44() Element of bool [:NAT,REAL:]
(Partial_Sums |.seq.|) . n is complex V34() ext-real Element of REAL
seq is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
seq *' is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
Sum (seq *') is complex Element of COMPLEX
Sum seq is complex Element of COMPLEX
(Sum seq) *' is complex Element of COMPLEX
seq is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
Sum seq is complex Element of COMPLEX
|.(Sum seq).| is complex V34() ext-real Element of REAL
|.seq.| is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
Sum |.seq.| is complex V34() ext-real Element of REAL
seq is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
Re seq is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
Im seq is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
Sum seq is complex Element of COMPLEX
|.(Sum seq).| is complex V34() ext-real Element of REAL
|.seq.| is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
Sum |.seq.| is complex V34() ext-real Element of REAL
seq is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
seq *' is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
seq (#) (seq *') is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
Re (seq (#) (seq *')) is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
n is V26() V27() V28() V32() complex V34() ext-real V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
(Re (seq (#) (seq *'))) . n is complex V34() ext-real Element of REAL
nn is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
nn *' is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
nn (#) (nn *') is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
Im (nn (#) (nn *')) is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
seqt is V26() V27() V28() V32() complex V34() ext-real V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
(Im (nn (#) (nn *'))) . seqt is complex V34() ext-real Element of REAL
seq is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
|.seq.| is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
Sum |.seq.| is complex V34() ext-real Element of REAL
Partial_Sums |.seq.| is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() V44() Element of bool [:NAT,REAL:]
n is V26() V27() V28() V32() complex V34() ext-real V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
(Partial_Sums |.seq.|) . n is complex V34() ext-real Element of REAL
lim (Partial_Sums |.seq.|) is complex V34() ext-real Element of REAL
n is V26() V27() V28() V32() complex V34() ext-real V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
|.seq.| . n is complex V34() ext-real Element of REAL
n is V26() V27() V28() V32() complex V34() ext-real V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
|.seq.| . n is complex V34() ext-real Element of REAL
nn is V26() V27() V28() V32() complex V34() ext-real V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
(Partial_Sums |.seq.|) . nn is complex V34() ext-real Element of REAL
|.seq.| . 0 is complex V34() ext-real Element of REAL
seq . 0 is complex Element of COMPLEX
|.(seq . 0).| is complex V34() ext-real Element of REAL
nn + 0 is V26() V27() V28() V32() complex V34() ext-real V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
(Partial_Sums |.seq.|) . 0 is complex V34() ext-real Element of REAL
(Partial_Sums |.seq.|) . n is complex V34() ext-real Element of REAL
n - 1 is complex V34() ext-real Element of REAL
seq . n is complex Element of COMPLEX
|.(seq . n).| is complex V34() ext-real Element of REAL
(n - 1) + 1 is complex V34() ext-real Element of REAL
0 + 1 is V26() V27() V28() V32() complex V34() ext-real V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
(Partial_Sums |.seq.|) . (n - 1) is complex V34() ext-real Element of REAL
(|.seq.| . n) + 0 is complex V34() ext-real Element of REAL
(|.seq.| . n) + ((Partial_Sums |.seq.|) . (n - 1)) is complex V34() ext-real Element of REAL
n is V26() V27() V28() V32() complex V34() ext-real V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
seq . n is complex Element of COMPLEX
|.seq.| . n is complex V34() ext-real Element of REAL
|.(seq . n).| is complex V34() ext-real Element of REAL
n is V26() V27() V28() V32() complex V34() ext-real V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
seq . n is complex Element of COMPLEX
seq is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
|.seq.| is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
seq *' is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
|.(seq *').| is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
n is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
nn is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
seq is complex set
lim nn is complex V34() ext-real Element of REAL
lim n is complex Element of COMPLEX
(lim n) - seq is complex set
|.((lim n) - seq).| is complex V34() ext-real Element of REAL
|.((lim n) - seq).| * |.((lim n) - seq).| is complex V34() ext-real Element of REAL
nn is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
n is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
seqt is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
seq is complex set
lim seqt is complex V34() ext-real Element of REAL
lim nn is complex Element of COMPLEX
(lim nn) - seq is complex set
|.((lim nn) - seq).| is complex V34() ext-real Element of REAL
|.((lim nn) - seq).| * |.((lim nn) - seq).| is complex V34() ext-real Element of REAL
lim n is complex V34() ext-real Element of REAL
(|.((lim nn) - seq).| * |.((lim nn) - seq).|) + (lim n) is complex V34() ext-real Element of REAL
n is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
nn is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
seq is complex set
lim nn is complex V34() ext-real Element of REAL
lim n is complex Element of COMPLEX
(lim n) - seq is complex set
|.((lim n) - seq).| is complex V34() ext-real Element of REAL
|.((lim n) - seq).| * |.((lim n) - seq).| is complex V34() ext-real Element of REAL
nn is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
n is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
seqt is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
seq is complex set
lim seqt is complex V34() ext-real Element of REAL
lim nn is complex Element of COMPLEX
(lim nn) - seq is complex set
|.((lim nn) - seq).| is complex V34() ext-real Element of REAL
|.((lim nn) - seq).| * |.((lim nn) - seq).| is complex V34() ext-real Element of REAL
lim n is complex V34() ext-real Element of REAL
(|.((lim nn) - seq).| * |.((lim nn) - seq).|) + (lim n) is complex V34() ext-real Element of REAL