:: RSSPACE3 semantic presentation

REAL is non empty V51() V57() V58() V59() V63() set
NAT is non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() Element of bool REAL
bool REAL is set
COMPLEX is non empty V51() V57() V63() set
RAT is non empty V51() V57() V58() V59() V60() V63() set
INT is non empty V51() V57() V58() V59() V60() V61() V63() set
[:NAT,REAL:] is V38() V39() V40() set
bool [:NAT,REAL:] is set
omega is non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() set
bool omega is set
bool NAT is set
the_set_of_RealSequences is non empty set
[:the_set_of_RealSequences,the_set_of_RealSequences:] is set
[:[:the_set_of_RealSequences,the_set_of_RealSequences:],the_set_of_RealSequences:] is set
bool [:[:the_set_of_RealSequences,the_set_of_RealSequences:],the_set_of_RealSequences:] is set
[:REAL,the_set_of_RealSequences:] is set
[:[:REAL,the_set_of_RealSequences:],the_set_of_RealSequences:] is set
bool [:[:REAL,the_set_of_RealSequences:],the_set_of_RealSequences:] is set
Linear_Space_of_RealSequences is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() RLSStruct
the carrier of Linear_Space_of_RealSequences is non empty set
bool the carrier of Linear_Space_of_RealSequences is set
the_set_of_l2RealSequences is non empty linearly-closed Element of bool the carrier of Linear_Space_of_RealSequences
[:the_set_of_l2RealSequences,the_set_of_l2RealSequences:] is set
[:[:the_set_of_l2RealSequences,the_set_of_l2RealSequences:],REAL:] is V38() V39() V40() set
bool [:[:the_set_of_l2RealSequences,the_set_of_l2RealSequences:],REAL:] is set
[:COMPLEX,COMPLEX:] is V38() set
bool [:COMPLEX,COMPLEX:] is set
[:[:COMPLEX,COMPLEX:],COMPLEX:] is V38() set
bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is set
[:REAL,REAL:] is V38() V39() V40() set
bool [:REAL,REAL:] is set
[:[:REAL,REAL:],REAL:] is V38() V39() V40() set
bool [:[:REAL,REAL:],REAL:] is set
[:RAT,RAT:] is RAT -valued V38() V39() V40() set
bool [:RAT,RAT:] is set
[:[:RAT,RAT:],RAT:] is RAT -valued V38() V39() V40() set
bool [:[:RAT,RAT:],RAT:] is set
[:INT,INT:] is RAT -valued INT -valued V38() V39() V40() set
bool [:INT,INT:] is set
[:[:INT,INT:],INT:] is RAT -valued INT -valued V38() V39() V40() set
bool [:[:INT,INT:],INT:] is set
[:NAT,NAT:] is RAT -valued INT -valued V38() V39() V40() V41() set
[:[:NAT,NAT:],NAT:] is RAT -valued INT -valued V38() V39() V40() V41() set
bool [:[:NAT,NAT:],NAT:] is set
{} is empty ext-real epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V36() real V57() V58() V59() V60() V61() V62() V63() set
1 is non empty ext-real positive epsilon-transitive epsilon-connected ordinal natural V36() real V50() V56() V57() V58() V59() V60() V61() V62() Element of NAT
0 is empty ext-real epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V36() real V50() V56() V57() V58() V59() V60() V61() V62() V63() Element of NAT
- 1 is ext-real V36() real Element of REAL
Zeroseq is Element of the_set_of_RealSequences
l_add is Relation-like [:the_set_of_RealSequences,the_set_of_RealSequences:] -defined the_set_of_RealSequences -valued Function-like V14([:the_set_of_RealSequences,the_set_of_RealSequences:]) V18([:the_set_of_RealSequences,the_set_of_RealSequences:], the_set_of_RealSequences ) Element of bool [:[:the_set_of_RealSequences,the_set_of_RealSequences:],the_set_of_RealSequences:]
l_mult is Relation-like [:REAL,the_set_of_RealSequences:] -defined the_set_of_RealSequences -valued Function-like V14([:REAL,the_set_of_RealSequences:]) V18([:REAL,the_set_of_RealSequences:], the_set_of_RealSequences ) Element of bool [:[:REAL,the_set_of_RealSequences:],the_set_of_RealSequences:]
RLSStruct(# the_set_of_RealSequences,Zeroseq,l_add,l_mult #) is non empty strict Abelian RLSStruct
the carrier of RLSStruct(# the_set_of_RealSequences,Zeroseq,l_add,l_mult #) is non empty set
2 is non empty ext-real positive epsilon-transitive epsilon-connected ordinal natural V36() real V50() V56() V57() V58() V59() V60() V61() V62() Element of NAT
vseq is set
f is set
bool the_set_of_RealSequences is set
vseq is Element of bool the carrier of Linear_Space_of_RealSequences
f is Element of bool the carrier of Linear_Space_of_RealSequences
tseq is set
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:]
tseq is set
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:]
() is Element of bool the carrier of Linear_Space_of_RealSequences
vseq is ext-real V36() real Element of REAL
NAT --> vseq is Relation-like NAT -defined REAL -valued Function-like constant non empty V14( NAT ) V18( NAT , REAL ) V38() V39() V40() convergent Element of bool [:NAT,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 ext-real V36() real Element of REAL
(lim tseq) - vseq is ext-real V36() real Element of REAL
abs ((lim tseq) - vseq) is ext-real V36() 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 - 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:]
abs (tseq - 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 Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
lim tv is ext-real V36() real Element of REAL
e is ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V50() V56() V57() V58() V59() V60() V61() V62() Element of NAT
tv . e is ext-real V36() real Element of REAL
tseq . e is ext-real V36() real Element of REAL
(tseq . e) - vseq is ext-real V36() real Element of REAL
abs ((tseq . e) - vseq) is ext-real V36() real Element of REAL
f . e is ext-real V36() real Element of REAL
(tseq . e) - (f . e) is ext-real V36() real Element of REAL
abs ((tseq . e) - (f . e)) is ext-real V36() real Element of REAL
- (f . e) is ext-real V36() real Element of REAL
(tseq . e) + (- (f . e)) is ext-real V36() real Element of REAL
abs ((tseq . e) + (- (f . e))) is ext-real V36() 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:]
(- f) . e is ext-real V36() real Element of REAL
(tseq . e) + ((- f) . e) is ext-real V36() real Element of REAL
abs ((tseq . e) + ((- f) . e)) is ext-real V36() real Element of REAL
tseq + (- 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 + (- f)) . e is ext-real V36() real Element of REAL
abs ((tseq + (- f)) . e) is ext-real V36() real Element of REAL
(tseq - f) . e is ext-real V36() real Element of REAL
abs ((tseq - f) . e) is ext-real V36() real Element of REAL
(abs (tseq - f)) . e is ext-real V36() real Element of REAL
e is set
tv . e is ext-real V36() real Element of REAL
(abs (tseq - f)) . e is ext-real V36() real Element of REAL
lim (abs (tseq - f)) is ext-real V36() real Element of REAL
lim (tseq - f) is ext-real V36() real Element of REAL
abs (lim (tseq - f)) is ext-real V36() real Element of REAL
lim f is ext-real V36() real Element of REAL
(lim tseq) - (lim f) is ext-real V36() real Element of REAL
abs ((lim tseq) - (lim f)) is ext-real V36() real Element of REAL
f . 0 is ext-real V36() real Element of REAL
(lim tseq) - (f . 0) is ext-real V36() real Element of REAL
abs ((lim tseq) - (f . 0)) is ext-real V36() real Element of REAL
seq_id Zeroseq is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
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 ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V50() V56() V57() V58() V59() V60() V61() V62() Element of NAT
vseq . f is ext-real V36() real Element of REAL
f is Element of the carrier of Linear_Space_of_RealSequences
tseq is Element of the carrier of Linear_Space_of_RealSequences
f + tseq is Element of the carrier of Linear_Space_of_RealSequences
the addF of Linear_Space_of_RealSequences is Relation-like [: the carrier of Linear_Space_of_RealSequences, the carrier of Linear_Space_of_RealSequences:] -defined the carrier of Linear_Space_of_RealSequences -valued Function-like V14([: the carrier of Linear_Space_of_RealSequences, the carrier of Linear_Space_of_RealSequences:]) V18([: the carrier of Linear_Space_of_RealSequences, the carrier of Linear_Space_of_RealSequences:], the carrier of Linear_Space_of_RealSequences) Element of bool [:[: the carrier of Linear_Space_of_RealSequences, the carrier of Linear_Space_of_RealSequences:], the carrier of Linear_Space_of_RealSequences:]
[: the carrier of Linear_Space_of_RealSequences, the carrier of Linear_Space_of_RealSequences:] is set
[:[: the carrier of Linear_Space_of_RealSequences, the carrier of Linear_Space_of_RealSequences:], the carrier of Linear_Space_of_RealSequences:] is set
bool [:[: the carrier of Linear_Space_of_RealSequences, the carrier of Linear_Space_of_RealSequences:], the carrier of Linear_Space_of_RealSequences:] is set
the addF of Linear_Space_of_RealSequences . (f,tseq) is Element of the carrier of Linear_Space_of_RealSequences
[f,tseq] is set
the addF of Linear_Space_of_RealSequences . [f,tseq] is set
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:]
abs (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 REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
abs (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 REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
abs (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 ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V50() V56() V57() V58() V59() V60() V61() V62() Element of NAT
(abs (seq_id (f + tseq))) . u is ext-real V36() real Element of REAL
(seq_id (f + tseq)) . u is ext-real V36() real Element of REAL
abs ((seq_id (f + tseq)) . u) is ext-real V36() real Element of REAL
(abs (seq_id f)) + (abs (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 ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V50() V56() V57() V58() V59() V60() V61() V62() Element of NAT
(abs (seq_id (f + tseq))) . u is ext-real V36() real Element of REAL
((abs (seq_id f)) + (abs (seq_id tseq))) . u is ext-real V36() real Element of REAL
(seq_id f) . u is ext-real V36() real Element of REAL
abs ((seq_id f) . u) is ext-real V36() real Element of REAL
(seq_id tseq) . u is ext-real V36() real Element of REAL
abs ((seq_id tseq) . u) is ext-real V36() real Element of REAL
(abs ((seq_id f) . u)) + (abs ((seq_id tseq) . u)) is ext-real V36() real Element of REAL
(abs (seq_id f)) . u is ext-real V36() real Element of REAL
((abs (seq_id f)) . u) + (abs ((seq_id tseq) . u)) is ext-real V36() real Element of REAL
(abs (seq_id tseq)) . u is ext-real V36() real Element of REAL
((abs (seq_id f)) . u) + ((abs (seq_id tseq)) . u) is ext-real V36() real Element of REAL
(seq_id (f + tseq)) . u is ext-real V36() real Element of REAL
abs ((seq_id (f + tseq)) . u) is ext-real V36() 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:]
seq_id ((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:]
(seq_id ((seq_id f) + (seq_id tseq))) . u is ext-real V36() real Element of REAL
abs ((seq_id ((seq_id f) + (seq_id tseq))) . u) is ext-real V36() real Element of REAL
((seq_id f) + (seq_id tseq)) . u is ext-real V36() real Element of REAL
abs (((seq_id f) + (seq_id tseq)) . u) is ext-real V36() real Element of REAL
((seq_id f) . u) + ((seq_id tseq) . u) is ext-real V36() real Element of REAL
abs (((seq_id f) . u) + ((seq_id tseq) . u)) is ext-real V36() real Element of REAL
f is ext-real V36() real Element of REAL
tseq is Element of the carrier of Linear_Space_of_RealSequences
f * tseq is Element of the carrier of Linear_Space_of_RealSequences
the Mult of Linear_Space_of_RealSequences is Relation-like [:REAL, the carrier of Linear_Space_of_RealSequences:] -defined the carrier of Linear_Space_of_RealSequences -valued Function-like V14([:REAL, the carrier of Linear_Space_of_RealSequences:]) V18([:REAL, the carrier of Linear_Space_of_RealSequences:], the carrier of Linear_Space_of_RealSequences) Element of bool [:[:REAL, the carrier of Linear_Space_of_RealSequences:], the carrier of Linear_Space_of_RealSequences:]
[:REAL, the carrier of Linear_Space_of_RealSequences:] is set
[:[:REAL, the carrier of Linear_Space_of_RealSequences:], the carrier of Linear_Space_of_RealSequences:] is set
bool [:[:REAL, the carrier of Linear_Space_of_RealSequences:], the carrier of Linear_Space_of_RealSequences:] is set
the Mult of Linear_Space_of_RealSequences . (f,tseq) is set
[f,tseq] is set
the Mult of Linear_Space_of_RealSequences . [f,tseq] is set
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 REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
abs (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:]
abs f is ext-real V36() real Element of REAL
(abs f) (#) (abs (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:]
abs (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 ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V50() V56() V57() V58() V59() V60() V61() V62() Element of NAT
(abs (seq_id (f * tseq))) . m is ext-real V36() real Element of REAL
(seq_id (f * tseq)) . m is ext-real V36() real Element of REAL
abs ((seq_id (f * tseq)) . m) is ext-real V36() real Element of REAL
m is ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V50() V56() V57() V58() V59() V60() V61() V62() Element of NAT
(abs (seq_id (f * tseq))) . m is ext-real V36() real Element of REAL
((abs f) (#) (abs (seq_id tseq))) . m is ext-real V36() real Element of REAL
(seq_id (f * tseq)) . m is ext-real V36() real Element of REAL
abs ((seq_id (f * tseq)) . m) is ext-real V36() 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 (#) (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 (#) (seq_id tseq))) . m is ext-real V36() real Element of REAL
abs ((seq_id (f (#) (seq_id tseq))) . m) is ext-real V36() real Element of REAL
(f (#) (seq_id tseq)) . m is ext-real V36() real Element of REAL
abs ((f (#) (seq_id tseq)) . m) is ext-real V36() real Element of REAL
abs (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:]
(abs (f (#) (seq_id tseq))) . m is ext-real V36() real Element of REAL
Zero_ ((),Linear_Space_of_RealSequences) is Element of ()
Add_ ((),Linear_Space_of_RealSequences) is Relation-like [:(),():] -defined () -valued Function-like V14([:(),():]) V18([:(),():],()) Element of bool [:[:(),():],():]
[:(),():] is set
[:[:(),():],():] is set
bool [:[:(),():],():] is set
Mult_ ((),Linear_Space_of_RealSequences) is Relation-like [:REAL,():] -defined () -valued Function-like V14([:REAL,():]) V18([:REAL,():],()) Element of bool [:[:REAL,():],():]
[:REAL,():] is set
[:[:REAL,():],():] is set
bool [:[:REAL,():],():] is set
RLSStruct(# (),(Zero_ ((),Linear_Space_of_RealSequences)),(Add_ ((),Linear_Space_of_RealSequences)),(Mult_ ((),Linear_Space_of_RealSequences)) #) is non empty strict RLSStruct
[:(),REAL:] is V38() V39() V40() set
bool [:(),REAL:] is set
vseq is set
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:]
abs (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 (abs (seq_id vseq)) is ext-real V36() 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 ext-real V36() real Element of REAL
f . tseq is ext-real V36() 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:]
abs (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 (abs (seq_id tseq)) is ext-real V36() 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 set
[:[:vseq,vseq:],vseq:] is set
bool [:[:vseq,vseq:],vseq:] is set
[:REAL,vseq:] is set
[:[:REAL,vseq:],vseq:] is set
bool [:[:REAL,vseq:],vseq:] is set
[:vseq,REAL:] is V38() V39() V40() set
bool [:vseq,REAL:] is set
f is Element of vseq
tseq is Relation-like [:vseq,vseq:] -defined vseq -valued Function-like V14([:vseq,vseq:]) V18([:vseq,vseq:],vseq) Element of bool [:[:vseq,vseq:],vseq:]
tv is Relation-like [:REAL,vseq:] -defined vseq -valued Function-like V14([:REAL,vseq:]) V18([:REAL,vseq:],vseq) Element of bool [:[:REAL,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:]
NORMSTR(# vseq,f,tseq,tv,e #) is strict NORMSTR
vseq is NORMSTR
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 set
the Mult of vseq is Relation-like [:REAL, the carrier of vseq:] -defined the carrier of vseq -valued Function-like V18([:REAL, the carrier of vseq:], the carrier of vseq) Element of bool [:[:REAL, the carrier of vseq:], the carrier of vseq:]
[:REAL, the carrier of vseq:] is set
[:[:REAL, the carrier of vseq:], the carrier of vseq:] is set
bool [:[:REAL, the carrier of vseq:], the carrier of vseq:] is set
RLSStruct(# the carrier of vseq, the ZeroF of vseq, the addF of vseq, the Mult of vseq #) is strict RLSStruct
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:]
abs 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 (abs vseq) is ext-real V36() real Element of REAL
f is ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V50() V56() V57() V58() V59() V60() V61() V62() Element of NAT
(abs vseq) . f is ext-real V36() real Element of REAL
vseq . f is ext-real V36() real Element of REAL
abs (vseq . f) is ext-real V36() real Element of REAL
Partial_Sums (abs 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 ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V50() V56() V57() V58() V59() V60() V61() V62() Element of NAT
(Partial_Sums (abs vseq)) . f is ext-real V36() real Element of REAL
tseq is ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V50() V56() V57() V58() V59() V60() V61() V62() Element of NAT
(abs vseq) . tseq is ext-real V36() real Element of REAL
(Partial_Sums (abs vseq)) . tseq is ext-real V36() real Element of REAL
tseq + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V50() V56() V57() V58() V59() V60() V61() V62() Element of NAT
(abs vseq) . (tseq + 1) is ext-real V36() real Element of REAL
(Partial_Sums (abs vseq)) . (tseq + 1) is ext-real V36() real Element of REAL
0 + ((abs vseq) . (tseq + 1)) is ext-real V36() real Element of REAL
((abs vseq) . tseq) + ((abs vseq) . (tseq + 1)) is ext-real V36() real Element of REAL
(abs vseq) . 0 is ext-real V36() real Element of REAL
(Partial_Sums (abs vseq)) . 0 is ext-real V36() real Element of REAL
(abs vseq) . f is ext-real V36() real Element of REAL
f is ext-real V36() real set
tseq is ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V50() V56() V57() V58() V59() V60() V61() V62() Element of NAT
(Partial_Sums (abs vseq)) . tseq is ext-real V36() real Element of REAL
((Partial_Sums (abs vseq)) . tseq) - 0 is ext-real V36() real Element of REAL
abs (((Partial_Sums (abs vseq)) . tseq) - 0) is ext-real V36() real Element of REAL
0 - 0 is ext-real V36() real Element of REAL
abs (0 - 0) is ext-real V36() real Element of REAL
lim (Partial_Sums (abs vseq)) is ext-real V36() real Element of REAL
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:]
abs 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 (abs vseq) is ext-real V36() real Element of REAL
tseq is ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V50() V56() V57() V58() V59() V60() V61() V62() Element of NAT
(abs vseq) . tseq is ext-real V36() real Element of REAL
vseq . tseq is ext-real V36() real Element of REAL
abs (vseq . tseq) is ext-real V36() 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 ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V50() V56() V57() V58() V59() V60() V61() V62() Element of NAT
vseq . tseq is ext-real V36() real Element of REAL
(abs vseq) . tseq is ext-real V36() real Element of REAL
abs (vseq . tseq) is ext-real V36() real Element of REAL
tseq is ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V50() V56() V57() V58() V59() V60() V61() V62() Element of NAT
vseq . tseq is ext-real V36() real Element of REAL
NORMSTR(# (),(Zero_ ((),Linear_Space_of_RealSequences)),(Add_ ((),Linear_Space_of_RealSequences)),(Mult_ ((),Linear_Space_of_RealSequences)),() #) is non empty strict NORMSTR
() is non empty NORMSTR
the carrier of () is non empty set
0. () is V84(()) 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 REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
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 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 set
[:[: the carrier of (), the carrier of ():], the carrier of ():] is set
bool [:[: the carrier of (), the carrier of ():], the carrier of ():] is 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 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 REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,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:]
the addF of Linear_Space_of_RealSequences is Relation-like [: the carrier of Linear_Space_of_RealSequences, the carrier of Linear_Space_of_RealSequences:] -defined the carrier of Linear_Space_of_RealSequences -valued Function-like V14([: the carrier of Linear_Space_of_RealSequences, the carrier of Linear_Space_of_RealSequences:]) V18([: the carrier of Linear_Space_of_RealSequences, the carrier of Linear_Space_of_RealSequences:], the carrier of Linear_Space_of_RealSequences) Element of bool [:[: the carrier of Linear_Space_of_RealSequences, the carrier of Linear_Space_of_RealSequences:], the carrier of Linear_Space_of_RealSequences:]
[: the carrier of Linear_Space_of_RealSequences, the carrier of Linear_Space_of_RealSequences:] is set
[:[: the carrier of Linear_Space_of_RealSequences, the carrier of Linear_Space_of_RealSequences:], the carrier of Linear_Space_of_RealSequences:] is set
bool [:[: the carrier of Linear_Space_of_RealSequences, the carrier of Linear_Space_of_RealSequences:], the carrier of Linear_Space_of_RealSequences:] is set
dom the addF of Linear_Space_of_RealSequences is Relation-like set
the addF of Linear_Space_of_RealSequences || () is Relation-like Function-like set
the addF of Linear_Space_of_RealSequences | [:(),():] is Relation-like set
dom ( the addF of Linear_Space_of_RealSequences || ()) is set
( the addF of Linear_Space_of_RealSequences || ()) . [f,tseq] is set
tv is Element of the carrier of Linear_Space_of_RealSequences
e is Element of the carrier of Linear_Space_of_RealSequences
tv + e is Element of the carrier of Linear_Space_of_RealSequences
the addF of Linear_Space_of_RealSequences . (tv,e) is Element of the carrier of Linear_Space_of_RealSequences
[tv,e] is set
the addF of Linear_Space_of_RealSequences . [tv,e] is set
f is ext-real V36() real Element of REAL
tseq is Element of the carrier of ()
f * tseq is Element of the carrier of ()
the Mult of () is Relation-like [:REAL, the carrier of ():] -defined the carrier of () -valued Function-like V14([:REAL, the carrier of ():]) V18([:REAL, the carrier of ():], the carrier of ()) Element of bool [:[:REAL, the carrier of ():], the carrier of ():]
[:REAL, the carrier of ():] is set
[:[:REAL, the carrier of ():], the carrier of ():] is set
bool [:[:REAL, the carrier of ():], the carrier of ():] is set
the Mult of () . (f,tseq) is set
[f,tseq] is set
the Mult of () . [f,tseq] is set
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) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
the Mult of Linear_Space_of_RealSequences is Relation-like [:REAL, the carrier of Linear_Space_of_RealSequences:] -defined the carrier of Linear_Space_of_RealSequences -valued Function-like V14([:REAL, the carrier of Linear_Space_of_RealSequences:]) V18([:REAL, the carrier of Linear_Space_of_RealSequences:], the carrier of Linear_Space_of_RealSequences) Element of bool [:[:REAL, the carrier of Linear_Space_of_RealSequences:], the carrier of Linear_Space_of_RealSequences:]
[:REAL, the carrier of Linear_Space_of_RealSequences:] is set
[:[:REAL, the carrier of Linear_Space_of_RealSequences:], the carrier of Linear_Space_of_RealSequences:] is set
bool [:[:REAL, the carrier of Linear_Space_of_RealSequences:], the carrier of Linear_Space_of_RealSequences:] is set
dom the Mult of Linear_Space_of_RealSequences is Relation-like set
the Mult of Linear_Space_of_RealSequences | [:REAL,():] is Relation-like [:REAL, the carrier of Linear_Space_of_RealSequences:] -defined the carrier of Linear_Space_of_RealSequences -valued Function-like Element of bool [:[:REAL, the carrier of Linear_Space_of_RealSequences:], the carrier of Linear_Space_of_RealSequences:]
dom ( the Mult of Linear_Space_of_RealSequences | [:REAL,():]) is Relation-like set
( the Mult of Linear_Space_of_RealSequences | [:REAL,():]) . [f,tseq] is set
tv is Element of the carrier of Linear_Space_of_RealSequences
f * tv is Element of the carrier of Linear_Space_of_RealSequences
the Mult of Linear_Space_of_RealSequences . (f,tv) is set
[f,tv] is set
the Mult of Linear_Space_of_RealSequences . [f,tv] is set
f is Element of the carrier of ()
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:]
f is Element of the carrier of ()
- f is Element of the carrier of ()
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 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 (- 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:]
(- 1) * f is Element of the carrier of ()
the Mult of () is Relation-like [:REAL, the carrier of ():] -defined the carrier of () -valued Function-like V14([:REAL, the carrier of ():]) V18([:REAL, the carrier of ():], the carrier of ()) Element of bool [:[:REAL, the carrier of ():], the carrier of ():]
[:REAL, the carrier of ():] is set
[:[:REAL, the carrier of ():], the carrier of ():] is set
bool [:[:REAL, the carrier of ():], the carrier of ():] is set
the Mult of () . ((- 1),f) is set
[(- 1),f] is set
the Mult of () . [(- 1),f] is set
(- 1) (#) (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:]
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 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 set
[:[: the carrier of (), the carrier of ():], the carrier of ():] is set
bool [:[: the carrier of (), the carrier of ():], the carrier of ():] is 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 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 REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,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:]
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) + (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 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) + (- (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 Element of the carrier of ()
||.f.|| is ext-real V36() 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 V38() V39() V40() set
bool [: the carrier of (),REAL:] is set
the normF of () . f is ext-real V36() 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:]
abs (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 (abs (seq_id f)) is ext-real V36() real Element of REAL
0. Linear_Space_of_RealSequences is V84( Linear_Space_of_RealSequences ) Element of the carrier of Linear_Space_of_RealSequences
the ZeroF of Linear_Space_of_RealSequences is Element of the carrier of Linear_Space_of_RealSequences
f is set
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:]
tseq is set
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:]
tv is Element of the carrier of ()
seq_id tv 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 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 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 set
[:[: the carrier of (), the carrier of ():], the carrier of ():] is set
bool [:[: the carrier of (), the carrier of ():], the carrier of ():] is 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 REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
seq_id 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:]
(seq_id e) + (seq_id 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 Element of the carrier of ()
u is ext-real V36() real Element of REAL
u * n is Element of the carrier of ()
the Mult of () is Relation-like [:REAL, the carrier of ():] -defined the carrier of () -valued Function-like V14([:REAL, the carrier of ():]) V18([:REAL, the carrier of ():], the carrier of ()) Element of bool [:[:REAL, the carrier of ():], the carrier of ():]
[:REAL, the carrier of ():] is set
[:[:REAL, the carrier of ():], the carrier of ():] is set
bool [:[:REAL, the carrier of ():], the carrier of ():] is set
the Mult of () . (u,n) is set
[u,n] is set
the Mult of () . [u,n] is set
seq_id 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:]
u (#) (seq_id 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:]
v is Element of the carrier of ()
- v is Element of the carrier of ()
seq_id 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:]
- (seq_id 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 Element of the carrier of ()
- m is Element of the carrier of ()
seq_id (- 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:]
seq_id 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:]
- (seq_id 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:]
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 REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
seq_id 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:]
(seq_id rseq) - (seq_id 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:]
c₁₃ is Element of the carrier of ()
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:]
c₁₄ is Element of the carrier of ()
||.c₁₄.|| is ext-real V36() 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 V38() V39() V40() set
bool [: the carrier of (),REAL:] is set
the normF of () . c₁₄ is ext-real V36() real Element of REAL
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:]
abs (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 (abs (seq_id c₁₄)) is ext-real V36() real Element of REAL
vseq is Element of the carrier of ()
||.vseq.|| is ext-real V36() 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 V38() V39() V40() set
bool [: the carrier of (),REAL:] is set
the normF of () . vseq is ext-real V36() 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 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 set
[:[: the carrier of (), the carrier of ():], the carrier of ():] is set
bool [:[: the carrier of (), the carrier of ():], the carrier of ():] is 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 ext-real V36() real Element of REAL
the normF of () . (vseq + f) is ext-real V36() real Element of REAL
||.f.|| is ext-real V36() real Element of REAL
the normF of () . f is ext-real V36() real Element of REAL
||.vseq.|| + ||.f.|| is ext-real V36() real Element of REAL
tseq is ext-real V36() real Element of REAL
tseq * vseq is Element of the carrier of ()
the Mult of () is Relation-like [:REAL, the carrier of ():] -defined the carrier of () -valued Function-like V14([:REAL, the carrier of ():]) V18([:REAL, the carrier of ():], the carrier of ()) Element of bool [:[:REAL, the carrier of ():], the carrier of ():]
[:REAL, the carrier of ():] is set
[:[:REAL, the carrier of ():], the carrier of ():] is set
bool [:[:REAL, the carrier of ():], the carrier of ():] is set
the Mult of () . (tseq,vseq) is set
[tseq,vseq] is set
the Mult of () . [tseq,vseq] is set
||.(tseq * vseq).|| is ext-real V36() real Element of REAL
the normF of () . (tseq * vseq) is ext-real V36() real Element of REAL
abs tseq is ext-real V36() real Element of REAL
(abs tseq) * ||.vseq.|| is ext-real V36() real Element of REAL
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:]
abs (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 ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V50() V56() V57() V58() V59() V60() V61() V62() Element of NAT
(abs (seq_id vseq)) . tv is ext-real V36() real Element of REAL
(seq_id vseq) . tv is ext-real V36() real Element of REAL
abs ((seq_id vseq) . tv) is ext-real V36() real Element of REAL
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:]
abs (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 ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V50() V56() V57() V58() V59() V60() V61() V62() Element of NAT
(abs (seq_id (vseq + f))) . tv is ext-real V36() real Element of REAL
(seq_id (vseq + f)) . tv is ext-real V36() real Element of REAL
abs ((seq_id (vseq + f)) . tv) is ext-real V36() 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 ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V50() V56() V57() V58() V59() V60() V61() V62() Element of NAT
(abs (seq_id (vseq + f))) . tv is ext-real V36() real Element of REAL
(seq_id vseq) . tv is ext-real V36() real Element of REAL
(seq_id f) . tv is ext-real V36() real Element of REAL
((seq_id vseq) . tv) + ((seq_id f) . tv) is ext-real V36() real Element of REAL
abs (((seq_id vseq) . tv) + ((seq_id f) . tv)) is ext-real V36() 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 ((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:]
abs (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:]
(abs (seq_id ((seq_id vseq) + (seq_id f)))) . tv is ext-real V36() real Element of REAL
abs ((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:]
(abs ((seq_id vseq) + (seq_id f))) . tv is ext-real V36() real Element of REAL
((seq_id vseq) + (seq_id f)) . tv is ext-real V36() real Element of REAL
abs (((seq_id vseq) + (seq_id f)) . tv) is ext-real V36() real Element of REAL
abs (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 ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V50() V56() V57() V58() V59() V60() V61() V62() Element of NAT
(abs (seq_id (vseq + f))) . tv is ext-real V36() real Element of REAL
(abs (seq_id vseq)) . tv is ext-real V36() real Element of REAL
(abs (seq_id f)) . tv is ext-real V36() real Element of REAL
((abs (seq_id vseq)) . tv) + ((abs (seq_id f)) . tv) is ext-real V36() real Element of REAL
(seq_id vseq) . tv is ext-real V36() real Element of REAL
(seq_id f) . tv is ext-real V36() real Element of REAL
((seq_id vseq) . tv) + ((seq_id f) . tv) is ext-real V36() real Element of REAL
abs (((seq_id vseq) . tv) + ((seq_id f) . tv)) is ext-real V36() real Element of REAL
abs ((seq_id vseq) . tv) is ext-real V36() real Element of REAL
abs ((seq_id f) . tv) is ext-real V36() real Element of REAL
(abs ((seq_id vseq) . tv)) + (abs ((seq_id f) . tv)) is ext-real V36() real Element of REAL
((abs (seq_id vseq)) . tv) + (abs ((seq_id f) . tv)) is ext-real V36() real Element of REAL
(abs (seq_id vseq)) + (abs (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 ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V50() V56() V57() V58() V59() V60() V61() V62() Element of NAT
(abs (seq_id (vseq + f))) . tv is ext-real V36() real Element of REAL
((abs (seq_id vseq)) + (abs (seq_id f))) . tv is ext-real V36() real Element of REAL
(abs (seq_id vseq)) . tv is ext-real V36() real Element of REAL
(abs (seq_id f)) . tv is ext-real V36() real Element of REAL
((abs (seq_id vseq)) . tv) + ((abs (seq_id f)) . tv) is ext-real V36() real Element of REAL
Sum (abs (seq_id (vseq + f))) is ext-real V36() real Element of REAL
Sum ((abs (seq_id vseq)) + (abs (seq_id f))) is ext-real V36() real Element of REAL
tv is ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V50() V56() V57() V58() V59() V60() V61() V62() Element of NAT
(seq_id vseq) . tv is ext-real V36() real Element of REAL
the normF of () . vseq is ext-real V36() real Element of REAL
Sum (abs (seq_id vseq)) is ext-real V36() real Element of REAL
tv is ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V50() V56() V57() V58() V59() V60() V61() V62() Element of NAT
(seq_id vseq) . tv is ext-real V36() real Element of REAL
Sum (abs (seq_id f)) is ext-real V36() 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:]
abs (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 ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V50() V56() V57() V58() V59() V60() V61() V62() Element of NAT
(abs (tseq (#) (seq_id vseq))) . tv is ext-real V36() real Element of REAL
(abs (seq_id vseq)) . tv is ext-real V36() real Element of REAL
(abs tseq) * ((abs (seq_id vseq)) . tv) is ext-real V36() real Element of REAL
(tseq (#) (seq_id vseq)) . tv is ext-real V36() real Element of REAL
abs ((tseq (#) (seq_id vseq)) . tv) is ext-real V36() real Element of REAL
(seq_id vseq) . tv is ext-real V36() real Element of REAL
tseq * ((seq_id vseq) . tv) is ext-real V36() real Element of REAL
abs (tseq * ((seq_id vseq) . tv)) is ext-real V36() real Element of REAL
abs ((seq_id vseq) . tv) is ext-real V36() real Element of REAL
(abs tseq) * (abs ((seq_id vseq) . tv)) is ext-real V36() real Element of REAL
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:]
abs (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 (abs (seq_id (tseq * vseq))) is ext-real V36() real Element of REAL
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:]
abs (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 (abs (seq_id (tseq (#) (seq_id vseq)))) is ext-real V36() real Element of REAL
Sum (abs (tseq (#) (seq_id vseq))) is ext-real V36() real Element of REAL
(abs tseq) (#) (abs (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 ((abs tseq) (#) (abs (seq_id vseq))) is ext-real V36() real Element of REAL
(abs tseq) * (Sum (abs (seq_id vseq))) is ext-real V36() real Element of REAL
||.(0. ()).|| is ext-real V36() 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 V38() V39() V40() set
bool [: the carrier of (),REAL:] is set
the normF of () . (0. ()) is ext-real V36() real Element of REAL
vseq is ext-real V36() 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 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 is ext-real V36() real Element of REAL
(lim f) - vseq is ext-real V36() real Element of REAL
abs ((lim f) - vseq) is ext-real V36() real Element of REAL
lim tseq is ext-real V36() real Element of REAL
(abs ((lim f) - vseq)) + (lim tseq) is ext-real V36() real Element of REAL
NAT --> vseq is Relation-like NAT -defined REAL -valued Function-like constant non empty V14( NAT ) V18( NAT , REAL ) V38() V39() V40() convergent Element of bool [:NAT,REAL:]
tv 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 - tv is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
abs (f - tv) 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 Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
lim e is ext-real V36() real Element of REAL
m is ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V50() V56() V57() V58() V59() V60() V61() V62() Element of NAT
e . m is ext-real V36() real Element of REAL
f . m is ext-real V36() real Element of REAL
(f . m) - vseq is ext-real V36() real Element of REAL
abs ((f . m) - vseq) is ext-real V36() real Element of REAL
tseq . m is ext-real V36() real Element of REAL
(abs ((f . m) - vseq)) + (tseq . m) is ext-real V36() real Element of REAL
tv . m is ext-real V36() real Element of REAL
(f . m) - (tv . m) is ext-real V36() real Element of REAL
abs ((f . m) - (tv . m)) is ext-real V36() real Element of REAL
(abs ((f . m) - (tv . m))) + (tseq . m) is ext-real V36() real Element of REAL
- (tv . m) is ext-real V36() real Element of REAL
(f . m) + (- (tv . m)) is ext-real V36() real Element of REAL
abs ((f . m) + (- (tv . m))) is ext-real V36() real Element of REAL
(abs ((f . m) + (- (tv . m)))) + (tseq . m) is ext-real V36() real Element of REAL
- tv 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) . m is ext-real V36() real Element of REAL
(f . m) + ((- tv) . m) is ext-real V36() real Element of REAL
abs ((f . m) + ((- tv) . m)) is ext-real V36() real Element of REAL
(abs ((f . m) + ((- tv) . m))) + (tseq . m) is ext-real V36() real Element of REAL
f + (- tv) 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 + (- tv)) . m is ext-real V36() real Element of REAL
abs ((f + (- tv)) . m) is ext-real V36() real Element of REAL
(abs ((f + (- tv)) . m)) + (tseq . m) is ext-real V36() real Element of REAL
(f - tv) . m is ext-real V36() real Element of REAL
abs ((f - tv) . m) is ext-real V36() real Element of REAL
(abs ((f - tv) . m)) + (tseq . m) is ext-real V36() real Element of REAL
(abs (f - tv)) . m is ext-real V36() real Element of REAL
((abs (f - tv)) . m) + (tseq . m) is ext-real V36() real Element of REAL
(abs (f - tv)) + 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:]
((abs (f - tv)) + tseq) . m is ext-real V36() real Element of REAL
lim (abs (f - tv)) is ext-real V36() real Element of REAL
lim (f - tv) is ext-real V36() real Element of REAL
abs (lim (f - tv)) is ext-real V36() real Element of REAL
lim tv is ext-real V36() real Element of REAL
(lim f) - (lim tv) is ext-real V36() real Element of REAL
abs ((lim f) - (lim tv)) is ext-real V36() real Element of REAL
tv . 0 is ext-real V36() real Element of REAL
(lim f) - (tv . 0) is ext-real V36() real Element of REAL
abs ((lim f) - (tv . 0)) is ext-real V36() real Element of REAL
vseq is non empty NORMSTR
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 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 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 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 ext-real V36() 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 V38() V39() V40() set
bool [: the carrier of vseq,REAL:] is set
the normF of vseq . (f - tseq) is ext-real V36() real Element of REAL
vseq is non empty NORMSTR
the carrier of vseq is non empty set
[:NAT, the carrier of vseq:] is set
bool [:NAT, the carrier of vseq:] is set
vseq is non empty NORMSTR
the carrier of vseq is non empty set
[:NAT, the carrier of vseq:] is set
bool [:NAT, the carrier of vseq:] is set
vseq is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() discerning reflexive RealNormSpace-like NORMSTR
the carrier of vseq is non empty set
[:NAT, the carrier of vseq:] is set
bool [:NAT, the carrier of vseq:] is 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 ext-real V36() real Element of REAL
tv is ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V50() V56() V57() V58() V59() V60() V61() V62() Element of NAT
e is ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V50() V56() V57() V58() V59() V60() V61() V62() Element of NAT
m is ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V50() V56() V57() V58() V59() V60() V61() V62() 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 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 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 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 ext-real non negative V36() 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 V38() V39() V40() set
bool [: the carrier of vseq,REAL:] is set
the normF of vseq . ((f . e) - (f . m)) is ext-real V36() real Element of REAL
(vseq,(f . e),(f . m)) is ext-real V36() real Element of REAL
tseq is ext-real V36() real Element of REAL
tv is ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V50() V56() V57() V58() V59() V60() V61() V62() Element of NAT
e is ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V50() V56() V57() V58() V59() V60() V61() V62() Element of NAT
m is ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V50() V56() V57() V58() V59() V60() V61() V62() 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 ext-real V36() 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 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 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 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 ext-real non negative V36() 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 V38() V39() V40() set
bool [: the carrier of vseq,REAL:] is set
the normF of vseq . ((f . e) - (f . m)) is ext-real V36() real Element of REAL
tv is ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V50() V56() V57() V58() V59() V60() V61() V62() Element of NAT
[:NAT, the carrier of ():] is set
bool [:NAT, the carrier of ():] is 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 ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V50() V56() V57() V58() V59() V60() V61() V62() Element of NAT
tv 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 tv is ext-real V36() real Element of REAL
e is ext-real V36() real set
m is ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V50() V56() V57() V58() V59() V60() V61() V62() Element of NAT
tv . m is ext-real V36() real Element of REAL
u is ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V50() V56() V57() V58() V59() V60() V61() V62() Element of NAT
tv . u is ext-real V36() real Element of REAL
(tv . u) - (tv . m) is ext-real V36() real Element of REAL
abs ((tv . u) - (tv . m)) is ext-real V36() 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 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 set
[:[: the carrier of (), the carrier of ():], the carrier of ():] is set
bool [:[: the carrier of (), the carrier of ():], the carrier of ():] is 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 REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
abs (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 ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V50() V56() V57() V58() V59() V60() V61() V62() Element of NAT
(abs (seq_id ((vseq . u) - (vseq . m)))) . n is ext-real V36() real Element of REAL
(seq_id ((vseq . u) - (vseq . m))) . n is ext-real V36() real Element of REAL
abs ((seq_id ((vseq . u) - (vseq . m))) . n) is ext-real V36() real Element of REAL
(abs (seq_id ((vseq . u) - (vseq . m)))) . tseq is ext-real V36() real Element of REAL
Sum (abs (seq_id ((vseq . u) - (vseq . m)))) is ext-real V36() real Element of REAL
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) 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 . u)) - (seq_id (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:]
seq_id ((seq_id (vseq . u)) - (seq_id (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:]
- (seq_id (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:]
(seq_id (vseq . u)) + (- (seq_id (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:]
(seq_id ((vseq . u) - (vseq . m))) . tseq is ext-real V36() real Element of REAL
(seq_id (vseq . u)) . tseq is ext-real V36() real Element of REAL
(- (seq_id (vseq . m))) . tseq is ext-real V36() real Element of REAL
((seq_id (vseq . u)) . tseq) + ((- (seq_id (vseq . m))) . tseq) is ext-real V36() real Element of REAL
(seq_id (vseq . m)) . tseq is ext-real V36() real Element of REAL
- ((seq_id (vseq . m)) . tseq) is ext-real V36() real Element of REAL
((seq_id (vseq . u)) . tseq) + (- ((seq_id (vseq . m)) . tseq)) is ext-real V36() real Element of REAL
((seq_id (vseq . u)) . tseq) - ((seq_id (vseq . m)) . tseq) is ext-real V36() real Element of REAL
(tv . u) - ((seq_id (vseq . m)) . tseq) is ext-real V36() real Element of REAL
||.((vseq . u) - (vseq . m)).|| is ext-real non negative V36() 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 V38() V39() V40() set
bool [: the carrier of (),REAL:] is set
the normF of () . ((vseq . u) - (vseq . m)) is ext-real V36() 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:]
tv is ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V50() V56() V57() V58() V59() V60() V61() V62() Element of NAT
e is set
f . e is ext-real V36() 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:]
tseq . tv is ext-real V36() real Element of REAL
m is ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V50() V56() V57() V58() V59() V60() V61() V62() Element of NAT
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:]
lim u is ext-real V36() 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:]
tv is ext-real V36() real Element of REAL
tv / 2 is ext-real V36() real Element of REAL
m is ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V50() V56() V57() V58() V59() V60() V61() V62() Element of NAT
n is ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V50() V56() V57() V58() V59() V60() V61() V62() Element of NAT
u is ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V50() V56() V57() V58() V59() V60() V61() V62() 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 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 set
[:[: the carrier of (), the carrier of ():], the carrier of ():] is set
bool [:[: the carrier of (), the carrier of ():], the carrier of ():] is 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 REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
abs (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 (abs (seq_id ((vseq . n) - (vseq . u)))) is ext-real V36() real Element of REAL
||.((vseq . n) - (vseq . u)).|| is ext-real non negative V36() 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 V38() V39() V40() set
bool [: the carrier of (),REAL:] is set
the normF of () . ((vseq . n) - (vseq . u)) is ext-real V36() real Element of REAL
the normF of () . ((vseq . n) - (vseq . u)) is ext-real V36() real Element of REAL
v is ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V50() V56() V57() V58() V59() V60() V61() V62() Element of NAT
(abs (seq_id ((vseq . n) - (vseq . u)))) . v is ext-real V36() real Element of REAL
(seq_id ((vseq . n) - (vseq . u))) . v is ext-real V36() real Element of REAL
abs ((seq_id ((vseq . n) - (vseq . u))) . v) is ext-real V36() real Element of REAL
v is ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V50() V56() V57() V58() V59() V60() V61() V62() Element of NAT
(abs (seq_id ((vseq . n) - (vseq . u)))) . v is ext-real V36() real Element of REAL
u is ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V50() V56() V57() V58() V59() V60() V61() V62() Element of NAT
vseq . u is Element of the carrier of ()
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 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:]
abs ((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 (abs ((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 ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V50() V56() V57() V58() V59() V60() V61() V62() Element of NAT
vseq . n is Element of the carrier of ()
v is ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V50() V56() V57() V58() V59() V60() V61() V62() 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 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 set
[:[: the carrier of (), the carrier of ():], the carrier of ():] is set
bool [:[: the carrier of (), the carrier of ():], the carrier of ():] is 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 REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
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:]
seq_id (vseq . 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:]
(seq_id (vseq . n)) - (seq_id (vseq . 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:]
seq_id ((seq_id (vseq . n)) - (seq_id (vseq . 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 ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V50() V56() V57() V58() V59() V60() V61() V62() Element of NAT
(Partial_Sums (abs ((seq_id tseq) - (seq_id (vseq . u))))) . n is ext-real V36() real Element of REAL
n + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V50() V56() V57() V58() V59() V60() V61() V62() Element of NAT
(Partial_Sums (abs ((seq_id tseq) - (seq_id (vseq . u))))) . (n + 1) is ext-real V36() 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 ext-real V36() 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 ext-real V36() real Element of REAL
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 ext-real V36() real Element of REAL
m is ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V50() V56() V57() V58() V59() V60() V61() V62() Element of NAT
rseq . m is ext-real V36() 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 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 set
[:[: the carrier of (), the carrier of ():], the carrier of ():] is set
bool [:[: the carrier of (), the carrier of ():], the carrier of ():] is 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 REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
abs (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 (abs (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 (abs (seq_id ((vseq . m) - (vseq . u))))) . (n + 1) is ext-real V36() real Element of REAL
(abs (seq_id ((vseq . m) - (vseq . u)))) . (n + 1) is ext-real V36() real Element of REAL
(Partial_Sums (abs (seq_id ((vseq . m) - (vseq . u))))) . n is ext-real V36() real Element of REAL
((abs (seq_id ((vseq . m) - (vseq . u)))) . (n + 1)) + ((Partial_Sums (abs (seq_id ((vseq . m) - (vseq . u))))) . n) is ext-real V36() real Element of REAL
seq_id (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:]
(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:]
abs ((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:]
(abs ((seq_id (vseq . m)) - (seq_id (vseq . u)))) . (n + 1) is ext-real V36() real Element of REAL
((abs ((seq_id (vseq . m)) - (seq_id (vseq . u)))) . (n + 1)) + ((Partial_Sums (abs (seq_id ((vseq . m) - (vseq . u))))) . n) is ext-real V36() real Element of REAL
v . m is ext-real V36() real Element of REAL
((abs ((seq_id (vseq . m)) - (seq_id (vseq . u)))) . (n + 1)) + (v . m) is ext-real V36() real Element of REAL
((seq_id (vseq . m)) - (seq_id (vseq . u))) . (n + 1) is ext-real V36() real Element of REAL
abs (((seq_id (vseq . m)) - (seq_id (vseq . u))) . (n + 1)) is ext-real V36() real Element of REAL
(abs (((seq_id (vseq . m)) - (seq_id (vseq . u))) . (n + 1))) + (v . m) is ext-real V36() real Element of REAL
- (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))) 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 ext-real V36() real Element of REAL
abs (((seq_id (vseq . m)) + (- (seq_id (vseq . u)))) . (n + 1)) is ext-real V36() real Element of REAL
(abs (((seq_id (vseq . m)) + (- (seq_id (vseq . u)))) . (n + 1))) + (v . m) is ext-real V36() real Element of REAL
(seq_id (vseq . m)) . (n + 1) is ext-real V36() real Element of REAL
(- (seq_id (vseq . u))) . (n + 1) is ext-real V36() real Element of REAL
((seq_id (vseq . m)) . (n + 1)) + ((- (seq_id (vseq . u))) . (n + 1)) is ext-real V36() real Element of REAL
abs (((seq_id (vseq . m)) . (n + 1)) + ((- (seq_id (vseq . u))) . (n + 1))) is ext-real V36() real Element of REAL
(abs (((seq_id (vseq . m)) . (n + 1)) + ((- (seq_id (vseq . u))) . (n + 1)))) + (v . m) is ext-real V36() real Element of REAL
(seq_id (vseq . u)) . (n + 1) is ext-real V36() real Element of REAL
- ((seq_id (vseq . u)) . (n + 1)) is ext-real V36() real Element of REAL
((seq_id (vseq . m)) . (n + 1)) + (- ((seq_id (vseq . u)) . (n + 1))) is ext-real V36() real Element of REAL
abs (((seq_id (vseq . m)) . (n + 1)) + (- ((seq_id (vseq . u)) . (n + 1)))) is ext-real V36() real Element of REAL
(abs (((seq_id (vseq . m)) . (n + 1)) + (- ((seq_id (vseq . u)) . (n + 1))))) + (v . m) is ext-real V36() real Element of REAL
((seq_id (vseq . m)) . (n + 1)) - ((seq_id (vseq . u)) . (n + 1)) is ext-real V36() real Element of REAL
abs (((seq_id (vseq . m)) . (n + 1)) - ((seq_id (vseq . u)) . (n + 1))) is ext-real V36() real Element of REAL
(abs (((seq_id (vseq . m)) . (n + 1)) - ((seq_id (vseq . u)) . (n + 1)))) + (v . m) is ext-real V36() real Element of REAL
m . m is ext-real V36() real Element of REAL
(m . m) - ((seq_id (vseq . u)) . (n + 1)) is ext-real V36() real Element of REAL
abs ((m . m) - ((seq_id (vseq . u)) . (n + 1))) is ext-real V36() real Element of REAL
(abs ((m . m) - ((seq_id (vseq . u)) . (n + 1)))) + (v . m) is ext-real V36() real Element of REAL
(lim m) - ((seq_id (vseq . u)) . (n + 1)) is ext-real V36() real Element of REAL
abs ((lim m) - ((seq_id (vseq . u)) . (n + 1))) is ext-real V36() real Element of REAL
lim v is ext-real V36() real Element of REAL
(abs ((lim m) - ((seq_id (vseq . u)) . (n + 1)))) + (lim v) is ext-real V36() real Element of REAL
(tseq . (n + 1)) + (- ((seq_id (vseq . u)) . (n + 1))) is ext-real V36() real Element of REAL
abs ((tseq . (n + 1)) + (- ((seq_id (vseq . u)) . (n + 1)))) is ext-real V36() real Element of REAL
(abs ((tseq . (n + 1)) + (- ((seq_id (vseq . u)) . (n + 1))))) + (lim v) is ext-real V36() real Element of REAL
(tseq . (n + 1)) + ((- (seq_id (vseq . u))) . (n + 1)) is ext-real V36() real Element of REAL
abs ((tseq . (n + 1)) + ((- (seq_id (vseq . u))) . (n + 1))) is ext-real V36() real Element of REAL
(abs ((tseq . (n + 1)) + ((- (seq_id (vseq . u))) . (n + 1)))) + (lim v) is ext-real V36() 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 ext-real V36() real Element of REAL
abs ((tseq + (- (seq_id (vseq . u)))) . (n + 1)) is ext-real V36() real Element of REAL
(abs ((tseq + (- (seq_id (vseq . u)))) . (n + 1))) + (lim v) is ext-real V36() 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 ext-real V36() real Element of REAL
abs ((tseq - (seq_id (vseq . u))) . (n + 1)) is ext-real V36() real Element of REAL
(abs ((tseq - (seq_id (vseq . u))) . (n + 1))) + (lim v) is ext-real V36() real Element of REAL
abs (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:]
(abs (tseq - (seq_id (vseq . u)))) . (n + 1) is ext-real V36() real Element of REAL
((abs (tseq - (seq_id (vseq . u)))) . (n + 1)) + (lim v) is ext-real V36() real Element of REAL
((abs (tseq - (seq_id (vseq . u)))) . (n + 1)) + ((Partial_Sums (abs ((seq_id tseq) - (seq_id (vseq . u))))) . n) is ext-real V36() real Element of REAL
(abs ((seq_id tseq) - (seq_id (vseq . u)))) . (n + 1) is ext-real V36() real Element of REAL
((abs ((seq_id tseq) - (seq_id (vseq . u)))) . (n + 1)) + ((Partial_Sums (abs ((seq_id tseq) - (seq_id (vseq . u))))) . n) is ext-real V36() real Element of REAL
n is ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V50() V56() V57() V58() V59() V60() V61() V62() Element of NAT
(Partial_Sums (abs ((seq_id tseq) - (seq_id (vseq . u))))) . n is ext-real V36() 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 ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V50() V56() V57() V58() V59() V60() V61() V62() Element of NAT
lim v is ext-real V36() real Element of REAL
(Partial_Sums (abs ((seq_id tseq) - (seq_id (vseq . u))))) . (n + 1) is ext-real V36() 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 ext-real V36() real Element of REAL
(Partial_Sums (abs ((seq_id tseq) - (seq_id (vseq . u))))) . 0 is ext-real V36() real Element of REAL
tseq . 0 is ext-real V36() 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:]
lim v is ext-real V36() real Element of REAL
(seq_id (vseq . u)) . 0 is ext-real V36() real Element of REAL
m is ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V50() V56() V57() V58() V59() V60() V61() V62() Element of NAT
n . m is ext-real V36() real Element of REAL
v . m is ext-real V36() real Element of REAL
(v . m) - ((seq_id (vseq . u)) . 0) is ext-real V36() real Element of REAL
abs ((v . m) - ((seq_id (vseq . u)) . 0)) is ext-real V36() 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 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 set
[:[: the carrier of (), the carrier of ():], the carrier of ():] is set
bool [:[: the carrier of (), the carrier of ():], the carrier of ():] is 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 REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
abs (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 (abs (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 (abs (seq_id ((vseq . m) - (vseq . u))))) . 0 is ext-real V36() real Element of REAL
(abs (seq_id ((vseq . m) - (vseq . u)))) . 0 is ext-real V36() real Element of REAL
seq_id (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:]
(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:]
abs ((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:]
(abs ((seq_id (vseq . m)) - (seq_id (vseq . u)))) . 0 is ext-real V36() real Element of REAL
- (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))) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
abs ((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:]
(abs ((seq_id (vseq . m)) + (- (seq_id (vseq . u))))) . 0 is ext-real V36() real Element of REAL
((seq_id (vseq . m)) + (- (seq_id (vseq . u)))) . 0 is ext-real V36() real Element of REAL
abs (((seq_id (vseq . m)) + (- (seq_id (vseq . u)))) . 0) is ext-real V36() real Element of REAL
(seq_id (vseq . m)) . 0 is ext-real V36() real Element of REAL
(- (seq_id (vseq . u))) . 0 is ext-real V36() real Element of REAL
((seq_id (vseq . m)) . 0) + ((- (seq_id (vseq . u))) . 0) is ext-real V36() real Element of REAL
abs (((seq_id (vseq . m)) . 0) + ((- (seq_id (vseq . u))) . 0)) is ext-real V36() real Element of REAL
- ((seq_id (vseq . u)) . 0) is ext-real V36() real Element of REAL
((seq_id (vseq . m)) . 0) + (- ((seq_id (vseq . u)) . 0)) is ext-real V36() real Element of REAL
abs (((seq_id (vseq . m)) . 0) + (- ((seq_id (vseq . u)) . 0))) is ext-real V36() real Element of REAL
((seq_id (vseq . m)) . 0) - ((seq_id (vseq . u)) . 0) is ext-real V36() real Element of REAL
abs (((seq_id (vseq . m)) . 0) - ((seq_id (vseq . u)) . 0)) is ext-real V36() real Element of REAL
(lim v) - ((seq_id (vseq . u)) . 0) is ext-real V36() real Element of REAL
abs ((lim v) - ((seq_id (vseq . u)) . 0)) is ext-real V36() real Element of REAL
- ((seq_id (vseq . u)) . 0) is ext-real V36() real Element of REAL
(tseq . 0) + (- ((seq_id (vseq . u)) . 0)) is ext-real V36() real Element of REAL
abs ((tseq . 0) + (- ((seq_id (vseq . u)) . 0))) is ext-real V36() real Element of REAL
- (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 . u))) . 0 is ext-real V36() real Element of REAL
(tseq . 0) + ((- (seq_id (vseq . u))) . 0) is ext-real V36() real Element of REAL
abs ((tseq . 0) + ((- (seq_id (vseq . u))) . 0)) is ext-real V36() 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)))) . 0 is ext-real V36() real Element of REAL
abs ((tseq + (- (seq_id (vseq . u)))) . 0) is ext-real V36() 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))) . 0 is ext-real V36() real Element of REAL
abs ((tseq - (seq_id (vseq . u))) . 0) is ext-real V36() real Element of REAL
((seq_id tseq) - (seq_id (vseq . u))) . 0 is ext-real V36() real Element of REAL
abs (((seq_id tseq) - (seq_id (vseq . u))) . 0) is ext-real V36() real Element of REAL
(abs ((seq_id tseq) - (seq_id (vseq . u)))) . 0 is ext-real V36() 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 ext-real V36() 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 ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V50() V56() V57() V58() V59() V60() V61() V62() Element of NAT
lim v is ext-real V36() real Element of REAL
(Partial_Sums (abs ((seq_id tseq) - (seq_id (vseq . u))))) . n is ext-real V36() real Element of REAL
u is ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V50() V56() V57() V58() V59() V60() V61() V62() Element of NAT
vseq . u is Element of the carrier of ()
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 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:]
abs ((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 (abs ((seq_id tseq) - (seq_id (vseq . u)))) is ext-real V36() real Element of REAL
Partial_Sums (abs ((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 ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V50() V56() V57() V58() V59() V60() V61() V62() Element of NAT
(Partial_Sums (abs ((seq_id tseq) - (seq_id (vseq . u))))) . n is ext-real V36() 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 ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V50() V56() V57() V58() V59() V60() V61() V62() Element of NAT
v . m is ext-real V36() 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 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 set
[:[: the carrier of (), the carrier of ():], the carrier of ():] is set
bool [:[: the carrier of (), the carrier of ():], the carrier of ():] is 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 REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
abs (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 (abs (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 (abs (seq_id ((vseq . m) - (vseq . u))))) . n is ext-real V36() real Element of REAL
rseq is ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V50() V56() V57() V58() V59() V60() V61() V62() Element of NAT
(abs (seq_id ((vseq . m) - (vseq . u)))) . rseq is ext-real V36() real Element of REAL
Sum (abs (seq_id ((vseq . m) - (vseq . u)))) is ext-real V36() real Element of REAL
lim v is ext-real V36() real Element of REAL
v is ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V50() V56() V57() V58() V59() V60() V61() V62() Element of NAT
(Partial_Sums (abs ((seq_id tseq) - (seq_id (vseq . u))))) . v is ext-real V36() real Element of REAL
n is ext-real V36() real Element of REAL
n is ext-real V36() real Element of REAL
n is ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V50() V56() V57() V58() V59() V60() V61() V62() Element of NAT
(abs ((seq_id tseq) - (seq_id (vseq . u)))) . n is ext-real V36() real Element of REAL
((seq_id tseq) - (seq_id (vseq . u))) . n is ext-real V36() real Element of REAL
abs (((seq_id tseq) - (seq_id (vseq . u))) . n) is ext-real V36() real Element of REAL
lim (Partial_Sums (abs ((seq_id tseq) - (seq_id (vseq . u))))) is ext-real V36() real Element of REAL
abs (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 ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V50() V56() V57() V58() V59() V60() V61() V62() Element of NAT
(abs (seq_id tseq)) . e is ext-real V36() real Element of REAL
(seq_id tseq) . e is ext-real V36() real Element of REAL
abs ((seq_id tseq) . e) is ext-real V36() real Element of REAL
e is ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V50() V56() V57() V58() V59() V60() V61() V62() Element of NAT
vseq . e is Element of the carrier of ()
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:]
abs (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 REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
abs ((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:]
(abs ((seq_id tseq) - (seq_id (vseq . e)))) + (abs (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 ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V50() V56() V57() V58() V59() V60() V61() V62() Element of NAT
(abs (seq_id tseq)) . n is ext-real V36() real Element of REAL
((abs ((seq_id tseq) - (seq_id (vseq . e)))) + (abs (seq_id (vseq . e)))) . n is ext-real V36() real Element of REAL
(abs (seq_id (vseq . e))) . n is ext-real V36() real Element of REAL
(seq_id (vseq . e)) . n is ext-real V36() real Element of REAL
abs ((seq_id (vseq . e)) . n) is ext-real V36() real Element of REAL
(seq_id tseq) . n is ext-real V36() real Element of REAL
abs ((seq_id tseq) . n) is ext-real V36() real Element of REAL
(abs ((seq_id tseq) - (seq_id (vseq . e)))) . n is ext-real V36() real Element of REAL
((seq_id tseq) - (seq_id (vseq . e))) . n is ext-real V36() real Element of REAL
abs (((seq_id tseq) - (seq_id (vseq . e))) . n) is ext-real V36() real Element of REAL
- (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 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)))) . n is ext-real V36() real Element of REAL
abs (((seq_id tseq) + (- (seq_id (vseq . e)))) . n) is ext-real V36() real Element of REAL
(- (seq_id (vseq . e))) . n is ext-real V36() real Element of REAL
((seq_id tseq) . n) + ((- (seq_id (vseq . e))) . n) is ext-real V36() real Element of REAL
abs (((seq_id tseq) . n) + ((- (seq_id (vseq . e))) . n)) is ext-real V36() real Element of REAL
- ((seq_id (vseq . e)) . n) is ext-real V36() real Element of REAL
((seq_id tseq) . n) + (- ((seq_id (vseq . e)) . n)) is ext-real V36() real Element of REAL
abs (((seq_id tseq) . n) + (- ((seq_id (vseq . e)) . n))) is ext-real V36() real Element of REAL
((seq_id tseq) . n) - ((seq_id (vseq . e)) . n) is ext-real V36() real Element of REAL
abs (((seq_id tseq) . n) - ((seq_id (vseq . e)) . n)) is ext-real V36() real Element of REAL
((abs (seq_id tseq)) . n) - ((abs (seq_id (vseq . e))) . n) is ext-real V36() real Element of REAL
(((abs (seq_id tseq)) . n) - ((abs (seq_id (vseq . e))) . n)) + ((abs (seq_id (vseq . e))) . n) is ext-real V36() real Element of REAL
((abs ((seq_id tseq) - (seq_id (vseq . e)))) . n) + ((abs (seq_id (vseq . e))) . n) is ext-real V36() real Element of REAL
tv is Element of the carrier of ()
e is ext-real V36() real Element of REAL
m is ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V50() V56() V57() V58() V59() V60() V61() V62() Element of NAT
n is ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V50() V56() V57() V58() V59() V60() V61() V62() Element of NAT
vseq . n is Element of the carrier of ()
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:]
(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:]
abs ((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 (abs ((seq_id tseq) - (seq_id (vseq . n)))) is ext-real V36() 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 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 set
[:[: the carrier of (), the carrier of ():], the carrier of ():] is set
bool [:[: the carrier of (), the carrier of ():], the carrier of ():] is 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 REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) V38() V39() V40() Element of bool [:NAT,REAL:]
abs (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 (abs (seq_id (u - v))) is ext-real V36() 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 V38() V39() V40() set
bool [: the carrier of (),REAL:] is set
the normF of () . (u - v) is ext-real V36() 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 ext-real non negative V36() real Element of REAL
the normF of () . ((vseq . n) - tv) is ext-real V36() 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 ext-real non negative V36() real Element of REAL
the normF of () . (- (tv - (vseq . n))) is ext-real V36() real Element of REAL
||.(tv - (vseq . n)).|| is ext-real non negative V36() real Element of REAL
the normF of () . (tv - (vseq . n)) is ext-real V36() real Element of REAL