:: CSSPACE3 semantic presentation

REAL is non empty V52() V64() V65() V66() V70() set
NAT is non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() Element of bool REAL
bool REAL is non empty set
COMPLEX is non empty V52() V64() V70() set
omega is non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() set
bool omega is non empty set
bool NAT is non empty set
RAT is non empty V52() V64() V65() V66() V67() V70() set
INT is non empty V52() V64() V65() V66() V67() V68() V70() set
[:NAT,REAL:] is non empty V38() V39() V40() set
bool [:NAT,REAL:] is non empty set
[:NAT,COMPLEX:] is non empty V38() set
bool [:NAT,COMPLEX:] is non empty set
the_set_of_ComplexSequences is non empty set
[:the_set_of_ComplexSequences,the_set_of_ComplexSequences:] is non empty set
[:[:the_set_of_ComplexSequences,the_set_of_ComplexSequences:],the_set_of_ComplexSequences:] is non empty set
bool [:[:the_set_of_ComplexSequences,the_set_of_ComplexSequences:],the_set_of_ComplexSequences:] is non empty set
[:COMPLEX,the_set_of_ComplexSequences:] is non empty set
[:[:COMPLEX,the_set_of_ComplexSequences:],the_set_of_ComplexSequences:] is non empty set
bool [:[:COMPLEX,the_set_of_ComplexSequences:],the_set_of_ComplexSequences:] is non empty set
Linear_Space_of_ComplexSequences is non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital CLSStruct
the carrier of Linear_Space_of_ComplexSequences is non empty set
bool the carrier of Linear_Space_of_ComplexSequences is non empty 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 empty set
{} is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V33() real ext-real V64() V65() V66() V67() V68() V69() V70() set
1 is non empty epsilon-transitive epsilon-connected ordinal natural V33() real ext-real positive V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V33() real ext-real V50() V63() V64() V65() V66() V67() V68() V69() V70() Element of NAT
CZeroseq is Element of the_set_of_ComplexSequences
0c is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V33() real ext-real 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 empty 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 empty 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:]
CLSStruct(# the_set_of_ComplexSequences,CZeroseq,l_add,l_mult #) is non empty Abelian strict CLSStruct
the carrier of CLSStruct(# the_set_of_ComplexSequences,CZeroseq,l_add,l_mult #) is non empty set
1r is V33() Element of COMPLEX
- 1r is V33() Element of COMPLEX
|.0.| is V33() real ext-real V63() Element of REAL
2 is non empty epsilon-transitive epsilon-connected ordinal natural V33() real ext-real positive V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
vseq is set
f is set
bool the_set_of_ComplexSequences is non empty set
vseq is Element of bool the carrier of Linear_Space_of_ComplexSequences
f is Element of bool the carrier of Linear_Space_of_ComplexSequences
tseq is set
seq_id tseq is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
tseq is set
seq_id tseq is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
() is Element of bool the carrier of Linear_Space_of_ComplexSequences
vseq is V33() set
f is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
lim f is V33() Element of COMPLEX
(lim f) - vseq is V33() set
|.((lim f) - vseq).| is V33() real ext-real Element of REAL
tseq is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
lim tseq is V33() real ext-real Element of REAL
tv is V33() Element of COMPLEX
NAT --> tv is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
e is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
m is epsilon-transitive epsilon-connected ordinal natural V33() real ext-real V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
e . m is V33() Element of COMPLEX
f - e is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
- e is Relation-like NAT -defined Function-like V14( NAT ) V38() set
- 1 is non empty V33() real ext-real set
(- 1) (#) e is Relation-like NAT -defined Function-like V14( NAT ) V38() set
f + (- e) is Relation-like NAT -defined Function-like V14( NAT ) V38() set
|.(f - e).| is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
lim |.(f - e).| is V33() real ext-real Element of REAL
lim (f - e) is V33() Element of COMPLEX
|.(lim (f - e)).| is V33() real ext-real Element of REAL
lim e is V33() Element of COMPLEX
(lim f) - (lim e) is V33() Element of COMPLEX
|.((lim f) - (lim e)).| is V33() real ext-real Element of REAL
u is epsilon-transitive epsilon-connected ordinal natural V33() real ext-real V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
tseq . u is V33() real ext-real Element of REAL
f . u is V33() Element of COMPLEX
(f . u) - vseq is V33() set
|.((f . u) - vseq).| is V33() real ext-real Element of REAL
e . u is V33() Element of COMPLEX
(f . u) - (e . u) is V33() Element of COMPLEX
|.((f . u) - (e . u)).| is V33() real ext-real Element of REAL
- (e . u) is V33() Element of COMPLEX
(f . u) + (- (e . u)) is V33() Element of COMPLEX
|.((f . u) + (- (e . u))).| is V33() real ext-real Element of REAL
- e is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
(- e) . u is V33() Element of COMPLEX
(f . u) + ((- e) . u) is V33() Element of COMPLEX
|.((f . u) + ((- e) . u)).| is V33() real ext-real Element of REAL
(f - e) . u is V33() Element of COMPLEX
|.((f - e) . u).| is V33() real ext-real Element of REAL
|.(f - e).| . u is V33() real ext-real Element of REAL
u is set
tseq . u is V33() real ext-real Element of REAL
|.(f - e).| . u is V33() real ext-real Element of REAL
m is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) V18( NAT , COMPLEX ) V38() bounded convergent Element of bool [:NAT,COMPLEX:]
|.m.| is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) V38() V39() V40() bounded convergent bounded_above bounded_below Element of bool [:NAT,REAL:]
seq_id CZeroseq is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
vseq is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
f is epsilon-transitive epsilon-connected ordinal natural V33() real ext-real V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
vseq . f is V33() Element of COMPLEX
f is Element of the carrier of Linear_Space_of_ComplexSequences
tseq is Element of the carrier of Linear_Space_of_ComplexSequences
f + tseq is Element of the carrier of Linear_Space_of_ComplexSequences
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 empty 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 empty set
[:[: the carrier of Linear_Space_of_ComplexSequences, the carrier of Linear_Space_of_ComplexSequences:], the carrier of Linear_Space_of_ComplexSequences:] is non empty 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 empty set
the addF of Linear_Space_of_ComplexSequences . (f,tseq) is Element of the carrier of Linear_Space_of_ComplexSequences
[f,tseq] is set
the addF of Linear_Space_of_ComplexSequences . [f,tseq] is set
seq_id (f + tseq) is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
|.(seq_id (f + tseq)).| is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
seq_id tseq is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
|.(seq_id tseq).| is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
seq_id f is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
|.(seq_id f).| is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
u is epsilon-transitive epsilon-connected ordinal natural V33() real ext-real V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
|.(seq_id (f + tseq)).| . u is V33() real ext-real Element of REAL
(seq_id (f + tseq)) . u is V33() Element of COMPLEX
|.((seq_id (f + tseq)) . u).| is V33() real ext-real Element of REAL
|.(seq_id f).| + |.(seq_id tseq).| is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
u is epsilon-transitive epsilon-connected ordinal natural V33() real ext-real V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
|.(seq_id (f + tseq)).| . u is V33() real ext-real Element of REAL
(|.(seq_id f).| + |.(seq_id tseq).|) . u is V33() real ext-real Element of REAL
(seq_id f) . u is V33() Element of COMPLEX
|.((seq_id f) . u).| is V33() real ext-real Element of REAL
(seq_id tseq) . u is V33() Element of COMPLEX
|.((seq_id tseq) . u).| is V33() real ext-real Element of REAL
|.((seq_id f) . u).| + |.((seq_id tseq) . u).| is V33() real ext-real Element of REAL
|.(seq_id f).| . u is V33() real ext-real Element of REAL
(|.(seq_id f).| . u) + |.((seq_id tseq) . u).| is V33() real ext-real Element of REAL
|.(seq_id tseq).| . u is V33() real ext-real Element of REAL
(|.(seq_id f).| . u) + (|.(seq_id tseq).| . u) is V33() real ext-real Element of REAL
(seq_id (f + tseq)) . u is V33() Element of COMPLEX
|.((seq_id (f + tseq)) . u).| is V33() real ext-real Element of REAL
(seq_id f) + (seq_id tseq) is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
seq_id ((seq_id f) + (seq_id tseq)) is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
(seq_id ((seq_id f) + (seq_id tseq))) . u is V33() Element of COMPLEX
|.((seq_id ((seq_id f) + (seq_id tseq))) . u).| is V33() real ext-real Element of REAL
((seq_id f) + (seq_id tseq)) . u is V33() Element of COMPLEX
|.(((seq_id f) + (seq_id tseq)) . u).| is V33() real ext-real Element of REAL
((seq_id f) . u) + ((seq_id tseq) . u) is V33() Element of COMPLEX
|.(((seq_id f) . u) + ((seq_id tseq) . u)).| is V33() real ext-real Element of REAL
f is V33() set
tseq is Element of the carrier of Linear_Space_of_ComplexSequences
f * tseq is Element of the carrier of Linear_Space_of_ComplexSequences
seq_id (f * tseq) is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
seq_id tseq is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
|.(seq_id tseq).| is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
|.f.| is V33() real ext-real Element of REAL
|.f.| (#) |.(seq_id tseq).| is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
|.(seq_id (f * tseq)).| is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
m is epsilon-transitive epsilon-connected ordinal natural V33() real ext-real V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
|.(seq_id (f * tseq)).| . m is V33() real ext-real Element of REAL
(seq_id (f * tseq)) . m is V33() Element of COMPLEX
|.((seq_id (f * tseq)) . m).| is V33() real ext-real Element of REAL
m is epsilon-transitive epsilon-connected ordinal natural V33() real ext-real V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
|.(seq_id (f * tseq)).| . m is V33() real ext-real Element of REAL
(|.f.| (#) |.(seq_id tseq).|) . m is V33() real ext-real Element of REAL
(seq_id (f * tseq)) . m is V33() Element of COMPLEX
|.((seq_id (f * tseq)) . m).| is V33() real ext-real Element of REAL
f (#) (seq_id tseq) is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
seq_id (f (#) (seq_id tseq)) is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
(seq_id (f (#) (seq_id tseq))) . m is V33() Element of COMPLEX
|.((seq_id (f (#) (seq_id tseq))) . m).| is V33() real ext-real Element of REAL
(f (#) (seq_id tseq)) . m is V33() Element of COMPLEX
|.((f (#) (seq_id tseq)) . m).| is V33() real ext-real Element of REAL
|.(f (#) (seq_id tseq)).| is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
|.(f (#) (seq_id tseq)).| . m is V33() real ext-real Element of REAL
Zero_ ((),Linear_Space_of_ComplexSequences) is Element of ()
Add_ ((),Linear_Space_of_ComplexSequences) is Relation-like [:(),():] -defined () -valued Function-like non empty V14([:(),():]) V18([:(),():],()) Element of bool [:[:(),():],():]
[:(),():] is non empty set
[:[:(),():],():] is non empty set
bool [:[:(),():],():] is non empty set
Mult_ ((),Linear_Space_of_ComplexSequences) is Relation-like [:COMPLEX,():] -defined () -valued Function-like non empty V14([:COMPLEX,():]) V18([:COMPLEX,():],()) Element of bool [:[:COMPLEX,():],():]
[:COMPLEX,():] is non empty set
[:[:COMPLEX,():],():] is non empty set
bool [:[:COMPLEX,():],():] is non empty set
CLSStruct(# (),(Zero_ ((),Linear_Space_of_ComplexSequences)),(Add_ ((),Linear_Space_of_ComplexSequences)),(Mult_ ((),Linear_Space_of_ComplexSequences)) #) is non empty strict CLSStruct
[:(),REAL:] is non empty V38() V39() V40() set
bool [:(),REAL:] is non empty set
vseq is set
seq_id vseq is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
|.(seq_id vseq).| is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
Sum |.(seq_id vseq).| is V33() real ext-real Element of REAL
vseq is Relation-like () -defined REAL -valued Function-like non empty V14(()) V18((), REAL ) V38() V39() V40() Element of bool [:(),REAL:]
vseq is Relation-like () -defined REAL -valued Function-like non empty V14(()) V18((), REAL ) V38() V39() V40() Element of bool [:(),REAL:]
f is Relation-like () -defined REAL -valued Function-like non empty V14(()) V18((), REAL ) V38() V39() V40() Element of bool [:(),REAL:]
tseq is set
vseq . tseq is V33() real ext-real Element of REAL
f . tseq is V33() real ext-real Element of REAL
seq_id tseq is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
|.(seq_id tseq).| is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
Sum |.(seq_id tseq).| is V33() real ext-real Element of REAL
dom vseq is set
dom f is set
() is Relation-like () -defined REAL -valued Function-like non empty V14(()) V18((), REAL ) V38() V39() V40() Element of bool [:(),REAL:]
vseq is non empty set
[:vseq,vseq:] is non empty set
[:[:vseq,vseq:],vseq:] is non empty set
bool [:[:vseq,vseq:],vseq:] is non empty set
[:COMPLEX,vseq:] is non empty set
[:[:COMPLEX,vseq:],vseq:] is non empty set
bool [:[:COMPLEX,vseq:],vseq:] is non empty set
[:vseq,REAL:] is non empty V38() V39() V40() set
bool [:vseq,REAL:] is non empty set
f is Element of vseq
tseq is Relation-like [:vseq,vseq:] -defined vseq -valued Function-like non empty V14([:vseq,vseq:]) V18([:vseq,vseq:],vseq) Element of bool [:[:vseq,vseq:],vseq:]
tv is Relation-like [:COMPLEX,vseq:] -defined vseq -valued Function-like non empty V14([:COMPLEX,vseq:]) V18([:COMPLEX,vseq:],vseq) Element of bool [:[:COMPLEX,vseq:],vseq:]
e is Relation-like vseq -defined REAL -valued Function-like non empty V14(vseq) V18(vseq, REAL ) V38() V39() V40() Element of bool [:vseq,REAL:]
CNORMSTR(# vseq,f,tseq,tv,e #) is strict CNORMSTR
vseq is CNORMSTR
the carrier of vseq is set
the ZeroF of vseq is Element of the carrier of vseq
the addF of vseq is Relation-like [: the carrier of vseq, the carrier of vseq:] -defined the carrier of vseq -valued Function-like V18([: the carrier of vseq, the carrier of vseq:], the carrier of vseq) Element of bool [:[: the carrier of vseq, the carrier of vseq:], the carrier of vseq:]
[: the carrier of vseq, the carrier of vseq:] is set
[:[: the carrier of vseq, the carrier of vseq:], the carrier of vseq:] is set
bool [:[: the carrier of vseq, the carrier of vseq:], the carrier of vseq:] is non empty set
the Mult of vseq is Relation-like [:COMPLEX, the carrier of vseq:] -defined the carrier of vseq -valued Function-like V18([:COMPLEX, the carrier of vseq:], the carrier of vseq) Element of bool [:[:COMPLEX, the carrier of vseq:], the carrier of vseq:]
[:COMPLEX, the carrier of vseq:] is set
[:[:COMPLEX, the carrier of vseq:], the carrier of vseq:] is set
bool [:[:COMPLEX, the carrier of vseq:], the carrier of vseq:] is non empty set
CLSStruct(# the carrier of vseq, the ZeroF of vseq, the addF of vseq, the Mult of vseq #) is strict CLSStruct
vseq is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
|.vseq.| is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
Sum |.vseq.| is V33() real ext-real Element of REAL
f is epsilon-transitive epsilon-connected ordinal natural V33() real ext-real V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
|.vseq.| . f is V33() real ext-real Element of REAL
vseq . f is V33() Element of COMPLEX
Partial_Sums |.vseq.| is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
f is epsilon-transitive epsilon-connected ordinal natural V33() real ext-real V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
(Partial_Sums |.vseq.|) . f is V33() real ext-real Element of REAL
tseq is epsilon-transitive epsilon-connected ordinal natural V33() real ext-real V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
|.vseq.| . tseq is V33() real ext-real Element of REAL
(Partial_Sums |.vseq.|) . tseq is V33() real ext-real Element of REAL
tseq + 1 is epsilon-transitive epsilon-connected ordinal natural V33() real ext-real V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
|.vseq.| . (tseq + 1) is V33() real ext-real Element of REAL
(Partial_Sums |.vseq.|) . (tseq + 1) is V33() real ext-real Element of REAL
0 + (|.vseq.| . (tseq + 1)) is V33() real ext-real Element of REAL
(|.vseq.| . tseq) + (|.vseq.| . (tseq + 1)) is V33() real ext-real Element of REAL
|.vseq.| . 0 is V33() real ext-real Element of REAL
(Partial_Sums |.vseq.|) . 0 is V33() real ext-real Element of REAL
|.vseq.| . f is V33() real ext-real Element of REAL
f is V33() real ext-real set
tseq is epsilon-transitive epsilon-connected ordinal natural V33() real ext-real V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
(Partial_Sums |.vseq.|) . tseq is V33() real ext-real Element of REAL
((Partial_Sums |.vseq.|) . tseq) - 0 is V33() real ext-real Element of REAL
abs (((Partial_Sums |.vseq.|) . tseq) - 0) is V33() real ext-real Element of REAL
0 - 0 is V33() real ext-real Element of REAL
abs (0 - 0) is V33() real ext-real Element of REAL
lim (Partial_Sums |.vseq.|) is V33() real ext-real Element of REAL
vseq is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
|.vseq.| is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
Sum |.vseq.| is V33() real ext-real Element of REAL
tseq is epsilon-transitive epsilon-connected ordinal natural V33() real ext-real V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
|.vseq.| . tseq is V33() real ext-real Element of REAL
vseq . tseq is V33() Element of COMPLEX
|.(vseq . tseq).| is V33() real ext-real Element of REAL
f is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
tseq is epsilon-transitive epsilon-connected ordinal natural V33() real ext-real V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
vseq . tseq is V33() Element of COMPLEX
|.vseq.| . tseq is V33() real ext-real Element of REAL
|.(vseq . tseq).| is V33() real ext-real Element of REAL
tseq is epsilon-transitive epsilon-connected ordinal natural V33() real ext-real V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
vseq . tseq is V33() Element of COMPLEX
CNORMSTR(# (),(Zero_ ((),Linear_Space_of_ComplexSequences)),(Add_ ((),Linear_Space_of_ComplexSequences)),(Mult_ ((),Linear_Space_of_ComplexSequences)),() #) is non empty strict CNORMSTR
() is non empty CNORMSTR
the carrier of () is non empty set
0. () is V87(()) Element of the carrier of ()
the ZeroF of () is Element of the carrier of ()
f is set
seq_id f is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
f is Element of the carrier of ()
tseq is Element of the carrier of ()
f + tseq is Element of the carrier of ()
the addF of () is Relation-like [: the carrier of (), the carrier of ():] -defined the carrier of () -valued Function-like non empty V14([: the carrier of (), the carrier of ():]) V18([: the carrier of (), the carrier of ():], the carrier of ()) Element of bool [:[: the carrier of (), the carrier of ():], the carrier of ():]
[: the carrier of (), the carrier of ():] is non empty set
[:[: the carrier of (), the carrier of ():], the carrier of ():] is non empty set
bool [:[: the carrier of (), the carrier of ():], the carrier of ():] is non empty set
the addF of () . (f,tseq) is Element of the carrier of ()
[f,tseq] is set
the addF of () . [f,tseq] is set
seq_id f is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
seq_id tseq is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
(seq_id f) + (seq_id tseq) is Relation-like NAT -defined COMPLEX -valued Function-like non empty 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 empty 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 empty set
[:[: the carrier of Linear_Space_of_ComplexSequences, the carrier of Linear_Space_of_ComplexSequences:], the carrier of Linear_Space_of_ComplexSequences:] is non empty 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 empty set
dom the addF of Linear_Space_of_ComplexSequences is Relation-like set
the addF of Linear_Space_of_ComplexSequences || () is Relation-like Function-like set
the addF of Linear_Space_of_ComplexSequences | [:(),():] is Relation-like set
dom ( the addF of Linear_Space_of_ComplexSequences || ()) is set
[f,tseq] is Element of [: the carrier of (), the carrier of ():]
( the addF of Linear_Space_of_ComplexSequences || ()) . [f,tseq] 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
[tv,e] is set
the addF of Linear_Space_of_ComplexSequences . [tv,e] is set
f is V33() set
tseq is Element of the carrier of ()
f * tseq is Element of the carrier of ()
seq_id tseq is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
f (#) (seq_id tseq) is Relation-like NAT -defined COMPLEX -valued Function-like non empty 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 empty 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 empty set
[:[:COMPLEX, the carrier of Linear_Space_of_ComplexSequences:], the carrier of Linear_Space_of_ComplexSequences:] is non empty set
bool [:[:COMPLEX, the carrier of Linear_Space_of_ComplexSequences:], the carrier of Linear_Space_of_ComplexSequences:] is non empty set
dom the Mult of Linear_Space_of_ComplexSequences is Relation-like set
the Mult of Linear_Space_of_ComplexSequences | [:COMPLEX,():] 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,():]) is Relation-like set
u is V33() Element of COMPLEX
u * tseq is Element of the carrier of ()
[:COMPLEX, the carrier of ():] is non empty set
the Mult of () is Relation-like [:COMPLEX, the carrier of ():] -defined the carrier of () -valued Function-like non empty V14([:COMPLEX, the carrier of ():]) V18([:COMPLEX, the carrier of ():], the carrier of ()) Element of bool [:[:COMPLEX, the carrier of ():], the carrier of ():]
[:[:COMPLEX, the carrier of ():], the carrier of ():] is non empty set
bool [:[:COMPLEX, the carrier of ():], the carrier of ():] is non empty set
[u,tseq] is Element of [:COMPLEX, the carrier of ():]
the Mult of () . [u,tseq] is Element of the carrier of ()
( the Mult of Linear_Space_of_ComplexSequences | [:COMPLEX,():]) . [u,tseq] is set
the Mult of Linear_Space_of_ComplexSequences . [u,tseq] is set
tv is Element of the carrier of Linear_Space_of_ComplexSequences
u * tv is Element of the carrier of Linear_Space_of_ComplexSequences
f is Element of the carrier of ()
seq_id f is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
f is Element of the carrier of ()
- f is Element of the carrier of ()
seq_id f is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
- (seq_id f) is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
- 1 is non empty V33() real ext-real set
(- 1) (#) (seq_id f) is Relation-like NAT -defined Function-like V14( NAT ) V38() set
seq_id (- f) is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
(- 1r) * f is Element of the carrier of ()
(- 1r) (#) (seq_id f) is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
f is Element of the carrier of ()
tseq is Element of the carrier of ()
f - tseq is Element of the carrier of ()
- tseq is Element of the carrier of ()
f + (- tseq) is Element of the carrier of ()
the addF of () is Relation-like [: the carrier of (), the carrier of ():] -defined the carrier of () -valued Function-like non empty V14([: the carrier of (), the carrier of ():]) V18([: the carrier of (), the carrier of ():], the carrier of ()) Element of bool [:[: the carrier of (), the carrier of ():], the carrier of ():]
[: the carrier of (), the carrier of ():] is non empty set
[:[: the carrier of (), the carrier of ():], the carrier of ():] is non empty set
bool [:[: the carrier of (), the carrier of ():], the carrier of ():] is non empty set
the addF of () . (f,(- tseq)) is Element of the carrier of ()
[f,(- tseq)] is set
the addF of () . [f,(- tseq)] is set
seq_id f is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
seq_id tseq is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
(seq_id f) - (seq_id tseq) is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
- (seq_id tseq) is Relation-like NAT -defined Function-like V14( NAT ) V38() set
- 1 is non empty V33() real ext-real set
(- 1) (#) (seq_id tseq) is Relation-like NAT -defined Function-like V14( NAT ) V38() set
(seq_id f) + (- (seq_id tseq)) is Relation-like NAT -defined Function-like V14( NAT ) V38() set
seq_id (- tseq) is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
(seq_id f) + (seq_id (- tseq)) is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
f is Element of the carrier of ()
||.f.|| is V33() real ext-real Element of REAL
the normF of () is Relation-like the carrier of () -defined REAL -valued Function-like non empty V14( the carrier of ()) V18( the carrier of (), REAL ) V38() V39() V40() Element of bool [: the carrier of (),REAL:]
[: the carrier of (),REAL:] is non empty V38() V39() V40() set
bool [: the carrier of (),REAL:] is non empty set
the normF of () . f is V33() real ext-real Element of REAL
seq_id f is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
|.(seq_id f).| is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
Sum |.(seq_id f).| is V33() real ext-real Element of REAL
0. Linear_Space_of_ComplexSequences is V87( Linear_Space_of_ComplexSequences ) 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
f is set
seq_id f is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
tseq is set
seq_id tseq is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
tv is Element of the carrier of ()
seq_id tv is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
e is Element of the carrier of ()
m is Element of the carrier of ()
e + m is Element of the carrier of ()
the addF of () is Relation-like [: the carrier of (), the carrier of ():] -defined the carrier of () -valued Function-like non empty V14([: the carrier of (), the carrier of ():]) V18([: the carrier of (), the carrier of ():], the carrier of ()) Element of bool [:[: the carrier of (), the carrier of ():], the carrier of ():]
[: the carrier of (), the carrier of ():] is non empty set
[:[: the carrier of (), the carrier of ():], the carrier of ():] is non empty set
bool [:[: the carrier of (), the carrier of ():], the carrier of ():] is non empty set
the addF of () . (e,m) is Element of the carrier of ()
[e,m] is set
the addF of () . [e,m] is set
seq_id e is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
seq_id m is Relation-like NAT -defined COMPLEX -valued Function-like non empty 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 empty V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
n is Element of the carrier of ()
u is V33() set
u * n is Element of the carrier of ()
seq_id n is Relation-like NAT -defined COMPLEX -valued Function-like non empty 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 empty V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
v is Element of the carrier of ()
- v is Element of the carrier of ()
seq_id v is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
- (seq_id v) is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
- 1 is non empty V33() real ext-real set
(- 1) (#) (seq_id v) is Relation-like NAT -defined Function-like V14( NAT ) V38() set
m is Element of the carrier of ()
- m is Element of the carrier of ()
seq_id (- m) is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
seq_id m is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
- (seq_id m) is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
(- 1) (#) (seq_id m) is Relation-like NAT -defined Function-like V14( NAT ) V38() set
rseq is Element of the carrier of ()
m is Element of the carrier of ()
rseq - m is Element of the carrier of ()
- m is Element of the carrier of ()
rseq + (- m) is Element of the carrier of ()
the addF of () . (rseq,(- m)) is Element of the carrier of ()
[rseq,(- m)] is set
the addF of () . [rseq,(- m)] is set
seq_id rseq is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
seq_id m is Relation-like NAT -defined COMPLEX -valued Function-like non empty 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 empty 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 ()
seq_id c₁₃ is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
c₁₄ is Element of the carrier of ()
||.c₁₄.|| is V33() real ext-real Element of REAL
the normF of () is Relation-like the carrier of () -defined REAL -valued Function-like non empty V14( the carrier of ()) V18( the carrier of (), REAL ) V38() V39() V40() Element of bool [: the carrier of (),REAL:]
[: the carrier of (),REAL:] is non empty V38() V39() V40() set
bool [: the carrier of (),REAL:] is non empty set
the normF of () . c₁₄ is V33() real ext-real Element of REAL
seq_id c₁₄ is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
|.(seq_id c₁₄).| is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
Sum |.(seq_id c₁₄).| is V33() real ext-real Element of REAL
vseq is Element of the carrier of ()
||.vseq.|| is V33() real ext-real Element of REAL
the normF of () is Relation-like the carrier of () -defined REAL -valued Function-like non empty V14( the carrier of ()) V18( the carrier of (), REAL ) V38() V39() V40() Element of bool [: the carrier of (),REAL:]
[: the carrier of (),REAL:] is non empty V38() V39() V40() set
bool [: the carrier of (),REAL:] is non empty set
the normF of () . vseq is V33() real ext-real Element of REAL
f is Element of the carrier of ()
vseq + f is Element of the carrier of ()
the addF of () is Relation-like [: the carrier of (), the carrier of ():] -defined the carrier of () -valued Function-like non empty V14([: the carrier of (), the carrier of ():]) V18([: the carrier of (), the carrier of ():], the carrier of ()) Element of bool [:[: the carrier of (), the carrier of ():], the carrier of ():]
[: the carrier of (), the carrier of ():] is non empty set
[:[: the carrier of (), the carrier of ():], the carrier of ():] is non empty set
bool [:[: the carrier of (), the carrier of ():], the carrier of ():] is non empty set
the addF of () . (vseq,f) is Element of the carrier of ()
[vseq,f] is set
the addF of () . [vseq,f] is set
||.(vseq + f).|| is V33() real ext-real Element of REAL
the normF of () . (vseq + f) is V33() real ext-real Element of REAL
||.f.|| is V33() real ext-real Element of REAL
the normF of () . f is V33() real ext-real Element of REAL
||.vseq.|| + ||.f.|| is V33() real ext-real Element of REAL
tseq is V33() set
tseq * vseq is Element of the carrier of ()
||.(tseq * vseq).|| is V33() real ext-real Element of REAL
the normF of () . (tseq * vseq) is V33() real ext-real Element of REAL
|.tseq.| is V33() real ext-real Element of REAL
|.tseq.| * ||.vseq.|| is V33() real ext-real Element of REAL
seq_id vseq is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
|.(seq_id vseq).| is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
tv is epsilon-transitive epsilon-connected ordinal natural V33() real ext-real V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
|.(seq_id vseq).| . tv is V33() real ext-real Element of REAL
(seq_id vseq) . tv is V33() Element of COMPLEX
|.((seq_id vseq) . tv).| is V33() real ext-real Element of REAL
seq_id (vseq + f) is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
|.(seq_id (vseq + f)).| is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
tv is epsilon-transitive epsilon-connected ordinal natural V33() real ext-real V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
|.(seq_id (vseq + f)).| . tv is V33() real ext-real Element of REAL
(seq_id (vseq + f)) . tv is V33() Element of COMPLEX
|.((seq_id (vseq + f)) . tv).| is V33() real ext-real Element of REAL
seq_id f is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
tv is epsilon-transitive epsilon-connected ordinal natural V33() real ext-real V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
|.(seq_id (vseq + f)).| . tv is V33() real ext-real Element of REAL
(seq_id vseq) . tv is V33() Element of COMPLEX
(seq_id f) . tv is V33() Element of COMPLEX
((seq_id vseq) . tv) + ((seq_id f) . tv) is V33() Element of COMPLEX
|.(((seq_id vseq) . tv) + ((seq_id f) . tv)).| is V33() real ext-real Element of REAL
(seq_id vseq) + (seq_id f) is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
seq_id ((seq_id vseq) + (seq_id f)) is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
|.(seq_id ((seq_id vseq) + (seq_id f))).| is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
|.(seq_id ((seq_id vseq) + (seq_id f))).| . tv is V33() real ext-real Element of REAL
|.((seq_id vseq) + (seq_id f)).| is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
|.((seq_id vseq) + (seq_id f)).| . tv is V33() real ext-real Element of REAL
((seq_id vseq) + (seq_id f)) . tv is V33() Element of COMPLEX
|.(((seq_id vseq) + (seq_id f)) . tv).| is V33() real ext-real Element of REAL
|.(seq_id f).| is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
tv is epsilon-transitive epsilon-connected ordinal natural V33() real ext-real V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
|.(seq_id (vseq + f)).| . tv is V33() real ext-real Element of REAL
|.(seq_id vseq).| . tv is V33() real ext-real Element of REAL
|.(seq_id f).| . tv is V33() real ext-real Element of REAL
(|.(seq_id vseq).| . tv) + (|.(seq_id f).| . tv) is V33() real ext-real Element of REAL
(seq_id vseq) . tv is V33() Element of COMPLEX
(seq_id f) . tv is V33() Element of COMPLEX
((seq_id vseq) . tv) + ((seq_id f) . tv) is V33() Element of COMPLEX
|.(((seq_id vseq) . tv) + ((seq_id f) . tv)).| is V33() real ext-real Element of REAL
|.((seq_id vseq) . tv).| is V33() real ext-real Element of REAL
|.((seq_id f) . tv).| is V33() real ext-real Element of REAL
|.((seq_id vseq) . tv).| + |.((seq_id f) . tv).| is V33() real ext-real Element of REAL
(|.(seq_id vseq).| . tv) + |.((seq_id f) . tv).| is V33() real ext-real Element of REAL
|.(seq_id vseq).| + |.(seq_id f).| is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
tv is epsilon-transitive epsilon-connected ordinal natural V33() real ext-real V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
|.(seq_id (vseq + f)).| . tv is V33() real ext-real Element of REAL
(|.(seq_id vseq).| + |.(seq_id f).|) . tv is V33() real ext-real Element of REAL
|.(seq_id vseq).| . tv is V33() real ext-real Element of REAL
|.(seq_id f).| . tv is V33() real ext-real Element of REAL
(|.(seq_id vseq).| . tv) + (|.(seq_id f).| . tv) is V33() real ext-real Element of REAL
Sum |.(seq_id (vseq + f)).| is V33() real ext-real Element of REAL
Sum (|.(seq_id vseq).| + |.(seq_id f).|) is V33() real ext-real Element of REAL
tv is epsilon-transitive epsilon-connected ordinal natural V33() real ext-real V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
(seq_id vseq) . tv is V33() Element of COMPLEX
the normF of () . vseq is V33() real ext-real Element of REAL
Sum |.(seq_id vseq).| is V33() real ext-real Element of REAL
tv is epsilon-transitive epsilon-connected ordinal natural V33() real ext-real V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
(seq_id vseq) . tv is V33() Element of COMPLEX
Sum |.(seq_id f).| is V33() real ext-real Element of REAL
tseq (#) (seq_id vseq) is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
|.(tseq (#) (seq_id vseq)).| is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
tv is epsilon-transitive epsilon-connected ordinal natural V33() real ext-real V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
|.(tseq (#) (seq_id vseq)).| . tv is V33() real ext-real Element of REAL
|.(seq_id vseq).| . tv is V33() real ext-real Element of REAL
|.tseq.| * (|.(seq_id vseq).| . tv) is V33() real ext-real Element of REAL
e is V33() Element of COMPLEX
e (#) (seq_id vseq) is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
|.(e (#) (seq_id vseq)).| is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
|.(e (#) (seq_id vseq)).| . tv is V33() real ext-real Element of REAL
(e (#) (seq_id vseq)) . tv is V33() Element of COMPLEX
|.((e (#) (seq_id vseq)) . tv).| is V33() real ext-real Element of REAL
(seq_id vseq) . tv is V33() Element of COMPLEX
e * ((seq_id vseq) . tv) is V33() Element of COMPLEX
|.(e * ((seq_id vseq) . tv)).| is V33() real ext-real Element of REAL
|.e.| is V33() real ext-real Element of REAL
|.((seq_id vseq) . tv).| is V33() real ext-real Element of REAL
|.e.| * |.((seq_id vseq) . tv).| is V33() real ext-real Element of REAL
|.e.| * (|.(seq_id vseq).| . tv) is V33() real ext-real Element of REAL
seq_id (tseq * vseq) is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
|.(seq_id (tseq * vseq)).| is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
Sum |.(seq_id (tseq * vseq)).| is V33() real ext-real Element of REAL
seq_id (tseq (#) (seq_id vseq)) is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
|.(seq_id (tseq (#) (seq_id vseq))).| is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
Sum |.(seq_id (tseq (#) (seq_id vseq))).| is V33() real ext-real Element of REAL
Sum |.(tseq (#) (seq_id vseq)).| is V33() real ext-real Element of REAL
|.tseq.| (#) |.(seq_id vseq).| is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
Sum (|.tseq.| (#) |.(seq_id vseq).|) is V33() real ext-real Element of REAL
|.tseq.| * (Sum |.(seq_id vseq).|) is V33() real ext-real Element of REAL
||.(0. ()).|| is V33() real ext-real Element of REAL
the normF of () is Relation-like the carrier of () -defined REAL -valued Function-like non empty V14( the carrier of ()) V18( the carrier of (), REAL ) V38() V39() V40() Element of bool [: the carrier of (),REAL:]
[: the carrier of (),REAL:] is non empty V38() V39() V40() set
bool [: the carrier of (),REAL:] is non empty set
the normF of () . (0. ()) is V33() real ext-real Element of REAL
vseq is V33() set
f is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
lim f is V33() Element of COMPLEX
(lim f) - vseq is V33() set
|.((lim f) - vseq).| is V33() real ext-real Element of REAL
tseq is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
lim tseq is V33() real ext-real Element of REAL
|.((lim f) - vseq).| + (lim tseq) is V33() real ext-real Element of REAL
tv is V33() Element of COMPLEX
NAT --> tv is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
e is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
m is epsilon-transitive epsilon-connected ordinal natural V33() real ext-real V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
e . m is V33() Element of COMPLEX
lim e is V33() Element of COMPLEX
e . 0 is V33() Element of COMPLEX
f - e is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
- e is Relation-like NAT -defined Function-like V14( NAT ) V38() set
- 1 is non empty V33() real ext-real set
(- 1) (#) e is Relation-like NAT -defined Function-like V14( NAT ) V38() set
f + (- e) is Relation-like NAT -defined Function-like V14( NAT ) V38() set
|.(f - e).| is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
lim |.(f - e).| is V33() real ext-real Element of REAL
lim (f - e) is V33() Element of COMPLEX
|.(lim (f - e)).| is V33() real ext-real Element of REAL
(lim f) - (e . 0) is V33() Element of COMPLEX
|.((lim f) - (e . 0)).| is V33() real ext-real Element of REAL
m is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
lim m is V33() real ext-real Element of REAL
u is epsilon-transitive epsilon-connected ordinal natural V33() real ext-real V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
m . u is V33() real ext-real Element of REAL
f . u is V33() Element of COMPLEX
(f . u) - vseq is V33() set
|.((f . u) - vseq).| is V33() real ext-real Element of REAL
tseq . u is V33() real ext-real Element of REAL
|.((f . u) - vseq).| + (tseq . u) is V33() real ext-real Element of REAL
e . u is V33() Element of COMPLEX
(f . u) - (e . u) is V33() Element of COMPLEX
|.((f . u) - (e . u)).| is V33() real ext-real Element of REAL
|.((f . u) - (e . u)).| + (tseq . u) is V33() real ext-real Element of REAL
- (e . u) is V33() Element of COMPLEX
(f . u) + (- (e . u)) is V33() Element of COMPLEX
|.((f . u) + (- (e . u))).| is V33() real ext-real Element of REAL
|.((f . u) + (- (e . u))).| + (tseq . u) is V33() real ext-real Element of REAL
- e is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
(- e) . u is V33() Element of COMPLEX
(f . u) + ((- e) . u) is V33() Element of COMPLEX
|.((f . u) + ((- e) . u)).| is V33() real ext-real Element of REAL
|.((f . u) + ((- e) . u)).| + (tseq . u) is V33() real ext-real Element of REAL
(f - e) . u is V33() Element of COMPLEX
|.((f - e) . u).| is V33() real ext-real Element of REAL
|.((f - e) . u).| + (tseq . u) is V33() real ext-real Element of REAL
|.(f - e).| . u is V33() real ext-real Element of REAL
(|.(f - e).| . u) + (tseq . u) is V33() real ext-real Element of REAL
|.(f - e).| + tseq is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
(|.(f - e).| + tseq) . u is V33() real ext-real Element of REAL
u is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) V18( NAT , COMPLEX ) V38() bounded convergent Element of bool [:NAT,COMPLEX:]
|.u.| is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) V38() V39() V40() bounded convergent bounded_above bounded_below Element of bool [:NAT,REAL:]
vseq is non empty CNORMSTR
the carrier of vseq is non empty set
f is Element of the carrier of vseq
tseq is Element of the carrier of vseq
f - tseq is Element of the carrier of vseq
- tseq is Element of the carrier of vseq
f + (- tseq) is Element of the carrier of vseq
the addF of vseq is Relation-like [: the carrier of vseq, the carrier of vseq:] -defined the carrier of vseq -valued Function-like non empty V14([: the carrier of vseq, the carrier of vseq:]) V18([: the carrier of vseq, the carrier of vseq:], the carrier of vseq) Element of bool [:[: the carrier of vseq, the carrier of vseq:], the carrier of vseq:]
[: the carrier of vseq, the carrier of vseq:] is non empty set
[:[: the carrier of vseq, the carrier of vseq:], the carrier of vseq:] is non empty set
bool [:[: the carrier of vseq, the carrier of vseq:], the carrier of vseq:] is non empty set
the addF of vseq . (f,(- tseq)) is Element of the carrier of vseq
[f,(- tseq)] is set
the addF of vseq . [f,(- tseq)] is set
||.(f - tseq).|| is V33() real ext-real Element of REAL
the normF of vseq is Relation-like the carrier of vseq -defined REAL -valued Function-like non empty V14( the carrier of vseq) V18( the carrier of vseq, REAL ) V38() V39() V40() Element of bool [: the carrier of vseq,REAL:]
[: the carrier of vseq,REAL:] is non empty V38() V39() V40() set
bool [: the carrier of vseq,REAL:] is non empty set
the normF of vseq . (f - tseq) is V33() real ext-real Element of REAL
vseq is non empty CNORMSTR
the carrier of vseq is non empty set
[:NAT, the carrier of vseq:] is non empty set
bool [:NAT, the carrier of vseq:] is non empty set
vseq is non empty CNORMSTR
the carrier of vseq is non empty set
[:NAT, the carrier of vseq:] is non empty set
bool [:NAT, the carrier of vseq:] is non empty set
vseq is non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like CNORMSTR
the carrier of vseq is non empty set
[:NAT, the carrier of vseq:] is non empty set
bool [:NAT, the carrier of vseq:] is non empty set
f is Relation-like NAT -defined the carrier of vseq -valued Function-like non empty V14( NAT ) V18( NAT , the carrier of vseq) Element of bool [:NAT, the carrier of vseq:]
tseq is V33() real ext-real Element of REAL
tv is epsilon-transitive epsilon-connected ordinal natural V33() real ext-real V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
e is epsilon-transitive epsilon-connected ordinal natural V33() real ext-real V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V33() real ext-real V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
f . e is Element of the carrier of vseq
f . m is Element of the carrier of vseq
(f . e) - (f . m) is Element of the carrier of vseq
- (f . m) is Element of the carrier of vseq
(f . e) + (- (f . m)) is Element of the carrier of vseq
the addF of vseq is Relation-like [: the carrier of vseq, the carrier of vseq:] -defined the carrier of vseq -valued Function-like non empty V14([: the carrier of vseq, the carrier of vseq:]) V18([: the carrier of vseq, the carrier of vseq:], the carrier of vseq) Element of bool [:[: the carrier of vseq, the carrier of vseq:], the carrier of vseq:]
[: the carrier of vseq, the carrier of vseq:] is non empty set
[:[: the carrier of vseq, the carrier of vseq:], the carrier of vseq:] is non empty set
bool [:[: the carrier of vseq, the carrier of vseq:], the carrier of vseq:] is non empty set
the addF of vseq . ((f . e),(- (f . m))) is Element of the carrier of vseq
[(f . e),(- (f . m))] is set
the addF of vseq . [(f . e),(- (f . m))] is set
||.((f . e) - (f . m)).|| is V33() real ext-real Element of REAL
the normF of vseq is Relation-like the carrier of vseq -defined REAL -valued Function-like non empty V14( the carrier of vseq) V18( the carrier of vseq, REAL ) V38() V39() V40() Element of bool [: the carrier of vseq,REAL:]
[: the carrier of vseq,REAL:] is non empty V38() V39() V40() set
bool [: the carrier of vseq,REAL:] is non empty set
the normF of vseq . ((f . e) - (f . m)) is V33() real ext-real Element of REAL
(vseq,(f . e),(f . m)) is V33() real ext-real Element of REAL
tseq is V33() real ext-real Element of REAL
tv is epsilon-transitive epsilon-connected ordinal natural V33() real ext-real V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
e is epsilon-transitive epsilon-connected ordinal natural V33() real ext-real V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V33() real ext-real V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
f . e is Element of the carrier of vseq
f . m is Element of the carrier of vseq
(vseq,(f . e),(f . m)) is V33() real ext-real Element of REAL
(f . e) - (f . m) is Element of the carrier of vseq
- (f . m) is Element of the carrier of vseq
(f . e) + (- (f . m)) is Element of the carrier of vseq
the addF of vseq is Relation-like [: the carrier of vseq, the carrier of vseq:] -defined the carrier of vseq -valued Function-like non empty V14([: the carrier of vseq, the carrier of vseq:]) V18([: the carrier of vseq, the carrier of vseq:], the carrier of vseq) Element of bool [:[: the carrier of vseq, the carrier of vseq:], the carrier of vseq:]
[: the carrier of vseq, the carrier of vseq:] is non empty set
[:[: the carrier of vseq, the carrier of vseq:], the carrier of vseq:] is non empty set
bool [:[: the carrier of vseq, the carrier of vseq:], the carrier of vseq:] is non empty set
the addF of vseq . ((f . e),(- (f . m))) is Element of the carrier of vseq
[(f . e),(- (f . m))] is set
the addF of vseq . [(f . e),(- (f . m))] is set
||.((f . e) - (f . m)).|| is V33() real ext-real Element of REAL
the normF of vseq is Relation-like the carrier of vseq -defined REAL -valued Function-like non empty V14( the carrier of vseq) V18( the carrier of vseq, REAL ) V38() V39() V40() Element of bool [: the carrier of vseq,REAL:]
[: the carrier of vseq,REAL:] is non empty V38() V39() V40() set
bool [: the carrier of vseq,REAL:] is non empty set
the normF of vseq . ((f . e) - (f . m)) is V33() real ext-real Element of REAL
tv is epsilon-transitive epsilon-connected ordinal natural V33() real ext-real V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
[:NAT, the carrier of ():] is non empty set
bool [:NAT, the carrier of ():] is non empty set
vseq is Relation-like NAT -defined the carrier of () -valued Function-like non empty V14( NAT ) V18( NAT , the carrier of ()) Element of bool [:NAT, the carrier of ():]
f is set
tseq is epsilon-transitive epsilon-connected ordinal natural V33() real ext-real V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
tv is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
lim tv is V33() Element of COMPLEX
e is V33() real ext-real Element of REAL
m is epsilon-transitive epsilon-connected ordinal natural V33() real ext-real V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
tv . m is V33() Element of COMPLEX
u is epsilon-transitive epsilon-connected ordinal natural V33() real ext-real V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
tv . u is V33() Element of COMPLEX
(tv . u) - (tv . m) is V33() Element of COMPLEX
|.((tv . u) - (tv . m)).| is V33() real ext-real Element of REAL
vseq . u is Element of the carrier of ()
vseq . m is Element of the carrier of ()
(vseq . u) - (vseq . m) is Element of the carrier of ()
- (vseq . m) is Element of the carrier of ()
(vseq . u) + (- (vseq . m)) is Element of the carrier of ()
the addF of () is Relation-like [: the carrier of (), the carrier of ():] -defined the carrier of () -valued Function-like non empty V14([: the carrier of (), the carrier of ():]) V18([: the carrier of (), the carrier of ():], the carrier of ()) Element of bool [:[: the carrier of (), the carrier of ():], the carrier of ():]
[: the carrier of (), the carrier of ():] is non empty set
[:[: the carrier of (), the carrier of ():], the carrier of ():] is non empty set
bool [:[: the carrier of (), the carrier of ():], the carrier of ():] is non empty set
the addF of () . ((vseq . u),(- (vseq . m))) is Element of the carrier of ()
[(vseq . u),(- (vseq . m))] is set
the addF of () . [(vseq . u),(- (vseq . m))] is set
seq_id ((vseq . u) - (vseq . m)) is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
|.(seq_id ((vseq . u) - (vseq . m))).| is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
n is epsilon-transitive epsilon-connected ordinal natural V33() real ext-real V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
|.(seq_id ((vseq . u) - (vseq . m))).| . n is V33() real ext-real Element of REAL
(seq_id ((vseq . u) - (vseq . m))) . n is V33() Element of COMPLEX
|.((seq_id ((vseq . u) - (vseq . m))) . n).| is V33() real ext-real Element of REAL
|.(seq_id ((vseq . u) - (vseq . m))).| . tseq is V33() real ext-real Element of REAL
Sum |.(seq_id ((vseq . u) - (vseq . m))).| is V33() real ext-real Element of REAL
seq_id (vseq . u) is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
seq_id (vseq . m) is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
(seq_id (vseq . u)) - (seq_id (vseq . m)) is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
- (seq_id (vseq . m)) is Relation-like NAT -defined Function-like V14( NAT ) V38() set
- 1 is non empty V33() real ext-real set
(- 1) (#) (seq_id (vseq . m)) is Relation-like NAT -defined Function-like V14( NAT ) V38() set
(seq_id (vseq . u)) + (- (seq_id (vseq . m))) is Relation-like NAT -defined Function-like V14( NAT ) V38() set
seq_id ((seq_id (vseq . u)) - (seq_id (vseq . m))) is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
- (seq_id (vseq . m)) is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
(seq_id (vseq . u)) + (- (seq_id (vseq . m))) is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
(seq_id ((vseq . u) - (vseq . m))) . tseq is V33() Element of COMPLEX
(seq_id (vseq . u)) . tseq is V33() Element of COMPLEX
(- (seq_id (vseq . m))) . tseq is V33() Element of COMPLEX
((seq_id (vseq . u)) . tseq) + ((- (seq_id (vseq . m))) . tseq) is V33() Element of COMPLEX
(seq_id (vseq . m)) . tseq is V33() Element of COMPLEX
- ((seq_id (vseq . m)) . tseq) is V33() Element of COMPLEX
((seq_id (vseq . u)) . tseq) + (- ((seq_id (vseq . m)) . tseq)) is V33() Element of COMPLEX
((seq_id (vseq . u)) . tseq) - ((seq_id (vseq . m)) . tseq) is V33() Element of COMPLEX
(tv . u) - ((seq_id (vseq . m)) . tseq) is V33() Element of COMPLEX
||.((vseq . u) - (vseq . m)).|| is V33() real ext-real Element of REAL
the normF of () is Relation-like the carrier of () -defined REAL -valued Function-like non empty V14( the carrier of ()) V18( the carrier of (), REAL ) V38() V39() V40() Element of bool [: the carrier of (),REAL:]
[: the carrier of (),REAL:] is non empty V38() V39() V40() set
bool [: the carrier of (),REAL:] is non empty set
the normF of () . ((vseq . u) - (vseq . m)) is V33() real ext-real Element of REAL
f is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
tv is epsilon-transitive epsilon-connected ordinal natural V33() real ext-real V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
e is set
f . e is V33() set
tseq is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
tseq . tv is V33() Element of COMPLEX
m is epsilon-transitive epsilon-connected ordinal natural V33() real ext-real V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
u is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
lim u is V33() Element of COMPLEX
seq_id tseq is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
tv is V33() real ext-real Element of REAL
tv / 2 is V33() real ext-real Element of REAL
m is epsilon-transitive epsilon-connected ordinal natural V33() real ext-real V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V33() real ext-real V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
u is epsilon-transitive epsilon-connected ordinal natural V33() real ext-real V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
vseq . n is Element of the carrier of ()
vseq . u is Element of the carrier of ()
(vseq . n) - (vseq . u) is Element of the carrier of ()
- (vseq . u) is Element of the carrier of ()
(vseq . n) + (- (vseq . u)) is Element of the carrier of ()
the addF of () is Relation-like [: the carrier of (), the carrier of ():] -defined the carrier of () -valued Function-like non empty V14([: the carrier of (), the carrier of ():]) V18([: the carrier of (), the carrier of ():], the carrier of ()) Element of bool [:[: the carrier of (), the carrier of ():], the carrier of ():]
[: the carrier of (), the carrier of ():] is non empty set
[:[: the carrier of (), the carrier of ():], the carrier of ():] is non empty set
bool [:[: the carrier of (), the carrier of ():], the carrier of ():] is non empty set
the addF of () . ((vseq . n),(- (vseq . u))) is Element of the carrier of ()
[(vseq . n),(- (vseq . u))] is set
the addF of () . [(vseq . n),(- (vseq . u))] is set
seq_id ((vseq . n) - (vseq . u)) is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
|.(seq_id ((vseq . n) - (vseq . u))).| is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
Sum |.(seq_id ((vseq . n) - (vseq . u))).| is V33() real ext-real Element of REAL
||.((vseq . n) - (vseq . u)).|| is V33() real ext-real Element of REAL
the normF of () is Relation-like the carrier of () -defined REAL -valued Function-like non empty V14( the carrier of ()) V18( the carrier of (), REAL ) V38() V39() V40() Element of bool [: the carrier of (),REAL:]
[: the carrier of (),REAL:] is non empty V38() V39() V40() set
bool [: the carrier of (),REAL:] is non empty set
the normF of () . ((vseq . n) - (vseq . u)) is V33() real ext-real Element of REAL
the normF of () . ((vseq . n) - (vseq . u)) is V33() real ext-real Element of REAL
v is epsilon-transitive epsilon-connected ordinal natural V33() real ext-real V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
|.(seq_id ((vseq . n) - (vseq . u))).| . v is V33() real ext-real Element of REAL
(seq_id ((vseq . n) - (vseq . u))) . v is V33() Element of COMPLEX
|.((seq_id ((vseq . n) - (vseq . u))) . v).| is V33() real ext-real Element of REAL
v is epsilon-transitive epsilon-connected ordinal natural V33() real ext-real V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
|.(seq_id ((vseq . n) - (vseq . u))).| . v is V33() real ext-real Element of REAL
u is epsilon-transitive epsilon-connected ordinal natural V33() real ext-real V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
vseq . u is Element of the carrier of ()
seq_id (vseq . u) is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
(seq_id tseq) - (seq_id (vseq . u)) is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
- (seq_id (vseq . u)) is Relation-like NAT -defined Function-like V14( NAT ) V38() set
- 1 is non empty V33() real ext-real set
(- 1) (#) (seq_id (vseq . u)) is Relation-like NAT -defined Function-like V14( NAT ) V38() set
(seq_id tseq) + (- (seq_id (vseq . u))) is Relation-like NAT -defined Function-like V14( NAT ) V38() set
|.((seq_id tseq) - (seq_id (vseq . u))).| is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
Partial_Sums |.((seq_id tseq) - (seq_id (vseq . u))).| is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
n is epsilon-transitive epsilon-connected ordinal natural V33() real ext-real V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
vseq . n is Element of the carrier of ()
v is epsilon-transitive epsilon-connected ordinal natural V33() real ext-real V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
vseq . v is Element of the carrier of ()
(vseq . n) - (vseq . v) is Element of the carrier of ()
- (vseq . v) is Element of the carrier of ()
(vseq . n) + (- (vseq . v)) is Element of the carrier of ()
the addF of () is Relation-like [: the carrier of (), the carrier of ():] -defined the carrier of () -valued Function-like non empty V14([: the carrier of (), the carrier of ():]) V18([: the carrier of (), the carrier of ():], the carrier of ()) Element of bool [:[: the carrier of (), the carrier of ():], the carrier of ():]
[: the carrier of (), the carrier of ():] is non empty set
[:[: the carrier of (), the carrier of ():], the carrier of ():] is non empty set
bool [:[: the carrier of (), the carrier of ():], the carrier of ():] is non empty set
the addF of () . ((vseq . n),(- (vseq . v))) is Element of the carrier of ()
[(vseq . n),(- (vseq . v))] is set
the addF of () . [(vseq . n),(- (vseq . v))] is set
seq_id ((vseq . n) - (vseq . v)) is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
seq_id (vseq . n) is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
seq_id (vseq . v) is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
(seq_id (vseq . n)) - (seq_id (vseq . v)) is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
- (seq_id (vseq . v)) is Relation-like NAT -defined Function-like V14( NAT ) V38() set
(- 1) (#) (seq_id (vseq . v)) is Relation-like NAT -defined Function-like V14( NAT ) V38() set
(seq_id (vseq . n)) + (- (seq_id (vseq . v))) is Relation-like NAT -defined Function-like V14( NAT ) V38() set
seq_id ((seq_id (vseq . n)) - (seq_id (vseq . v))) is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
n is epsilon-transitive epsilon-connected ordinal natural V33() real ext-real V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
(Partial_Sums |.((seq_id tseq) - (seq_id (vseq . u))).|) . n is V33() real ext-real Element of REAL
n + 1 is epsilon-transitive epsilon-connected ordinal natural V33() real ext-real V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
(Partial_Sums |.((seq_id tseq) - (seq_id (vseq . u))).|) . (n + 1) is V33() real ext-real Element of REAL
v is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
tseq . (n + 1) is V33() Element of COMPLEX
m is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
lim m is V33() Element of COMPLEX
rseq is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
lim rseq is V33() real ext-real Element of REAL
m is epsilon-transitive epsilon-connected ordinal natural V33() real ext-real V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
rseq . m is V33() real ext-real Element of REAL
vseq . m is Element of the carrier of ()
(vseq . m) - (vseq . u) is Element of the carrier of ()
- (vseq . u) is Element of the carrier of ()
(vseq . m) + (- (vseq . u)) is Element of the carrier of ()
the addF of () is Relation-like [: the carrier of (), the carrier of ():] -defined the carrier of () -valued Function-like non empty V14([: the carrier of (), the carrier of ():]) V18([: the carrier of (), the carrier of ():], the carrier of ()) Element of bool [:[: the carrier of (), the carrier of ():], the carrier of ():]
[: the carrier of (), the carrier of ():] is non empty set
[:[: the carrier of (), the carrier of ():], the carrier of ():] is non empty set
bool [:[: the carrier of (), the carrier of ():], the carrier of ():] is non empty set
the addF of () . ((vseq . m),(- (vseq . u))) is Element of the carrier of ()
[(vseq . m),(- (vseq . u))] is set
the addF of () . [(vseq . m),(- (vseq . u))] is set
seq_id ((vseq . m) - (vseq . u)) is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
|.(seq_id ((vseq . m) - (vseq . u))).| is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
Partial_Sums |.(seq_id ((vseq . m) - (vseq . u))).| is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
(Partial_Sums |.(seq_id ((vseq . m) - (vseq . u))).|) . (n + 1) is V33() real ext-real Element of REAL
|.(seq_id ((vseq . m) - (vseq . u))).| . (n + 1) is V33() real ext-real Element of REAL
(Partial_Sums |.(seq_id ((vseq . m) - (vseq . u))).|) . n is V33() real ext-real Element of REAL
(|.(seq_id ((vseq . m) - (vseq . u))).| . (n + 1)) + ((Partial_Sums |.(seq_id ((vseq . m) - (vseq . u))).|) . n) is V33() real ext-real Element of REAL
seq_id (vseq . m) is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
(seq_id (vseq . m)) - (seq_id (vseq . u)) is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
(seq_id (vseq . m)) + (- (seq_id (vseq . u))) is Relation-like NAT -defined Function-like V14( NAT ) V38() set
|.((seq_id (vseq . m)) - (seq_id (vseq . u))).| is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
|.((seq_id (vseq . m)) - (seq_id (vseq . u))).| . (n + 1) is V33() real ext-real Element of REAL
(|.((seq_id (vseq . m)) - (seq_id (vseq . u))).| . (n + 1)) + ((Partial_Sums |.(seq_id ((vseq . m) - (vseq . u))).|) . n) is V33() real ext-real Element of REAL
v . m is V33() real ext-real Element of REAL
(|.((seq_id (vseq . m)) - (seq_id (vseq . u))).| . (n + 1)) + (v . m) is V33() real ext-real Element of REAL
- (seq_id (vseq . u)) is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
(seq_id (vseq . m)) + (- (seq_id (vseq . u))) is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
((seq_id (vseq . m)) + (- (seq_id (vseq . u)))) . (n + 1) is V33() Element of COMPLEX
|.(((seq_id (vseq . m)) + (- (seq_id (vseq . u)))) . (n + 1)).| is V33() real ext-real Element of REAL
|.(((seq_id (vseq . m)) + (- (seq_id (vseq . u)))) . (n + 1)).| + (v . m) is V33() real ext-real Element of REAL
(seq_id (vseq . m)) . (n + 1) is V33() Element of COMPLEX
(- (seq_id (vseq . u))) . (n + 1) is V33() Element of COMPLEX
((seq_id (vseq . m)) . (n + 1)) + ((- (seq_id (vseq . u))) . (n + 1)) is V33() Element of COMPLEX
|.(((seq_id (vseq . m)) . (n + 1)) + ((- (seq_id (vseq . u))) . (n + 1))).| is V33() real ext-real Element of REAL
|.(((seq_id (vseq . m)) . (n + 1)) + ((- (seq_id (vseq . u))) . (n + 1))).| + (v . m) is V33() real ext-real Element of REAL
(seq_id (vseq . u)) . (n + 1) is V33() Element of COMPLEX
- ((seq_id (vseq . u)) . (n + 1)) is V33() Element of COMPLEX
((seq_id (vseq . m)) . (n + 1)) + (- ((seq_id (vseq . u)) . (n + 1))) is V33() Element of COMPLEX
|.(((seq_id (vseq . m)) . (n + 1)) + (- ((seq_id (vseq . u)) . (n + 1)))).| is V33() real ext-real Element of REAL
|.(((seq_id (vseq . m)) . (n + 1)) + (- ((seq_id (vseq . u)) . (n + 1)))).| + (v . m) is V33() real ext-real Element of REAL
((seq_id (vseq . m)) . (n + 1)) - ((seq_id (vseq . u)) . (n + 1)) is V33() Element of COMPLEX
|.(((seq_id (vseq . m)) . (n + 1)) - ((seq_id (vseq . u)) . (n + 1))).| is V33() real ext-real Element of REAL
|.(((seq_id (vseq . m)) . (n + 1)) - ((seq_id (vseq . u)) . (n + 1))).| + (v . m) is V33() real ext-real Element of REAL
m . m is V33() Element of COMPLEX
(m . m) - ((seq_id (vseq . u)) . (n + 1)) is V33() Element of COMPLEX
|.((m . m) - ((seq_id (vseq . u)) . (n + 1))).| is V33() real ext-real Element of REAL
|.((m . m) - ((seq_id (vseq . u)) . (n + 1))).| + (v . m) is V33() real ext-real Element of REAL
(lim m) - ((seq_id (vseq . u)) . (n + 1)) is V33() Element of COMPLEX
|.((lim m) - ((seq_id (vseq . u)) . (n + 1))).| is V33() real ext-real Element of REAL
lim v is V33() real ext-real Element of REAL
|.((lim m) - ((seq_id (vseq . u)) . (n + 1))).| + (lim v) is V33() real ext-real Element of REAL
(tseq . (n + 1)) + (- ((seq_id (vseq . u)) . (n + 1))) is V33() Element of COMPLEX
|.((tseq . (n + 1)) + (- ((seq_id (vseq . u)) . (n + 1)))).| is V33() real ext-real Element of REAL
|.((tseq . (n + 1)) + (- ((seq_id (vseq . u)) . (n + 1)))).| + (lim v) is V33() real ext-real Element of REAL
(tseq . (n + 1)) + ((- (seq_id (vseq . u))) . (n + 1)) is V33() Element of COMPLEX
|.((tseq . (n + 1)) + ((- (seq_id (vseq . u))) . (n + 1))).| is V33() real ext-real Element of REAL
|.((tseq . (n + 1)) + ((- (seq_id (vseq . u))) . (n + 1))).| + (lim v) is V33() real ext-real Element of REAL
tseq - (seq_id (vseq . u)) is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
tseq + (- (seq_id (vseq . u))) is Relation-like NAT -defined Function-like V14( NAT ) V38() set
(tseq - (seq_id (vseq . u))) . (n + 1) is V33() Element of COMPLEX
|.((tseq - (seq_id (vseq . u))) . (n + 1)).| is V33() real ext-real Element of REAL
|.((tseq - (seq_id (vseq . u))) . (n + 1)).| + (lim v) is V33() real ext-real Element of REAL
|.(tseq - (seq_id (vseq . u))).| is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
|.(tseq - (seq_id (vseq . u))).| . (n + 1) is V33() real ext-real Element of REAL
(|.(tseq - (seq_id (vseq . u))).| . (n + 1)) + (lim v) is V33() real ext-real Element of REAL
(|.(tseq - (seq_id (vseq . u))).| . (n + 1)) + ((Partial_Sums |.((seq_id tseq) - (seq_id (vseq . u))).|) . n) is V33() real ext-real Element of REAL
|.((seq_id tseq) - (seq_id (vseq . u))).| . (n + 1) is V33() real ext-real Element of REAL
(|.((seq_id tseq) - (seq_id (vseq . u))).| . (n + 1)) + ((Partial_Sums |.((seq_id tseq) - (seq_id (vseq . u))).|) . n) is V33() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V33() real ext-real V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
(Partial_Sums |.((seq_id tseq) - (seq_id (vseq . u))).|) . n is V33() real ext-real Element of REAL
v is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
n + 1 is epsilon-transitive epsilon-connected ordinal natural V33() real ext-real V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
lim v is V33() real ext-real Element of REAL
(Partial_Sums |.((seq_id tseq) - (seq_id (vseq . u))).|) . (n + 1) is V33() real ext-real Element of REAL
n is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
lim n is V33() real ext-real Element of REAL
(Partial_Sums |.((seq_id tseq) - (seq_id (vseq . u))).|) . 0 is V33() real ext-real Element of REAL
tseq . 0 is V33() Element of COMPLEX
v is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
lim v is V33() Element of COMPLEX
(seq_id (vseq . u)) . 0 is V33() Element of COMPLEX
m is epsilon-transitive epsilon-connected ordinal natural V33() real ext-real V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
n . m is V33() real ext-real Element of REAL
v . m is V33() Element of COMPLEX
(v . m) - ((seq_id (vseq . u)) . 0) is V33() Element of COMPLEX
|.((v . m) - ((seq_id (vseq . u)) . 0)).| is V33() real ext-real Element of REAL
vseq . m is Element of the carrier of ()
(vseq . m) - (vseq . u) is Element of the carrier of ()
- (vseq . u) is Element of the carrier of ()
(vseq . m) + (- (vseq . u)) is Element of the carrier of ()
the addF of () is Relation-like [: the carrier of (), the carrier of ():] -defined the carrier of () -valued Function-like non empty V14([: the carrier of (), the carrier of ():]) V18([: the carrier of (), the carrier of ():], the carrier of ()) Element of bool [:[: the carrier of (), the carrier of ():], the carrier of ():]
[: the carrier of (), the carrier of ():] is non empty set
[:[: the carrier of (), the carrier of ():], the carrier of ():] is non empty set
bool [:[: the carrier of (), the carrier of ():], the carrier of ():] is non empty set
the addF of () . ((vseq . m),(- (vseq . u))) is Element of the carrier of ()
[(vseq . m),(- (vseq . u))] is set
the addF of () . [(vseq . m),(- (vseq . u))] is set
seq_id ((vseq . m) - (vseq . u)) is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
|.(seq_id ((vseq . m) - (vseq . u))).| is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
Partial_Sums |.(seq_id ((vseq . m) - (vseq . u))).| is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
(Partial_Sums |.(seq_id ((vseq . m) - (vseq . u))).|) . 0 is V33() real ext-real Element of REAL
|.(seq_id ((vseq . m) - (vseq . u))).| . 0 is V33() real ext-real Element of REAL
seq_id (vseq . m) is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
(seq_id (vseq . m)) - (seq_id (vseq . u)) is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
(seq_id (vseq . m)) + (- (seq_id (vseq . u))) is Relation-like NAT -defined Function-like V14( NAT ) V38() set
|.((seq_id (vseq . m)) - (seq_id (vseq . u))).| is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
|.((seq_id (vseq . m)) - (seq_id (vseq . u))).| . 0 is V33() real ext-real Element of REAL
- (seq_id (vseq . u)) is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
(seq_id (vseq . m)) + (- (seq_id (vseq . u))) is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
((seq_id (vseq . m)) + (- (seq_id (vseq . u)))) . 0 is V33() Element of COMPLEX
|.(((seq_id (vseq . m)) + (- (seq_id (vseq . u)))) . 0).| is V33() real ext-real Element of REAL
(seq_id (vseq . m)) . 0 is V33() Element of COMPLEX
(- (seq_id (vseq . u))) . 0 is V33() Element of COMPLEX
((seq_id (vseq . m)) . 0) + ((- (seq_id (vseq . u))) . 0) is V33() Element of COMPLEX
|.(((seq_id (vseq . m)) . 0) + ((- (seq_id (vseq . u))) . 0)).| is V33() real ext-real Element of REAL
- ((seq_id (vseq . u)) . 0) is V33() Element of COMPLEX
((seq_id (vseq . m)) . 0) + (- ((seq_id (vseq . u)) . 0)) is V33() Element of COMPLEX
|.(((seq_id (vseq . m)) . 0) + (- ((seq_id (vseq . u)) . 0))).| is V33() real ext-real Element of REAL
((seq_id (vseq . m)) . 0) - ((seq_id (vseq . u)) . 0) is V33() Element of COMPLEX
|.(((seq_id (vseq . m)) . 0) - ((seq_id (vseq . u)) . 0)).| is V33() real ext-real Element of REAL
(lim v) - ((seq_id (vseq . u)) . 0) is V33() Element of COMPLEX
|.((lim v) - ((seq_id (vseq . u)) . 0)).| is V33() real ext-real Element of REAL
- ((seq_id (vseq . u)) . 0) is V33() Element of COMPLEX
(tseq . 0) + (- ((seq_id (vseq . u)) . 0)) is V33() Element of COMPLEX
|.((tseq . 0) + (- ((seq_id (vseq . u)) . 0))).| is V33() real ext-real Element of REAL
- (seq_id (vseq . u)) is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
(- (seq_id (vseq . u))) . 0 is V33() Element of COMPLEX
(tseq . 0) + ((- (seq_id (vseq . u))) . 0) is V33() Element of COMPLEX
|.((tseq . 0) + ((- (seq_id (vseq . u))) . 0)).| is V33() real ext-real Element of REAL
tseq - (seq_id (vseq . u)) is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
tseq + (- (seq_id (vseq . u))) is Relation-like NAT -defined Function-like V14( NAT ) V38() set
(tseq - (seq_id (vseq . u))) . 0 is V33() Element of COMPLEX
|.((tseq - (seq_id (vseq . u))) . 0).| is V33() real ext-real Element of REAL
((seq_id tseq) - (seq_id (vseq . u))) . 0 is V33() Element of COMPLEX
|.(((seq_id tseq) - (seq_id (vseq . u))) . 0).| is V33() real ext-real Element of REAL
|.((seq_id tseq) - (seq_id (vseq . u))).| . 0 is V33() real ext-real Element of REAL
n is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
lim n is V33() real ext-real Element of REAL
v is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
n is epsilon-transitive epsilon-connected ordinal natural V33() real ext-real V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
lim v is V33() real ext-real Element of REAL
(Partial_Sums |.((seq_id tseq) - (seq_id (vseq . u))).|) . n is V33() real ext-real Element of REAL
u is epsilon-transitive epsilon-connected ordinal natural V33() real ext-real V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
vseq . u is Element of the carrier of ()
seq_id (vseq . u) is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
(seq_id tseq) - (seq_id (vseq . u)) is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
- (seq_id (vseq . u)) is Relation-like NAT -defined Function-like V14( NAT ) V38() set
- 1 is non empty V33() real ext-real set
(- 1) (#) (seq_id (vseq . u)) is Relation-like NAT -defined Function-like V14( NAT ) V38() set
(seq_id tseq) + (- (seq_id (vseq . u))) is Relation-like NAT -defined Function-like V14( NAT ) V38() set
|.((seq_id tseq) - (seq_id (vseq . u))).| is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
Sum |.((seq_id tseq) - (seq_id (vseq . u))).| is V33() real ext-real Element of REAL
Partial_Sums |.((seq_id tseq) - (seq_id (vseq . u))).| is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
n is epsilon-transitive epsilon-connected ordinal natural V33() real ext-real V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
(Partial_Sums |.((seq_id tseq) - (seq_id (vseq . u))).|) . n is V33() real ext-real Element of REAL
v is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
m is epsilon-transitive epsilon-connected ordinal natural V33() real ext-real V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
v . m is V33() real ext-real Element of REAL
vseq . m is Element of the carrier of ()
(vseq . m) - (vseq . u) is Element of the carrier of ()
- (vseq . u) is Element of the carrier of ()
(vseq . m) + (- (vseq . u)) is Element of the carrier of ()
the addF of () is Relation-like [: the carrier of (), the carrier of ():] -defined the carrier of () -valued Function-like non empty V14([: the carrier of (), the carrier of ():]) V18([: the carrier of (), the carrier of ():], the carrier of ()) Element of bool [:[: the carrier of (), the carrier of ():], the carrier of ():]
[: the carrier of (), the carrier of ():] is non empty set
[:[: the carrier of (), the carrier of ():], the carrier of ():] is non empty set
bool [:[: the carrier of (), the carrier of ():], the carrier of ():] is non empty set
the addF of () . ((vseq . m),(- (vseq . u))) is Element of the carrier of ()
[(vseq . m),(- (vseq . u))] is set
the addF of () . [(vseq . m),(- (vseq . u))] is set
seq_id ((vseq . m) - (vseq . u)) is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
|.(seq_id ((vseq . m) - (vseq . u))).| is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
Partial_Sums |.(seq_id ((vseq . m) - (vseq . u))).| is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
(Partial_Sums |.(seq_id ((vseq . m) - (vseq . u))).|) . n is V33() real ext-real Element of REAL
rseq is epsilon-transitive epsilon-connected ordinal natural V33() real ext-real V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
|.(seq_id ((vseq . m) - (vseq . u))).| . rseq is V33() real ext-real Element of REAL
Sum |.(seq_id ((vseq . m) - (vseq . u))).| is V33() real ext-real Element of REAL
lim v is V33() real ext-real Element of REAL
v is epsilon-transitive epsilon-connected ordinal natural V33() real ext-real V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
(Partial_Sums |.((seq_id tseq) - (seq_id (vseq . u))).|) . v is V33() real ext-real Element of REAL
n is V33() real ext-real Element of REAL
n is V33() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V33() real ext-real V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
|.((seq_id tseq) - (seq_id (vseq . u))).| . n is V33() real ext-real Element of REAL
((seq_id tseq) - (seq_id (vseq . u))) . n is V33() Element of COMPLEX
|.(((seq_id tseq) - (seq_id (vseq . u))) . n).| is V33() real ext-real Element of REAL
lim (Partial_Sums |.((seq_id tseq) - (seq_id (vseq . u))).|) is V33() real ext-real Element of REAL
|.(seq_id tseq).| is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
e is epsilon-transitive epsilon-connected ordinal natural V33() real ext-real V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
|.(seq_id tseq).| . e is V33() real ext-real Element of REAL
(seq_id tseq) . e is V33() Element of COMPLEX
|.((seq_id tseq) . e).| is V33() real ext-real Element of REAL
e is epsilon-transitive epsilon-connected ordinal natural V33() real ext-real V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
vseq . e is Element of the carrier of ()
seq_id (vseq . e) is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
|.(seq_id (vseq . e)).| is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
(seq_id tseq) - (seq_id (vseq . e)) is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
- (seq_id (vseq . e)) is Relation-like NAT -defined Function-like V14( NAT ) V38() set
- 1 is non empty V33() real ext-real set
(- 1) (#) (seq_id (vseq . e)) is Relation-like NAT -defined Function-like V14( NAT ) V38() set
(seq_id tseq) + (- (seq_id (vseq . e))) is Relation-like NAT -defined Function-like V14( NAT ) V38() set
|.((seq_id tseq) - (seq_id (vseq . e))).| is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
|.((seq_id tseq) - (seq_id (vseq . e))).| + |.(seq_id (vseq . e)).| is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
n is epsilon-transitive epsilon-connected ordinal natural V33() real ext-real V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
|.(seq_id tseq).| . n is V33() real ext-real Element of REAL
(|.((seq_id tseq) - (seq_id (vseq . e))).| + |.(seq_id (vseq . e)).|) . n is V33() real ext-real Element of REAL
|.(seq_id (vseq . e)).| . n is V33() real ext-real Element of REAL
(seq_id (vseq . e)) . n is V33() Element of COMPLEX
|.((seq_id (vseq . e)) . n).| is V33() real ext-real Element of REAL
(seq_id tseq) . n is V33() Element of COMPLEX
|.((seq_id tseq) . n).| is V33() real ext-real Element of REAL
|.((seq_id tseq) - (seq_id (vseq . e))).| . n is V33() real ext-real Element of REAL
- (seq_id (vseq . e)) is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
(seq_id tseq) + (- (seq_id (vseq . e))) is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
((seq_id tseq) + (- (seq_id (vseq . e)))) . n is V33() Element of COMPLEX
|.(((seq_id tseq) + (- (seq_id (vseq . e)))) . n).| is V33() real ext-real Element of REAL
(- (seq_id (vseq . e))) . n is V33() Element of COMPLEX
((seq_id tseq) . n) + ((- (seq_id (vseq . e))) . n) is V33() Element of COMPLEX
|.(((seq_id tseq) . n) + ((- (seq_id (vseq . e))) . n)).| is V33() real ext-real Element of REAL
- ((seq_id (vseq . e)) . n) is V33() Element of COMPLEX
((seq_id tseq) . n) + (- ((seq_id (vseq . e)) . n)) is V33() Element of COMPLEX
|.(((seq_id tseq) . n) + (- ((seq_id (vseq . e)) . n))).| is V33() real ext-real Element of REAL
((seq_id tseq) . n) - ((seq_id (vseq . e)) . n) is V33() Element of COMPLEX
|.(((seq_id tseq) . n) - ((seq_id (vseq . e)) . n)).| is V33() real ext-real Element of REAL
(|.(seq_id tseq).| . n) - (|.(seq_id (vseq . e)).| . n) is V33() real ext-real Element of REAL
((|.(seq_id tseq).| . n) - (|.(seq_id (vseq . e)).| . n)) + (|.(seq_id (vseq . e)).| . n) is V33() real ext-real Element of REAL
(|.((seq_id tseq) - (seq_id (vseq . e))).| . n) + (|.(seq_id (vseq . e)).| . n) is V33() real ext-real Element of REAL
tv is Element of the carrier of ()
e is V33() real ext-real Element of REAL
m is epsilon-transitive epsilon-connected ordinal natural V33() real ext-real V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V33() real ext-real V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
vseq . n is Element of the carrier of ()
seq_id (vseq . n) is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
(seq_id tseq) - (seq_id (vseq . n)) is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
- (seq_id (vseq . n)) is Relation-like NAT -defined Function-like V14( NAT ) V38() set
- 1 is non empty V33() real ext-real set
(- 1) (#) (seq_id (vseq . n)) is Relation-like NAT -defined Function-like V14( NAT ) V38() set
(seq_id tseq) + (- (seq_id (vseq . n))) is Relation-like NAT -defined Function-like V14( NAT ) V38() set
|.((seq_id tseq) - (seq_id (vseq . n))).| is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
Sum |.((seq_id tseq) - (seq_id (vseq . n))).| is V33() real ext-real Element of REAL
u is Element of the carrier of ()
v is Element of the carrier of ()
u - v is Element of the carrier of ()
- v is Element of the carrier of ()
u + (- v) is Element of the carrier of ()
the addF of () is Relation-like [: the carrier of (), the carrier of ():] -defined the carrier of () -valued Function-like non empty V14([: the carrier of (), the carrier of ():]) V18([: the carrier of (), the carrier of ():], the carrier of ()) Element of bool [:[: the carrier of (), the carrier of ():], the carrier of ():]
[: the carrier of (), the carrier of ():] is non empty set
[:[: the carrier of (), the carrier of ():], the carrier of ():] is non empty set
bool [:[: the carrier of (), the carrier of ():], the carrier of ():] is non empty set
the addF of () . (u,(- v)) is Element of the carrier of ()
[u,(- v)] is set
the addF of () . [u,(- v)] is set
seq_id (u - v) is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) V18( NAT , COMPLEX ) V38() Element of bool [:NAT,COMPLEX:]
|.(seq_id (u - v)).| is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
Sum |.(seq_id (u - v)).| is V33() real ext-real Element of REAL
the normF of () is Relation-like the carrier of () -defined REAL -valued Function-like non empty V14( the carrier of ()) V18( the carrier of (), REAL ) V38() V39() V40() Element of bool [: the carrier of (),REAL:]
[: the carrier of (),REAL:] is non empty V38() V39() V40() set
bool [: the carrier of (),REAL:] is non empty set
the normF of () . (u - v) is V33() real ext-real Element of REAL
(vseq . n) - tv is Element of the carrier of ()
- tv is Element of the carrier of ()
(vseq . n) + (- tv) is Element of the carrier of ()
the addF of () . ((vseq . n),(- tv)) is Element of the carrier of ()
[(vseq . n),(- tv)] is set
the addF of () . [(vseq . n),(- tv)] is set
||.((vseq . n) - tv).|| is V33() real ext-real Element of REAL
the normF of () . ((vseq . n) - tv) is V33() real ext-real Element of REAL
tv - (vseq . n) is Element of the carrier of ()
- (vseq . n) is Element of the carrier of ()
tv + (- (vseq . n)) is Element of the carrier of ()
the addF of () . (tv,(- (vseq . n))) is Element of the carrier of ()
[tv,(- (vseq . n))] is set
the addF of () . [tv,(- (vseq . n))] is set
- (tv - (vseq . n)) is Element of the carrier of ()
||.(- (tv - (vseq . n))).|| is V33() real ext-real Element of REAL
the normF of () . (- (tv - (vseq . n))) is V33() real ext-real Element of REAL
||.(tv - (vseq . n)).|| is V33() real ext-real Element of REAL
the normF of () . (tv - (vseq . n)) is V33() real ext-real Element of REAL