:: RSSPACE2 semantic presentation

REAL is V11() V52() V58() V59() V60() V64() set
NAT is V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() Element of bool REAL
bool REAL is set
COMPLEX is V11() V52() V58() V64() set
RAT is V11() V52() V58() V59() V60() V61() V64() set
INT is V11() V52() V58() V59() V60() V61() V62() V64() set
[:NAT,REAL:] is V40() V41() V42() set
bool [:NAT,REAL:] is set
omega is V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() set
bool omega is set
bool NAT is set
the_set_of_RealSequences is V11() 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 V78() right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of Linear_Space_of_RealSequences is V11() set
bool the carrier of Linear_Space_of_RealSequences is set
the_set_of_l2RealSequences is V11() V137( Linear_Space_of_RealSequences ) 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 V40() V41() V42() set
bool [:[:the_set_of_l2RealSequences,the_set_of_l2RealSequences:],REAL:] is set
[:COMPLEX,COMPLEX:] is V40() set
bool [:COMPLEX,COMPLEX:] is set
[:[:COMPLEX,COMPLEX:],COMPLEX:] is V40() set
bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is set
[:REAL,REAL:] is V40() V41() V42() set
bool [:REAL,REAL:] is set
[:[:REAL,REAL:],REAL:] is V40() V41() V42() set
bool [:[:REAL,REAL:],REAL:] is set
[:RAT,RAT:] is RAT -valued V40() V41() V42() set
bool [:RAT,RAT:] is set
[:[:RAT,RAT:],RAT:] is RAT -valued V40() V41() V42() set
bool [:[:RAT,RAT:],RAT:] is set
[:INT,INT:] is RAT -valued INT -valued V40() V41() V42() set
bool [:INT,INT:] is set
[:[:INT,INT:],INT:] is RAT -valued INT -valued V40() V41() V42() set
bool [:[:INT,INT:],INT:] is set
[:NAT,NAT:] is RAT -valued INT -valued V40() V41() V42() V43() set
[:[:NAT,NAT:],NAT:] is RAT -valued INT -valued V40() V41() V42() V43() set
bool [:[:NAT,NAT:],NAT:] is set
0 is V11() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V33() real ext-real non positive non negative V58() V59() V60() V61() V62() V63() V64() set
1 is V11() epsilon-transitive epsilon-connected ordinal natural V33() real ext-real positive non negative V38() V57() V58() V59() V60() V61() V62() V63() Element of NAT
0 is V11() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V33() real ext-real non positive non negative V38() V57() V58() V59() V60() V61() V62() V63() V64() Element of NAT
- 1 is V33() real ext-real non positive 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 strict Abelian RLSStruct
Zero_ (the_set_of_l2RealSequences,Linear_Space_of_RealSequences) is Element of the_set_of_l2RealSequences
Add_ (the_set_of_l2RealSequences,Linear_Space_of_RealSequences) is Relation-like [:the_set_of_l2RealSequences,the_set_of_l2RealSequences:] -defined the_set_of_l2RealSequences -valued Function-like V14([:the_set_of_l2RealSequences,the_set_of_l2RealSequences:]) V18([:the_set_of_l2RealSequences,the_set_of_l2RealSequences:], the_set_of_l2RealSequences ) Element of bool [:[:the_set_of_l2RealSequences,the_set_of_l2RealSequences:],the_set_of_l2RealSequences:]
[:[:the_set_of_l2RealSequences,the_set_of_l2RealSequences:],the_set_of_l2RealSequences:] is set
bool [:[:the_set_of_l2RealSequences,the_set_of_l2RealSequences:],the_set_of_l2RealSequences:] is set
Mult_ (the_set_of_l2RealSequences,Linear_Space_of_RealSequences) is Relation-like [:REAL,the_set_of_l2RealSequences:] -defined the_set_of_l2RealSequences -valued Function-like V14([:REAL,the_set_of_l2RealSequences:]) V18([:REAL,the_set_of_l2RealSequences:], the_set_of_l2RealSequences ) Element of bool [:[:REAL,the_set_of_l2RealSequences:],the_set_of_l2RealSequences:]
[:REAL,the_set_of_l2RealSequences:] is set
[:[:REAL,the_set_of_l2RealSequences:],the_set_of_l2RealSequences:] is set
bool [:[:REAL,the_set_of_l2RealSequences:],the_set_of_l2RealSequences:] is set
RLSStruct(# the_set_of_l2RealSequences,(Zero_ (the_set_of_l2RealSequences,Linear_Space_of_RealSequences)),(Add_ (the_set_of_l2RealSequences,Linear_Space_of_RealSequences)),(Mult_ (the_set_of_l2RealSequences,Linear_Space_of_RealSequences)) #) is strict RLSStruct
l_scalar is Relation-like [:the_set_of_l2RealSequences,the_set_of_l2RealSequences:] -defined REAL -valued Function-like V14([:the_set_of_l2RealSequences,the_set_of_l2RealSequences:]) V18([:the_set_of_l2RealSequences,the_set_of_l2RealSequences:], REAL ) V40() V41() V42() Element of bool [:[:the_set_of_l2RealSequences,the_set_of_l2RealSequences:],REAL:]
l2_Space is V78() right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital UNITSTR
UNITSTR(# the_set_of_l2RealSequences,(Zero_ (the_set_of_l2RealSequences,Linear_Space_of_RealSequences)),(Add_ (the_set_of_l2RealSequences,Linear_Space_of_RealSequences)),(Mult_ (the_set_of_l2RealSequences,Linear_Space_of_RealSequences)),l_scalar #) is V78() strict UNITSTR
2 is V11() epsilon-transitive epsilon-connected ordinal natural V33() real ext-real positive non negative V38() V57() V58() V59() V60() V61() V62() V63() Element of NAT
the carrier of l2_Space is V11() set
0. l2_Space is V85( l2_Space ) Element of the carrier of l2_Space
the ZeroF of l2_Space is Element of the carrier of l2_Space
1 / 2 is V33() real ext-real non negative Element of REAL
f is Element of the carrier of l2_Space
seq_id f is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
tseq is Element of the carrier of l2_Space
seq_id tseq is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
(seq_id f) (#) (seq_id tseq) is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
(seq_id tseq) (#) (seq_id tseq) is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
(seq_id f) (#) (seq_id f) is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
abs ((seq_id f) (#) (seq_id tseq)) is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
2 (#) (abs ((seq_id f) (#) (seq_id tseq))) is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
n is epsilon-transitive epsilon-connected ordinal natural V33() real ext-real non negative V38() V57() V58() V59() V60() V61() V62() V63() Element of NAT
(2 (#) (abs ((seq_id f) (#) (seq_id tseq)))) . n is V33() real ext-real Element of REAL
((seq_id f) (#) (seq_id tseq)) . n is V33() real ext-real Element of REAL
abs (((seq_id f) (#) (seq_id tseq)) . n) is V33() real ext-real Element of REAL
v is V33() real ext-real Element of REAL
(abs ((seq_id f) (#) (seq_id tseq))) . n is V33() real ext-real Element of REAL
2 * ((abs ((seq_id f) (#) (seq_id tseq))) . n) is V33() real ext-real Element of REAL
2 * (abs (((seq_id f) (#) (seq_id tseq)) . n)) is V33() real ext-real Element of REAL
((seq_id tseq) (#) (seq_id tseq)) + ((seq_id f) (#) (seq_id f)) is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
v is epsilon-transitive epsilon-connected ordinal natural V33() real ext-real non negative V38() V57() V58() V59() V60() V61() V62() V63() Element of NAT
(2 (#) (abs ((seq_id f) (#) (seq_id tseq)))) . v is V33() real ext-real Element of REAL
(((seq_id tseq) (#) (seq_id tseq)) + ((seq_id f) (#) (seq_id f))) . v is V33() real ext-real Element of REAL
(seq_id tseq) . v is V33() real ext-real Element of REAL
(seq_id f) . v is V33() real ext-real Element of REAL
y is V33() real ext-real Element of REAL
abs y is V33() real ext-real Element of REAL
rseq is V33() real ext-real Element of REAL
abs rseq is V33() real ext-real Element of REAL
((seq_id tseq) (#) (seq_id tseq)) . v is V33() real ext-real Element of REAL
((seq_id f) (#) (seq_id f)) . v is V33() real ext-real Element of REAL
(((seq_id tseq) (#) (seq_id tseq)) . v) + (((seq_id f) (#) (seq_id f)) . v) is V33() real ext-real Element of REAL
((seq_id tseq) . v) * ((seq_id tseq) . v) is V33() real ext-real Element of REAL
(((seq_id tseq) . v) * ((seq_id tseq) . v)) + (((seq_id f) (#) (seq_id f)) . v) is V33() real ext-real Element of REAL
y ^2 is V33() real ext-real Element of REAL
y * y is V33() real ext-real set
((seq_id f) . v) * ((seq_id f) . v) is V33() real ext-real Element of REAL
(y ^2) + (((seq_id f) . v) * ((seq_id f) . v)) is V33() real ext-real Element of REAL
(abs y) ^2 is V33() real ext-real Element of REAL
(abs y) * (abs y) is V33() real ext-real set
rseq ^2 is V33() real ext-real Element of REAL
rseq * rseq is V33() real ext-real set
((abs y) ^2) + (rseq ^2) is V33() real ext-real Element of REAL
(abs rseq) ^2 is V33() real ext-real Element of REAL
(abs rseq) * (abs rseq) is V33() real ext-real set
((abs y) ^2) + ((abs rseq) ^2) is V33() real ext-real Element of REAL
(abs y) - (abs rseq) is V33() real ext-real Element of REAL
((abs y) - (abs rseq)) ^2 is V33() real ext-real Element of REAL
((abs y) - (abs rseq)) * ((abs y) - (abs rseq)) is V33() real ext-real set
(abs ((seq_id f) (#) (seq_id tseq))) . v is V33() real ext-real Element of REAL
2 * ((abs ((seq_id f) (#) (seq_id tseq))) . v) is V33() real ext-real Element of REAL
((seq_id f) (#) (seq_id tseq)) . v is V33() real ext-real Element of REAL
abs (((seq_id f) (#) (seq_id tseq)) . v) is V33() real ext-real Element of REAL
2 * (abs (((seq_id f) (#) (seq_id tseq)) . v)) is V33() real ext-real Element of REAL
((seq_id f) . v) * ((seq_id tseq) . v) is V33() real ext-real Element of REAL
abs (((seq_id f) . v) * ((seq_id tseq) . v)) is V33() real ext-real Element of REAL
2 * (abs (((seq_id f) . v) * ((seq_id tseq) . v))) is V33() real ext-real Element of REAL
m is V33() real ext-real Element of REAL
tt is V33() real ext-real Element of REAL
m * tt is V33() real ext-real Element of REAL
2 * (m * tt) is V33() real ext-real Element of REAL
2 * (abs y) is V33() real ext-real Element of REAL
(2 * (abs y)) * (abs rseq) is V33() real ext-real Element of REAL
0 + ((2 (#) (abs ((seq_id f) (#) (seq_id tseq)))) . v) is V33() real ext-real Element of REAL
((((seq_id tseq) (#) (seq_id tseq)) + ((seq_id f) (#) (seq_id f))) . v) - ((2 (#) (abs ((seq_id f) (#) (seq_id tseq)))) . v) is V33() real ext-real Element of REAL
(((((seq_id tseq) (#) (seq_id tseq)) + ((seq_id f) (#) (seq_id f))) . v) - ((2 (#) (abs ((seq_id f) (#) (seq_id tseq)))) . v)) + ((2 (#) (abs ((seq_id f) (#) (seq_id tseq)))) . v) is V33() real ext-real Element of REAL
(1 / 2) (#) (2 (#) (abs ((seq_id f) (#) (seq_id tseq)))) is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
(1 / 2) * 2 is V33() real ext-real non negative Element of REAL
((1 / 2) * 2) (#) (abs ((seq_id f) (#) (seq_id tseq))) is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
c₁ is set
seq_id c₁ is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
(seq_id c₁) (#) (seq_id c₁) is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
c₁ is Element of the carrier of l2_Space
f is Element of the carrier of l2_Space
c₁ .|. f is V33() real ext-real Element of REAL
seq_id c₁ is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
seq_id f is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
(seq_id c₁) (#) (seq_id f) is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
Sum ((seq_id c₁) (#) (seq_id f)) is V33() real ext-real Element of REAL
the scalar of l2_Space is Relation-like [: the carrier of l2_Space, the carrier of l2_Space:] -defined REAL -valued Function-like V14([: the carrier of l2_Space, the carrier of l2_Space:]) V18([: the carrier of l2_Space, the carrier of l2_Space:], REAL ) V40() V41() V42() Element of bool [:[: the carrier of l2_Space, the carrier of l2_Space:],REAL:]
[: the carrier of l2_Space, the carrier of l2_Space:] is set
[:[: the carrier of l2_Space, the carrier of l2_Space:],REAL:] is V40() V41() V42() set
bool [:[: the carrier of l2_Space, the carrier of l2_Space:],REAL:] is set
the scalar of l2_Space . (c₁,f) is V33() real ext-real Element of REAL
[c₁,f] is set
the scalar of l2_Space . [c₁,f] is V33() real ext-real set
tseq is Element of the carrier of l2_Space
tv is Element of the carrier of l2_Space
tseq + tv is Element of the carrier of l2_Space
the addF of l2_Space is Relation-like [: the carrier of l2_Space, the carrier of l2_Space:] -defined the carrier of l2_Space -valued Function-like V14([: the carrier of l2_Space, the carrier of l2_Space:]) V18([: the carrier of l2_Space, the carrier of l2_Space:], the carrier of l2_Space) Element of bool [:[: the carrier of l2_Space, the carrier of l2_Space:], the carrier of l2_Space:]
[: the carrier of l2_Space, the carrier of l2_Space:] is set
[:[: the carrier of l2_Space, the carrier of l2_Space:], the carrier of l2_Space:] is set
bool [:[: the carrier of l2_Space, the carrier of l2_Space:], the carrier of l2_Space:] is set
the addF of l2_Space . (tseq,tv) is Element of the carrier of l2_Space
[tseq,tv] is set
the addF of l2_Space . [tseq,tv] is set
seq_id tseq is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
seq_id tv is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
(seq_id tseq) + (seq_id tv) is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() 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 || the_set_of_l2RealSequences is Relation-like Function-like set
the addF of Linear_Space_of_RealSequences | [:the_set_of_l2RealSequences,the_set_of_l2RealSequences:] is Relation-like set
dom ( the addF of Linear_Space_of_RealSequences || the_set_of_l2RealSequences) is set
( the addF of Linear_Space_of_RealSequences || the_set_of_l2RealSequences) . [tseq,tv] is set
e is Element of the carrier of Linear_Space_of_RealSequences
m is Element of the carrier of Linear_Space_of_RealSequences
e + m is Element of the carrier of Linear_Space_of_RealSequences
the addF of Linear_Space_of_RealSequences . (e,m) is Element of the carrier of Linear_Space_of_RealSequences
[e,m] is set
the addF of Linear_Space_of_RealSequences . [e,m] is set
tseq is V33() real ext-real Element of REAL
tv is Element of the carrier of l2_Space
tseq * tv is Element of the carrier of l2_Space
the Mult of l2_Space is Relation-like [:REAL, the carrier of l2_Space:] -defined the carrier of l2_Space -valued Function-like V14([:REAL, the carrier of l2_Space:]) V18([:REAL, the carrier of l2_Space:], the carrier of l2_Space) Element of bool [:[:REAL, the carrier of l2_Space:], the carrier of l2_Space:]
[:REAL, the carrier of l2_Space:] is set
[:[:REAL, the carrier of l2_Space:], the carrier of l2_Space:] is set
bool [:[:REAL, the carrier of l2_Space:], the carrier of l2_Space:] is set
the Mult of l2_Space . (tseq,tv) is set
[tseq,tv] is set
the Mult of l2_Space . [tseq,tv] is set
seq_id tv is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
tseq (#) (seq_id tv) is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() 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,the_set_of_l2RealSequences:] 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,the_set_of_l2RealSequences:]) is Relation-like set
( the Mult of Linear_Space_of_RealSequences | [:REAL,the_set_of_l2RealSequences:]) . [tseq,tv] is set
e is Element of the carrier of Linear_Space_of_RealSequences
tseq * e is Element of the carrier of Linear_Space_of_RealSequences
the Mult of Linear_Space_of_RealSequences . (tseq,e) is set
[tseq,e] is set
the Mult of Linear_Space_of_RealSequences . [tseq,e] is set
c₁ is Element of the carrier of l2_Space
seq_id c₁ is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
c₁ is Element of the carrier of l2_Space
- c₁ is Element of the carrier of l2_Space
seq_id c₁ is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
- (seq_id c₁) is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
seq_id (- c₁) is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
(- 1) * c₁ is Element of the carrier of l2_Space
the Mult of l2_Space is Relation-like [:REAL, the carrier of l2_Space:] -defined the carrier of l2_Space -valued Function-like V14([:REAL, the carrier of l2_Space:]) V18([:REAL, the carrier of l2_Space:], the carrier of l2_Space) Element of bool [:[:REAL, the carrier of l2_Space:], the carrier of l2_Space:]
[:REAL, the carrier of l2_Space:] is set
[:[:REAL, the carrier of l2_Space:], the carrier of l2_Space:] is set
bool [:[:REAL, the carrier of l2_Space:], the carrier of l2_Space:] is set
the Mult of l2_Space . ((- 1),c₁) is set
[(- 1),c₁] is set
the Mult of l2_Space . [(- 1),c₁] is set
(- 1) (#) (seq_id c₁) is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
c₁ is Element of the carrier of l2_Space
f is Element of the carrier of l2_Space
c₁ - f is Element of the carrier of l2_Space
- f is Element of the carrier of l2_Space
c₁ + (- f) is Element of the carrier of l2_Space
the addF of l2_Space is Relation-like [: the carrier of l2_Space, the carrier of l2_Space:] -defined the carrier of l2_Space -valued Function-like V14([: the carrier of l2_Space, the carrier of l2_Space:]) V18([: the carrier of l2_Space, the carrier of l2_Space:], the carrier of l2_Space) Element of bool [:[: the carrier of l2_Space, the carrier of l2_Space:], the carrier of l2_Space:]
[: the carrier of l2_Space, the carrier of l2_Space:] is set
[:[: the carrier of l2_Space, the carrier of l2_Space:], the carrier of l2_Space:] is set
bool [:[: the carrier of l2_Space, the carrier of l2_Space:], the carrier of l2_Space:] is set
the addF of l2_Space . (c₁,(- f)) is Element of the carrier of l2_Space
[c₁,(- f)] is set
the addF of l2_Space . [c₁,(- f)] is set
seq_id c₁ is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
seq_id f is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
(seq_id c₁) - (seq_id f) is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
seq_id (- f) is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
(seq_id c₁) + (seq_id (- f)) is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
- (seq_id f) is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
(seq_id c₁) + (- (seq_id f)) is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
0. Linear_Space_of_RealSequences is V85( 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
c₁ is set
seq_id c₁ is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
(seq_id c₁) (#) (seq_id c₁) is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
f is set
seq_id f is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
(seq_id f) (#) (seq_id f) is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
tseq is Element of the carrier of l2_Space
seq_id tseq is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
tv is Element of the carrier of l2_Space
e is Element of the carrier of l2_Space
tv + e is Element of the carrier of l2_Space
the addF of l2_Space is Relation-like [: the carrier of l2_Space, the carrier of l2_Space:] -defined the carrier of l2_Space -valued Function-like V14([: the carrier of l2_Space, the carrier of l2_Space:]) V18([: the carrier of l2_Space, the carrier of l2_Space:], the carrier of l2_Space) Element of bool [:[: the carrier of l2_Space, the carrier of l2_Space:], the carrier of l2_Space:]
[: the carrier of l2_Space, the carrier of l2_Space:] is set
[:[: the carrier of l2_Space, the carrier of l2_Space:], the carrier of l2_Space:] is set
bool [:[: the carrier of l2_Space, the carrier of l2_Space:], the carrier of l2_Space:] is set
the addF of l2_Space . (tv,e) is Element of the carrier of l2_Space
[tv,e] is set
the addF of l2_Space . [tv,e] is set
seq_id tv is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
seq_id e is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
(seq_id tv) + (seq_id e) is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
u is Element of the carrier of l2_Space
m is V33() real ext-real Element of REAL
m * u is Element of the carrier of l2_Space
the Mult of l2_Space is Relation-like [:REAL, the carrier of l2_Space:] -defined the carrier of l2_Space -valued Function-like V14([:REAL, the carrier of l2_Space:]) V18([:REAL, the carrier of l2_Space:], the carrier of l2_Space) Element of bool [:[:REAL, the carrier of l2_Space:], the carrier of l2_Space:]
[:REAL, the carrier of l2_Space:] is set
[:[:REAL, the carrier of l2_Space:], the carrier of l2_Space:] is set
bool [:[:REAL, the carrier of l2_Space:], the carrier of l2_Space:] is set
the Mult of l2_Space . (m,u) is set
[m,u] is set
the Mult of l2_Space . [m,u] is set
seq_id u is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
m (#) (seq_id u) is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
n is Element of the carrier of l2_Space
- n is Element of the carrier of l2_Space
seq_id n is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
- (seq_id n) is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
v is Element of the carrier of l2_Space
- v is Element of the carrier of l2_Space
seq_id (- v) is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
seq_id v is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
- (seq_id v) is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
y is Element of the carrier of l2_Space
rseq is Element of the carrier of l2_Space
y - rseq is Element of the carrier of l2_Space
- rseq is Element of the carrier of l2_Space
y + (- rseq) is Element of the carrier of l2_Space
the addF of l2_Space . (y,(- rseq)) is Element of the carrier of l2_Space
[y,(- rseq)] is set
the addF of l2_Space . [y,(- rseq)] is set
seq_id y is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
seq_id rseq is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
(seq_id y) - (seq_id rseq) is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
m is Element of the carrier of l2_Space
seq_id m is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
tt is Element of the carrier of l2_Space
seq_id tt is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
(seq_id m) (#) (seq_id tt) is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
c₁₄ is Element of the carrier of l2_Space
c₁₅ is Element of the carrier of l2_Space
c₁₄ .|. c₁₅ is V33() real ext-real Element of REAL
seq_id c₁₄ is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
seq_id c₁₅ is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
(seq_id c₁₄) (#) (seq_id c₁₅) is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
Sum ((seq_id c₁₄) (#) (seq_id c₁₅)) is V33() real ext-real Element of REAL
c₁ is Element of the carrier of l2_Space
c₁ .|. c₁ is V33() real ext-real Element of REAL
f is Element of the carrier of l2_Space
c₁ .|. f is V33() real ext-real Element of REAL
f .|. c₁ is V33() real ext-real Element of REAL
c₁ + f is Element of the carrier of l2_Space
the addF of l2_Space is Relation-like [: the carrier of l2_Space, the carrier of l2_Space:] -defined the carrier of l2_Space -valued Function-like V14([: the carrier of l2_Space, the carrier of l2_Space:]) V18([: the carrier of l2_Space, the carrier of l2_Space:], the carrier of l2_Space) Element of bool [:[: the carrier of l2_Space, the carrier of l2_Space:], the carrier of l2_Space:]
[: the carrier of l2_Space, the carrier of l2_Space:] is set
[:[: the carrier of l2_Space, the carrier of l2_Space:], the carrier of l2_Space:] is set
bool [:[: the carrier of l2_Space, the carrier of l2_Space:], the carrier of l2_Space:] is set
the addF of l2_Space . (c₁,f) is Element of the carrier of l2_Space
[c₁,f] is set
the addF of l2_Space . [c₁,f] is set
tseq is Element of the carrier of l2_Space
(c₁ + f) .|. tseq is V33() real ext-real Element of REAL
c₁ .|. tseq is V33() real ext-real Element of REAL
f .|. tseq is V33() real ext-real Element of REAL
(c₁ .|. tseq) + (f .|. tseq) is V33() real ext-real Element of REAL
tv is V33() real ext-real Element of REAL
tv * c₁ is Element of the carrier of l2_Space
the Mult of l2_Space is Relation-like [:REAL, the carrier of l2_Space:] -defined the carrier of l2_Space -valued Function-like V14([:REAL, the carrier of l2_Space:]) V18([:REAL, the carrier of l2_Space:], the carrier of l2_Space) Element of bool [:[:REAL, the carrier of l2_Space:], the carrier of l2_Space:]
[:REAL, the carrier of l2_Space:] is set
[:[:REAL, the carrier of l2_Space:], the carrier of l2_Space:] is set
bool [:[:REAL, the carrier of l2_Space:], the carrier of l2_Space:] is set
the Mult of l2_Space . (tv,c₁) is set
[tv,c₁] is set
the Mult of l2_Space . [tv,c₁] is set
(tv * c₁) .|. f is V33() real ext-real Element of REAL
tv * (c₁ .|. f) is V33() real ext-real Element of REAL
seq_id c₁ is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
(seq_id c₁) (#) (seq_id c₁) is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
e is epsilon-transitive epsilon-connected ordinal natural V33() real ext-real non negative V38() V57() V58() V59() V60() V61() V62() V63() Element of NAT
((seq_id c₁) (#) (seq_id c₁)) . e is V33() real ext-real Element of REAL
(seq_id c₁) . e is V33() real ext-real Element of REAL
((seq_id c₁) . e) * ((seq_id c₁) . e) is V33() real ext-real Element of REAL
Sum ((seq_id c₁) (#) (seq_id c₁)) is V33() real ext-real Element of REAL
e is epsilon-transitive epsilon-connected ordinal natural V33() real ext-real non negative V38() V57() V58() V59() V60() V61() V62() V63() Element of NAT
((seq_id c₁) (#) (seq_id c₁)) . e is V33() real ext-real Element of REAL
(seq_id c₁) . e is V33() real ext-real Element of REAL
((seq_id c₁) . e) * ((seq_id c₁) . e) is V33() real ext-real Element of REAL
e is epsilon-transitive epsilon-connected ordinal natural V33() real ext-real non negative V38() V57() V58() V59() V60() V61() V62() V63() Element of NAT
(seq_id c₁) . e is V33() real ext-real Element of REAL
((seq_id c₁) (#) (seq_id c₁)) . e is V33() real ext-real Element of REAL
((seq_id c₁) . e) * ((seq_id c₁) . e) is V33() real ext-real Element of REAL
seq_id f is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
(seq_id c₁) (#) (seq_id f) is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
Sum ((seq_id c₁) (#) (seq_id f)) is V33() real ext-real Element of REAL
e is epsilon-transitive epsilon-connected ordinal natural V33() real ext-real non negative V38() V57() V58() V59() V60() V61() V62() V63() Element of NAT
((seq_id c₁) (#) (seq_id c₁)) . e is V33() real ext-real Element of REAL
(seq_id c₁) . e is V33() real ext-real Element of REAL
((seq_id c₁) . e) * ((seq_id c₁) . e) is V33() real ext-real Element of REAL
((seq_id c₁) . e) * 0 is V33() real ext-real Element of REAL
seq_id (tv * c₁) is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
(seq_id (tv * c₁)) (#) (seq_id f) is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
Sum ((seq_id (tv * c₁)) (#) (seq_id f)) is V33() real ext-real Element of REAL
tv (#) (seq_id c₁) is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
seq_id (tv (#) (seq_id c₁)) is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
(seq_id (tv (#) (seq_id c₁))) (#) (seq_id f) is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
Sum ((seq_id (tv (#) (seq_id c₁))) (#) (seq_id f)) is V33() real ext-real Element of REAL
(tv (#) (seq_id c₁)) (#) (seq_id f) is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
Sum ((tv (#) (seq_id c₁)) (#) (seq_id f)) is V33() real ext-real Element of REAL
tv (#) ((seq_id c₁) (#) (seq_id f)) is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
Sum (tv (#) ((seq_id c₁) (#) (seq_id f))) is V33() real ext-real Element of REAL
tv * (Sum ((seq_id c₁) (#) (seq_id f))) is V33() real ext-real Element of REAL
seq_id tseq is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
(seq_id c₁) (#) (seq_id tseq) is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
(seq_id f) (#) (seq_id tseq) is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
seq_id (c₁ + f) is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
(seq_id (c₁ + f)) (#) (seq_id tseq) is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
Sum ((seq_id (c₁ + f)) (#) (seq_id tseq)) is V33() real ext-real Element of REAL
(seq_id c₁) + (seq_id f) is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
seq_id ((seq_id c₁) + (seq_id f)) is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
(seq_id ((seq_id c₁) + (seq_id f))) (#) (seq_id tseq) is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
Sum ((seq_id ((seq_id c₁) + (seq_id f))) (#) (seq_id tseq)) is V33() real ext-real Element of REAL
((seq_id c₁) + (seq_id f)) (#) (seq_id tseq) is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
Sum (((seq_id c₁) + (seq_id f)) (#) (seq_id tseq)) is V33() real ext-real Element of REAL
((seq_id c₁) (#) (seq_id tseq)) + ((seq_id f) (#) (seq_id tseq)) is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
Sum (((seq_id c₁) (#) (seq_id tseq)) + ((seq_id f) (#) (seq_id tseq))) is V33() real ext-real Element of REAL
Sum ((seq_id c₁) (#) (seq_id tseq)) is V33() real ext-real Element of REAL
Sum ((seq_id f) (#) (seq_id tseq)) is V33() real ext-real Element of REAL
(Sum ((seq_id c₁) (#) (seq_id tseq))) + (Sum ((seq_id f) (#) (seq_id tseq))) is V33() real ext-real Element of REAL
(c₁ .|. tseq) + (Sum ((seq_id f) (#) (seq_id tseq))) is V33() real ext-real Element of REAL
c₁ is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
Partial_Sums c₁ is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
Sum c₁ is V33() real ext-real Element of REAL
f is epsilon-transitive epsilon-connected ordinal natural V33() real ext-real non negative V38() V57() V58() V59() V60() V61() V62() V63() Element of NAT
(Partial_Sums c₁) . f is V33() real ext-real Element of REAL
f + 0 is epsilon-transitive epsilon-connected ordinal natural V33() real ext-real non negative V38() V57() V58() V59() V60() V61() V62() V63() Element of NAT
(Partial_Sums c₁) . 0 is V33() real ext-real Element of REAL
c₁ . 0 is V33() real ext-real Element of REAL
f is epsilon-transitive epsilon-connected ordinal natural V33() real ext-real non negative V38() V57() V58() V59() V60() V61() V62() V63() Element of NAT
c₁ . f is V33() real ext-real Element of REAL
(Partial_Sums c₁) . f is V33() real ext-real Element of REAL
f - 1 is V33() real ext-real Element of REAL
0 + 1 is V11() epsilon-transitive epsilon-connected ordinal natural V33() real ext-real positive non negative V38() V57() V58() V59() V60() V61() V62() V63() Element of NAT
(Partial_Sums c₁) . (f - 1) is V33() real ext-real Element of REAL
(f - 1) + 1 is V33() real ext-real Element of REAL
(c₁ . f) + 0 is V33() real ext-real Element of REAL
(c₁ . f) + ((Partial_Sums c₁) . (f - 1)) is V33() real ext-real Element of REAL
f is epsilon-transitive epsilon-connected ordinal natural V33() real ext-real non negative V38() V57() V58() V59() V60() V61() V62() V63() Element of NAT
(Partial_Sums c₁) . f is V33() real ext-real Element of REAL
lim (Partial_Sums c₁) is V33() real ext-real Element of REAL
f is epsilon-transitive epsilon-connected ordinal natural V33() real ext-real non negative V38() V57() V58() V59() V60() V61() V62() V63() Element of NAT
c₁ . f is V33() real ext-real Element of REAL
(Partial_Sums c₁) . f is V33() real ext-real Element of REAL
c₁ is V33() real ext-real Element of REAL
f is V33() real ext-real Element of REAL
c₁ - f is V33() real ext-real Element of REAL
(c₁ - f) ^2 is V33() real ext-real Element of REAL
(c₁ - f) * (c₁ - f) is V33() real ext-real set
c₁ + f is V33() real ext-real Element of REAL
(c₁ + f) * (c₁ + f) is V33() real ext-real Element of REAL
0 + ((c₁ + f) * (c₁ + f)) is V33() real ext-real Element of REAL
2 * c₁ is V33() real ext-real Element of REAL
(2 * c₁) * c₁ is V33() real ext-real Element of REAL
2 * f is V33() real ext-real Element of REAL
(2 * f) * f is V33() real ext-real Element of REAL
((2 * c₁) * c₁) + ((2 * f) * f) is V33() real ext-real Element of REAL
(((2 * c₁) * c₁) + ((2 * f) * f)) - ((c₁ + f) * (c₁ + f)) is V33() real ext-real Element of REAL
((((2 * c₁) * c₁) + ((2 * f) * f)) - ((c₁ + f) * (c₁ + f))) + ((c₁ + f) * (c₁ + f)) is V33() real ext-real Element of REAL
c₁ is V33() real ext-real Element of REAL
f is V33() real ext-real Element of REAL
c₁ - f is V33() real ext-real Element of REAL
(c₁ - f) + f is V33() real ext-real Element of REAL
c₁ * c₁ is V33() real ext-real Element of REAL
2 * (c₁ - f) is V33() real ext-real Element of REAL
(2 * (c₁ - f)) * (c₁ - f) is V33() real ext-real Element of REAL
2 * f is V33() real ext-real Element of REAL
(2 * f) * f is V33() real ext-real Element of REAL
((2 * (c₁ - f)) * (c₁ - f)) + ((2 * f) * f) is V33() real ext-real Element of REAL
c₁ is V33() real ext-real Element of REAL
f is V33() real ext-real Element of REAL
c₁ + f is V33() real ext-real Element of REAL
(c₁ + f) * (c₁ + f) is V33() real ext-real Element of REAL
2 * c₁ is V33() real ext-real Element of REAL
(2 * c₁) * c₁ is V33() real ext-real Element of REAL
2 * f is V33() real ext-real Element of REAL
(2 * f) * f is V33() real ext-real Element of REAL
((2 * c₁) * c₁) + ((2 * f) * f) is V33() real ext-real Element of REAL
tseq is V33() real ext-real Element of REAL
tseq * tseq is V33() real ext-real Element of REAL
tv is V33() real ext-real Element of REAL
tseq - tv is V33() real ext-real Element of REAL
2 * (tseq - tv) is V33() real ext-real Element of REAL
(2 * (tseq - tv)) * (tseq - tv) is V33() real ext-real Element of REAL
2 * tv is V33() real ext-real Element of REAL
(2 * tv) * tv is V33() real ext-real Element of REAL
((2 * (tseq - tv)) * (tseq - tv)) + ((2 * tv) * tv) is V33() real ext-real Element of REAL
c₁ is V33() real ext-real Element of REAL
f is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
lim f is V33() real ext-real Element of REAL
tseq is epsilon-transitive epsilon-connected ordinal natural V33() real ext-real non negative V38() V57() V58() V59() V60() V61() V62() V63() Element of NAT
tseq is epsilon-transitive epsilon-connected ordinal natural V33() real ext-real non negative V38() V57() V58() V59() V60() V61() V62() V63() Element of NAT
NAT --> c₁ is Relation-like NAT -defined REAL -valued Function-like constant V11() V14( NAT ) V18( NAT , REAL ) T-Sequence-like V40() V41() V42() convergent Element of bool [:NAT,REAL:]
tv is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
lim tv is V33() real ext-real Element of REAL
tv . 0 is V33() real ext-real Element of REAL
f ^\ tseq is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
e is epsilon-transitive epsilon-connected ordinal natural V33() real ext-real non negative V38() V57() V58() V59() V60() V61() V62() V63() Element of NAT
(f ^\ tseq) . e is V33() real ext-real Element of REAL
tseq + e is epsilon-transitive epsilon-connected ordinal natural V33() real ext-real non negative V38() V57() V58() V59() V60() V61() V62() V63() Element of NAT
f . (tseq + e) is V33() real ext-real Element of REAL
tv . e is V33() real ext-real Element of REAL
lim (f ^\ tseq) is V33() real ext-real Element of REAL
c₁ is V33() real ext-real Element of REAL
NAT --> c₁ is Relation-like NAT -defined REAL -valued Function-like constant V11() V14( NAT ) V18( NAT , REAL ) T-Sequence-like V40() V41() V42() convergent Element of bool [:NAT,REAL:]
tseq is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
lim tseq is V33() real ext-real Element of REAL
(lim tseq) - c₁ is V33() real ext-real Element of REAL
((lim tseq) - c₁) * ((lim tseq) - c₁) is V33() real ext-real Element of REAL
f is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
tseq - f is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
(tseq - f) (#) (tseq - f) is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
tv is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
lim tv is V33() real ext-real Element of REAL
e is epsilon-transitive epsilon-connected ordinal natural V33() real ext-real non negative V38() V57() V58() V59() V60() V61() V62() V63() Element of NAT
tv . e is V33() real ext-real Element of REAL
tseq . e is V33() real ext-real Element of REAL
(tseq . e) - c₁ is V33() real ext-real Element of REAL
((tseq . e) - c₁) * ((tseq . e) - c₁) is V33() real ext-real Element of REAL
f . e is V33() real ext-real Element of REAL
(tseq . e) - (f . e) is V33() real ext-real Element of REAL
((tseq . e) - (f . e)) * ((tseq . e) - c₁) is V33() real ext-real Element of REAL
- (f . e) is V33() real ext-real Element of REAL
(tseq . e) + (- (f . e)) is V33() real ext-real Element of REAL
((tseq . e) - (f . e)) * ((tseq . e) + (- (f . e))) is V33() real ext-real Element of REAL
- f is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
(- f) . e is V33() real ext-real Element of REAL
(tseq . e) + ((- f) . e) is V33() real ext-real Element of REAL
((tseq . e) + ((- f) . e)) * ((tseq . e) + (- (f . e))) is V33() real ext-real Element of REAL
((tseq . e) + ((- f) . e)) * ((tseq . e) + ((- f) . e)) is V33() real ext-real Element of REAL
tseq + (- f) is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
(tseq + (- f)) . e is V33() real ext-real Element of REAL
((tseq + (- f)) . e) * ((tseq . e) + ((- f) . e)) is V33() real ext-real Element of REAL
((tseq + (- f)) . e) * ((tseq + (- f)) . e) is V33() real ext-real Element of REAL
(tseq - f) . e is V33() real ext-real Element of REAL
((tseq - f) . e) * ((tseq + (- f)) . e) is V33() real ext-real Element of REAL
((tseq - f) . e) * ((tseq - f) . e) is V33() real ext-real Element of REAL
((tseq - f) (#) (tseq - f)) . e is V33() real ext-real Element of REAL
e is set
tv . e is V33() real ext-real Element of REAL
((tseq - f) (#) (tseq - f)) . e is V33() real ext-real Element of REAL
lim ((tseq - f) (#) (tseq - f)) is V33() real ext-real Element of REAL
lim (tseq - f) is V33() real ext-real Element of REAL
(lim (tseq - f)) * (lim (tseq - f)) is V33() real ext-real Element of REAL
lim f is V33() real ext-real Element of REAL
(lim tseq) - (lim f) is V33() real ext-real Element of REAL
((lim tseq) - (lim f)) * (lim (tseq - f)) is V33() real ext-real Element of REAL
((lim tseq) - (lim f)) * ((lim tseq) - (lim f)) is V33() real ext-real Element of REAL
f . 0 is V33() real ext-real Element of REAL
(lim tseq) - (f . 0) is V33() real ext-real Element of REAL
((lim tseq) - (f . 0)) * ((lim tseq) - (lim f)) is V33() real ext-real Element of REAL
((lim tseq) - (f . 0)) * ((lim tseq) - (f . 0)) is V33() real ext-real Element of REAL
((lim tseq) - c₁) * ((lim tseq) - (f . 0)) is V33() real ext-real Element of REAL
c₁ is V33() real ext-real Element of REAL
f is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
tseq is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
lim f is V33() real ext-real Element of REAL
(lim f) - c₁ is V33() real ext-real Element of REAL
((lim f) - c₁) * ((lim f) - c₁) is V33() real ext-real Element of REAL
lim tseq is V33() real ext-real Element of REAL
(((lim f) - c₁) * ((lim f) - c₁)) + (lim tseq) is V33() real ext-real Element of REAL
NAT --> c₁ is Relation-like NAT -defined REAL -valued Function-like constant V11() V14( NAT ) V18( NAT , REAL ) T-Sequence-like V40() V41() V42() convergent Element of bool [:NAT,REAL:]
tv is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
f - tv is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
(f - tv) (#) (f - tv) is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
e is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
lim e is V33() real ext-real Element of REAL
m is epsilon-transitive epsilon-connected ordinal natural V33() real ext-real non negative V38() V57() V58() V59() V60() V61() V62() V63() Element of NAT
e . m is V33() real ext-real Element of REAL
f . m is V33() real ext-real Element of REAL
(f . m) - c₁ is V33() real ext-real Element of REAL
((f . m) - c₁) * ((f . m) - c₁) is V33() real ext-real Element of REAL
tseq . m is V33() real ext-real Element of REAL
(((f . m) - c₁) * ((f . m) - c₁)) + (tseq . m) is V33() real ext-real Element of REAL
tv . m is V33() real ext-real Element of REAL
(f . m) - (tv . m) is V33() real ext-real Element of REAL
((f . m) - (tv . m)) * ((f . m) - c₁) is V33() real ext-real Element of REAL
(((f . m) - (tv . m)) * ((f . m) - c₁)) + (tseq . m) is V33() real ext-real Element of REAL
- (tv . m) is V33() real ext-real Element of REAL
(f . m) + (- (tv . m)) is V33() real ext-real Element of REAL
((f . m) - (tv . m)) * ((f . m) + (- (tv . m))) is V33() real ext-real Element of REAL
(((f . m) - (tv . m)) * ((f . m) + (- (tv . m)))) + (tseq . m) is V33() real ext-real Element of REAL
- tv is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
(- tv) . m is V33() real ext-real Element of REAL
(f . m) + ((- tv) . m) is V33() real ext-real Element of REAL
((f . m) + ((- tv) . m)) * ((f . m) + (- (tv . m))) is V33() real ext-real Element of REAL
(((f . m) + ((- tv) . m)) * ((f . m) + (- (tv . m)))) + (tseq . m) is V33() real ext-real Element of REAL
((f . m) + ((- tv) . m)) * ((f . m) + ((- tv) . m)) is V33() real ext-real Element of REAL
(((f . m) + ((- tv) . m)) * ((f . m) + ((- tv) . m))) + (tseq . m) is V33() real ext-real Element of REAL
f + (- tv) is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
(f + (- tv)) . m is V33() real ext-real Element of REAL
((f + (- tv)) . m) * ((f . m) + ((- tv) . m)) is V33() real ext-real Element of REAL
(((f + (- tv)) . m) * ((f . m) + ((- tv) . m))) + (tseq . m) is V33() real ext-real Element of REAL
((f + (- tv)) . m) * ((f + (- tv)) . m) is V33() real ext-real Element of REAL
(((f + (- tv)) . m) * ((f + (- tv)) . m)) + (tseq . m) is V33() real ext-real Element of REAL
(f - tv) . m is V33() real ext-real Element of REAL
((f - tv) . m) * ((f + (- tv)) . m) is V33() real ext-real Element of REAL
(((f - tv) . m) * ((f + (- tv)) . m)) + (tseq . m) is V33() real ext-real Element of REAL
((f - tv) . m) * ((f - tv) . m) is V33() real ext-real Element of REAL
(((f - tv) . m) * ((f - tv) . m)) + (tseq . m) is V33() real ext-real Element of REAL
((f - tv) (#) (f - tv)) . m is V33() real ext-real Element of REAL
(((f - tv) (#) (f - tv)) . m) + (tseq . m) is V33() real ext-real Element of REAL
((f - tv) (#) (f - tv)) + tseq is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
(((f - tv) (#) (f - tv)) + tseq) . m is V33() real ext-real Element of REAL
lim ((f - tv) (#) (f - tv)) is V33() real ext-real Element of REAL
lim (f - tv) is V33() real ext-real Element of REAL
(lim (f - tv)) * (lim (f - tv)) is V33() real ext-real Element of REAL
lim tv is V33() real ext-real Element of REAL
(lim f) - (lim tv) is V33() real ext-real Element of REAL
((lim f) - (lim tv)) * (lim (f - tv)) is V33() real ext-real Element of REAL
((lim f) - (lim tv)) * ((lim f) - (lim tv)) is V33() real ext-real Element of REAL
tv . 0 is V33() real ext-real Element of REAL
(lim f) - (tv . 0) is V33() real ext-real Element of REAL
((lim f) - (tv . 0)) * ((lim f) - (lim tv)) is V33() real ext-real Element of REAL
((lim f) - (tv . 0)) * ((lim f) - (tv . 0)) is V33() real ext-real Element of REAL
((lim f) - c₁) * ((lim f) - (tv . 0)) is V33() real ext-real Element of REAL
[:NAT, the carrier of l2_Space:] is set
bool [:NAT, the carrier of l2_Space:] is set
c₁ is Relation-like NAT -defined the carrier of l2_Space -valued Function-like V11() V14( NAT ) V18( NAT , the carrier of l2_Space) Element of bool [:NAT, the carrier of l2_Space:]
f is set
tseq is epsilon-transitive epsilon-connected ordinal natural V33() real ext-real non negative V38() V57() V58() V59() V60() V61() V62() V63() Element of NAT
tv is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
lim tv is V33() real ext-real Element of REAL
e is V33() real ext-real set
m is epsilon-transitive epsilon-connected ordinal natural V33() real ext-real non negative V38() V57() V58() V59() V60() V61() V62() V63() Element of NAT
u is epsilon-transitive epsilon-connected ordinal natural V33() real ext-real non negative V38() V57() V58() V59() V60() V61() V62() V63() Element of NAT
c₁ . u is Element of the carrier of l2_Space
c₁ . m is Element of the carrier of l2_Space
(c₁ . u) - (c₁ . m) is Element of the carrier of l2_Space
- (c₁ . m) is Element of the carrier of l2_Space
(c₁ . u) + (- (c₁ . m)) is Element of the carrier of l2_Space
the addF of l2_Space is Relation-like [: the carrier of l2_Space, the carrier of l2_Space:] -defined the carrier of l2_Space -valued Function-like V14([: the carrier of l2_Space, the carrier of l2_Space:]) V18([: the carrier of l2_Space, the carrier of l2_Space:], the carrier of l2_Space) Element of bool [:[: the carrier of l2_Space, the carrier of l2_Space:], the carrier of l2_Space:]
[: the carrier of l2_Space, the carrier of l2_Space:] is set
[:[: the carrier of l2_Space, the carrier of l2_Space:], the carrier of l2_Space:] is set
bool [:[: the carrier of l2_Space, the carrier of l2_Space:], the carrier of l2_Space:] is set
the addF of l2_Space . ((c₁ . u),(- (c₁ . m))) is Element of the carrier of l2_Space
[(c₁ . u),(- (c₁ . m))] is set
the addF of l2_Space . [(c₁ . u),(- (c₁ . m))] is set
||.((c₁ . u) - (c₁ . m)).|| is V33() real ext-real Element of REAL
((c₁ . u) - (c₁ . m)) .|. ((c₁ . u) - (c₁ . m)) is V33() real ext-real Element of REAL
sqrt (((c₁ . u) - (c₁ . m)) .|. ((c₁ . u) - (c₁ . m))) is V33() real ext-real Element of REAL
seq_id ((c₁ . u) - (c₁ . m)) is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
(seq_id ((c₁ . u) - (c₁ . m))) (#) (seq_id ((c₁ . u) - (c₁ . m))) is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
Sum ((seq_id ((c₁ . u) - (c₁ . m))) (#) (seq_id ((c₁ . u) - (c₁ . m)))) is V33() real ext-real Element of REAL
sqrt (Sum ((seq_id ((c₁ . u) - (c₁ . m))) (#) (seq_id ((c₁ . u) - (c₁ . m))))) is V33() real ext-real Element of REAL
tv . u is V33() real ext-real Element of REAL
tv . m is V33() real ext-real Element of REAL
(tv . u) - (tv . m) is V33() real ext-real Element of REAL
abs ((tv . u) - (tv . m)) is V33() real ext-real Element of REAL
(abs ((tv . u) - (tv . m))) * (abs ((tv . u) - (tv . m))) is V33() real ext-real Element of REAL
sqrt ((abs ((tv . u) - (tv . m))) * (abs ((tv . u) - (tv . m)))) is V33() real ext-real Element of REAL
(abs ((tv . u) - (tv . m))) ^2 is V33() real ext-real Element of REAL
(abs ((tv . u) - (tv . m))) * (abs ((tv . u) - (tv . m))) is V33() real ext-real set
sqrt ((abs ((tv . u) - (tv . m))) ^2) is V33() real ext-real Element of REAL
seq_id (c₁ . u) is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
seq_id (c₁ . m) is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
(seq_id (c₁ . u)) - (seq_id (c₁ . m)) is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
seq_id ((seq_id (c₁ . u)) - (seq_id (c₁ . m))) is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
- (seq_id (c₁ . m)) is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
(seq_id (c₁ . u)) + (- (seq_id (c₁ . m))) is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
(seq_id ((c₁ . u) - (c₁ . m))) . tseq is V33() real ext-real Element of REAL
(seq_id (c₁ . u)) . tseq is V33() real ext-real Element of REAL
(- (seq_id (c₁ . m))) . tseq is V33() real ext-real Element of REAL
((seq_id (c₁ . u)) . tseq) + ((- (seq_id (c₁ . m))) . tseq) is V33() real ext-real Element of REAL
(seq_id (c₁ . m)) . tseq is V33() real ext-real Element of REAL
- ((seq_id (c₁ . m)) . tseq) is V33() real ext-real Element of REAL
((seq_id (c₁ . u)) . tseq) + (- ((seq_id (c₁ . m)) . tseq)) is V33() real ext-real Element of REAL
((seq_id (c₁ . u)) . tseq) - ((seq_id (c₁ . m)) . tseq) is V33() real ext-real Element of REAL
(tv . u) - ((seq_id (c₁ . m)) . tseq) is V33() real ext-real Element of REAL
((seq_id ((c₁ . u) - (c₁ . m))) . tseq) * ((seq_id ((c₁ . u) - (c₁ . m))) . tseq) is V33() real ext-real Element of REAL
((tv . u) - (tv . m)) ^2 is V33() real ext-real Element of REAL
((tv . u) - (tv . m)) * ((tv . u) - (tv . m)) is V33() real ext-real set
((seq_id ((c₁ . u) - (c₁ . m))) (#) (seq_id ((c₁ . u) - (c₁ . m)))) . tseq is V33() real ext-real Element of REAL
v is epsilon-transitive epsilon-connected ordinal natural V33() real ext-real non negative V38() V57() V58() V59() V60() V61() V62() V63() Element of NAT
((seq_id ((c₁ . u) - (c₁ . m))) (#) (seq_id ((c₁ . u) - (c₁ . m)))) . v is V33() real ext-real Element of REAL
(seq_id ((c₁ . u) - (c₁ . m))) . v is V33() real ext-real Element of REAL
((seq_id ((c₁ . u) - (c₁ . m))) . v) * ((seq_id ((c₁ . u) - (c₁ . m))) . v) is V33() real ext-real Element of REAL
n is V33() real ext-real Element of REAL
n ^2 is V33() real ext-real Element of REAL
n * n is V33() real ext-real set
(sqrt (Sum ((seq_id ((c₁ . u) - (c₁ . m))) (#) (seq_id ((c₁ . u) - (c₁ . m)))))) ^2 is V33() real ext-real Element of REAL
(sqrt (Sum ((seq_id ((c₁ . u) - (c₁ . m))) (#) (seq_id ((c₁ . u) - (c₁ . m)))))) * (sqrt (Sum ((seq_id ((c₁ . u) - (c₁ . m))) (#) (seq_id ((c₁ . u) - (c₁ . m)))))) is V33() real ext-real set
e * e is V33() real ext-real set
sqrt (e * e) is V33() real ext-real set
sqrt (n ^2) is V33() real ext-real Element of REAL
f is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
tv is epsilon-transitive epsilon-connected ordinal natural V33() real ext-real non negative V38() V57() V58() V59() V60() V61() V62() V63() Element of NAT
e is set
f . e is V33() real ext-real Element of REAL
tseq is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
tseq . tv is V33() real ext-real Element of REAL
m is epsilon-transitive epsilon-connected ordinal natural V33() real ext-real non negative V38() V57() V58() V59() V60() V61() V62() V63() Element of NAT
u is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
lim u is V33() real ext-real Element of REAL
seq_id tseq is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
tv is V33() real ext-real Element of REAL
tv * tv is V33() real ext-real Element of REAL
tv / 2 is V33() real ext-real Element of REAL
m is epsilon-transitive epsilon-connected ordinal natural V33() real ext-real non negative V38() V57() V58() V59() V60() V61() V62() V63() Element of NAT
(tv / 2) * (tv / 2) is V33() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V33() real ext-real non negative V38() V57() V58() V59() V60() V61() V62() V63() Element of NAT
u is epsilon-transitive epsilon-connected ordinal natural V33() real ext-real non negative V38() V57() V58() V59() V60() V61() V62() V63() Element of NAT
c₁ . n is Element of the carrier of l2_Space
c₁ . u is Element of the carrier of l2_Space
(c₁ . n) - (c₁ . u) is Element of the carrier of l2_Space
- (c₁ . u) is Element of the carrier of l2_Space
(c₁ . n) + (- (c₁ . u)) is Element of the carrier of l2_Space
the addF of l2_Space is Relation-like [: the carrier of l2_Space, the carrier of l2_Space:] -defined the carrier of l2_Space -valued Function-like V14([: the carrier of l2_Space, the carrier of l2_Space:]) V18([: the carrier of l2_Space, the carrier of l2_Space:], the carrier of l2_Space) Element of bool [:[: the carrier of l2_Space, the carrier of l2_Space:], the carrier of l2_Space:]
[: the carrier of l2_Space, the carrier of l2_Space:] is set
[:[: the carrier of l2_Space, the carrier of l2_Space:], the carrier of l2_Space:] is set
bool [:[: the carrier of l2_Space, the carrier of l2_Space:], the carrier of l2_Space:] is set
the addF of l2_Space . ((c₁ . n),(- (c₁ . u))) is Element of the carrier of l2_Space
[(c₁ . n),(- (c₁ . u))] is set
the addF of l2_Space . [(c₁ . n),(- (c₁ . u))] is set
seq_id ((c₁ . n) - (c₁ . u)) is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
(seq_id ((c₁ . n) - (c₁ . u))) (#) (seq_id ((c₁ . n) - (c₁ . u))) is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
Sum ((seq_id ((c₁ . n) - (c₁ . u))) (#) (seq_id ((c₁ . n) - (c₁ . u)))) is V33() real ext-real Element of REAL
||.((c₁ . n) - (c₁ . u)).|| is V33() real ext-real Element of REAL
((c₁ . n) - (c₁ . u)) .|. ((c₁ . n) - (c₁ . u)) is V33() real ext-real Element of REAL
sqrt (((c₁ . n) - (c₁ . u)) .|. ((c₁ . n) - (c₁ . u))) is V33() real ext-real Element of REAL
sqrt (Sum ((seq_id ((c₁ . n) - (c₁ . u))) (#) (seq_id ((c₁ . n) - (c₁ . u))))) is V33() real ext-real Element of REAL
v is epsilon-transitive epsilon-connected ordinal natural V33() real ext-real non negative V38() V57() V58() V59() V60() V61() V62() V63() Element of NAT
((seq_id ((c₁ . n) - (c₁ . u))) (#) (seq_id ((c₁ . n) - (c₁ . u)))) . v is V33() real ext-real Element of REAL
(seq_id ((c₁ . n) - (c₁ . u))) . v is V33() real ext-real Element of REAL
((seq_id ((c₁ . n) - (c₁ . u))) . v) * ((seq_id ((c₁ . n) - (c₁ . u))) . v) is V33() real ext-real Element of REAL
(tv / 2) ^2 is V33() real ext-real Element of REAL
(tv / 2) * (tv / 2) is V33() real ext-real set
(sqrt (Sum ((seq_id ((c₁ . n) - (c₁ . u))) (#) (seq_id ((c₁ . n) - (c₁ . u)))))) ^2 is V33() real ext-real Element of REAL
(sqrt (Sum ((seq_id ((c₁ . n) - (c₁ . u))) (#) (seq_id ((c₁ . n) - (c₁ . u)))))) * (sqrt (Sum ((seq_id ((c₁ . n) - (c₁ . u))) (#) (seq_id ((c₁ . n) - (c₁ . u)))))) is V33() real ext-real set
v is epsilon-transitive epsilon-connected ordinal natural V33() real ext-real non negative V38() V57() V58() V59() V60() V61() V62() V63() Element of NAT
((seq_id ((c₁ . n) - (c₁ . u))) (#) (seq_id ((c₁ . n) - (c₁ . u)))) . v is V33() real ext-real Element of REAL
u is epsilon-transitive epsilon-connected ordinal natural V33() real ext-real non negative V38() V57() V58() V59() V60() V61() V62() V63() Element of NAT
c₁ . u is Element of the carrier of l2_Space
seq_id (c₁ . u) is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
(seq_id tseq) - (seq_id (c₁ . u)) is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
((seq_id tseq) - (seq_id (c₁ . u))) (#) ((seq_id tseq) - (seq_id (c₁ . u))) is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
Partial_Sums (((seq_id tseq) - (seq_id (c₁ . u))) (#) ((seq_id tseq) - (seq_id (c₁ . u)))) is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
n is epsilon-transitive epsilon-connected ordinal natural V33() real ext-real non negative V38() V57() V58() V59() V60() V61() V62() V63() Element of NAT
c₁ . n is Element of the carrier of l2_Space
v is epsilon-transitive epsilon-connected ordinal natural V33() real ext-real non negative V38() V57() V58() V59() V60() V61() V62() V63() Element of NAT
c₁ . v is Element of the carrier of l2_Space
(c₁ . n) - (c₁ . v) is Element of the carrier of l2_Space
- (c₁ . v) is Element of the carrier of l2_Space
(c₁ . n) + (- (c₁ . v)) is Element of the carrier of l2_Space
the addF of l2_Space is Relation-like [: the carrier of l2_Space, the carrier of l2_Space:] -defined the carrier of l2_Space -valued Function-like V14([: the carrier of l2_Space, the carrier of l2_Space:]) V18([: the carrier of l2_Space, the carrier of l2_Space:], the carrier of l2_Space) Element of bool [:[: the carrier of l2_Space, the carrier of l2_Space:], the carrier of l2_Space:]
[: the carrier of l2_Space, the carrier of l2_Space:] is set
[:[: the carrier of l2_Space, the carrier of l2_Space:], the carrier of l2_Space:] is set
bool [:[: the carrier of l2_Space, the carrier of l2_Space:], the carrier of l2_Space:] is set
the addF of l2_Space . ((c₁ . n),(- (c₁ . v))) is Element of the carrier of l2_Space
[(c₁ . n),(- (c₁ . v))] is set
the addF of l2_Space . [(c₁ . n),(- (c₁ . v))] is set
seq_id ((c₁ . n) - (c₁ . v)) is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
seq_id (c₁ . n) is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
seq_id (c₁ . v) is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
(seq_id (c₁ . n)) - (seq_id (c₁ . v)) is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
seq_id ((seq_id (c₁ . n)) - (seq_id (c₁ . v))) is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
n is epsilon-transitive epsilon-connected ordinal natural V33() real ext-real non negative V38() V57() V58() V59() V60() V61() V62() V63() Element of NAT
(Partial_Sums (((seq_id tseq) - (seq_id (c₁ . u))) (#) ((seq_id tseq) - (seq_id (c₁ . u))))) . n is V33() real ext-real Element of REAL
n + 1 is V11() epsilon-transitive epsilon-connected ordinal natural V33() real ext-real positive non negative V38() V57() V58() V59() V60() V61() V62() V63() Element of NAT
(Partial_Sums (((seq_id tseq) - (seq_id (c₁ . u))) (#) ((seq_id tseq) - (seq_id (c₁ . u))))) . (n + 1) is V33() real ext-real Element of REAL
v is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
tseq . (n + 1) is V33() real ext-real Element of REAL
y is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
lim y is V33() real ext-real Element of REAL
rseq is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
lim rseq is V33() real ext-real Element of REAL
m is epsilon-transitive epsilon-connected ordinal natural V33() real ext-real non negative V38() V57() V58() V59() V60() V61() V62() V63() Element of NAT
rseq . m is V33() real ext-real Element of REAL
c₁ . m is Element of the carrier of l2_Space
(c₁ . m) - (c₁ . u) is Element of the carrier of l2_Space
- (c₁ . u) is Element of the carrier of l2_Space
(c₁ . m) + (- (c₁ . u)) is Element of the carrier of l2_Space
the addF of l2_Space is Relation-like [: the carrier of l2_Space, the carrier of l2_Space:] -defined the carrier of l2_Space -valued Function-like V14([: the carrier of l2_Space, the carrier of l2_Space:]) V18([: the carrier of l2_Space, the carrier of l2_Space:], the carrier of l2_Space) Element of bool [:[: the carrier of l2_Space, the carrier of l2_Space:], the carrier of l2_Space:]
[: the carrier of l2_Space, the carrier of l2_Space:] is set
[:[: the carrier of l2_Space, the carrier of l2_Space:], the carrier of l2_Space:] is set
bool [:[: the carrier of l2_Space, the carrier of l2_Space:], the carrier of l2_Space:] is set
the addF of l2_Space . ((c₁ . m),(- (c₁ . u))) is Element of the carrier of l2_Space
[(c₁ . m),(- (c₁ . u))] is set
the addF of l2_Space . [(c₁ . m),(- (c₁ . u))] is set
seq_id ((c₁ . m) - (c₁ . u)) is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
(seq_id ((c₁ . m) - (c₁ . u))) (#) (seq_id ((c₁ . m) - (c₁ . u))) is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
Partial_Sums ((seq_id ((c₁ . m) - (c₁ . u))) (#) (seq_id ((c₁ . m) - (c₁ . u)))) is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
(Partial_Sums ((seq_id ((c₁ . m) - (c₁ . u))) (#) (seq_id ((c₁ . m) - (c₁ . u))))) . (n + 1) is V33() real ext-real Element of REAL
((seq_id ((c₁ . m) - (c₁ . u))) (#) (seq_id ((c₁ . m) - (c₁ . u)))) . (n + 1) is V33() real ext-real Element of REAL
(Partial_Sums ((seq_id ((c₁ . m) - (c₁ . u))) (#) (seq_id ((c₁ . m) - (c₁ . u))))) . n is V33() real ext-real Element of REAL
(((seq_id ((c₁ . m) - (c₁ . u))) (#) (seq_id ((c₁ . m) - (c₁ . u)))) . (n + 1)) + ((Partial_Sums ((seq_id ((c₁ . m) - (c₁ . u))) (#) (seq_id ((c₁ . m) - (c₁ . u))))) . n) is V33() real ext-real Element of REAL
seq_id (c₁ . m) is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
(seq_id (c₁ . m)) - (seq_id (c₁ . u)) is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
((seq_id (c₁ . m)) - (seq_id (c₁ . u))) (#) (seq_id ((c₁ . m) - (c₁ . u))) is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
(((seq_id (c₁ . m)) - (seq_id (c₁ . u))) (#) (seq_id ((c₁ . m) - (c₁ . u)))) . (n + 1) is V33() real ext-real Element of REAL
((((seq_id (c₁ . m)) - (seq_id (c₁ . u))) (#) (seq_id ((c₁ . m) - (c₁ . u)))) . (n + 1)) + ((Partial_Sums ((seq_id ((c₁ . m) - (c₁ . u))) (#) (seq_id ((c₁ . m) - (c₁ . u))))) . n) is V33() real ext-real Element of REAL
v . m is V33() real ext-real Element of REAL
((((seq_id (c₁ . m)) - (seq_id (c₁ . u))) (#) (seq_id ((c₁ . m) - (c₁ . u)))) . (n + 1)) + (v . m) is V33() real ext-real Element of REAL
((seq_id (c₁ . m)) - (seq_id (c₁ . u))) (#) ((seq_id (c₁ . m)) - (seq_id (c₁ . u))) is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
(((seq_id (c₁ . m)) - (seq_id (c₁ . u))) (#) ((seq_id (c₁ . m)) - (seq_id (c₁ . u)))) . (n + 1) is V33() real ext-real Element of REAL
((((seq_id (c₁ . m)) - (seq_id (c₁ . u))) (#) ((seq_id (c₁ . m)) - (seq_id (c₁ . u)))) . (n + 1)) + (v . m) is V33() real ext-real Element of REAL
((seq_id (c₁ . m)) - (seq_id (c₁ . u))) . (n + 1) is V33() real ext-real Element of REAL
(((seq_id (c₁ . m)) - (seq_id (c₁ . u))) . (n + 1)) * (((seq_id (c₁ . m)) - (seq_id (c₁ . u))) . (n + 1)) is V33() real ext-real Element of REAL
((((seq_id (c₁ . m)) - (seq_id (c₁ . u))) . (n + 1)) * (((seq_id (c₁ . m)) - (seq_id (c₁ . u))) . (n + 1))) + (v . m) is V33() real ext-real Element of REAL
- (seq_id (c₁ . u)) is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
(seq_id (c₁ . m)) + (- (seq_id (c₁ . u))) is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
((seq_id (c₁ . m)) + (- (seq_id (c₁ . u)))) . (n + 1) is V33() real ext-real Element of REAL
(((seq_id (c₁ . m)) + (- (seq_id (c₁ . u)))) . (n + 1)) * (((seq_id (c₁ . m)) - (seq_id (c₁ . u))) . (n + 1)) is V33() real ext-real Element of REAL
((((seq_id (c₁ . m)) + (- (seq_id (c₁ . u)))) . (n + 1)) * (((seq_id (c₁ . m)) - (seq_id (c₁ . u))) . (n + 1))) + (v . m) is V33() real ext-real Element of REAL
(((seq_id (c₁ . m)) + (- (seq_id (c₁ . u)))) . (n + 1)) * (((seq_id (c₁ . m)) + (- (seq_id (c₁ . u)))) . (n + 1)) is V33() real ext-real Element of REAL
((((seq_id (c₁ . m)) + (- (seq_id (c₁ . u)))) . (n + 1)) * (((seq_id (c₁ . m)) + (- (seq_id (c₁ . u)))) . (n + 1))) + (v . m) is V33() real ext-real Element of REAL
(seq_id (c₁ . m)) . (n + 1) is V33() real ext-real Element of REAL
(- (seq_id (c₁ . u))) . (n + 1) is V33() real ext-real Element of REAL
((seq_id (c₁ . m)) . (n + 1)) + ((- (seq_id (c₁ . u))) . (n + 1)) is V33() real ext-real Element of REAL
(((seq_id (c₁ . m)) . (n + 1)) + ((- (seq_id (c₁ . u))) . (n + 1))) * (((seq_id (c₁ . m)) + (- (seq_id (c₁ . u)))) . (n + 1)) is V33() real ext-real Element of REAL
((((seq_id (c₁ . m)) . (n + 1)) + ((- (seq_id (c₁ . u))) . (n + 1))) * (((seq_id (c₁ . m)) + (- (seq_id (c₁ . u)))) . (n + 1))) + (v . m) is V33() real ext-real Element of REAL
(((seq_id (c₁ . m)) . (n + 1)) + ((- (seq_id (c₁ . u))) . (n + 1))) * (((seq_id (c₁ . m)) . (n + 1)) + ((- (seq_id (c₁ . u))) . (n + 1))) is V33() real ext-real Element of REAL
((((seq_id (c₁ . m)) . (n + 1)) + ((- (seq_id (c₁ . u))) . (n + 1))) * (((seq_id (c₁ . m)) . (n + 1)) + ((- (seq_id (c₁ . u))) . (n + 1)))) + (v . m) is V33() real ext-real Element of REAL
(seq_id (c₁ . u)) . (n + 1) is V33() real ext-real Element of REAL
- ((seq_id (c₁ . u)) . (n + 1)) is V33() real ext-real Element of REAL
((seq_id (c₁ . m)) . (n + 1)) + (- ((seq_id (c₁ . u)) . (n + 1))) is V33() real ext-real Element of REAL
(((seq_id (c₁ . m)) . (n + 1)) + (- ((seq_id (c₁ . u)) . (n + 1)))) * (((seq_id (c₁ . m)) . (n + 1)) + ((- (seq_id (c₁ . u))) . (n + 1))) is V33() real ext-real Element of REAL
((((seq_id (c₁ . m)) . (n + 1)) + (- ((seq_id (c₁ . u)) . (n + 1)))) * (((seq_id (c₁ . m)) . (n + 1)) + ((- (seq_id (c₁ . u))) . (n + 1)))) + (v . m) is V33() real ext-real Element of REAL
((seq_id (c₁ . m)) . (n + 1)) - ((seq_id (c₁ . u)) . (n + 1)) is V33() real ext-real Element of REAL
(((seq_id (c₁ . m)) . (n + 1)) - ((seq_id (c₁ . u)) . (n + 1))) * (((seq_id (c₁ . m)) . (n + 1)) + (- ((seq_id (c₁ . u)) . (n + 1)))) is V33() real ext-real Element of REAL
((((seq_id (c₁ . m)) . (n + 1)) - ((seq_id (c₁ . u)) . (n + 1))) * (((seq_id (c₁ . m)) . (n + 1)) + (- ((seq_id (c₁ . u)) . (n + 1))))) + (v . m) is V33() real ext-real Element of REAL
y . m is V33() real ext-real Element of REAL
(y . m) - ((seq_id (c₁ . u)) . (n + 1)) is V33() real ext-real Element of REAL
((y . m) - ((seq_id (c₁ . u)) . (n + 1))) * (((seq_id (c₁ . m)) . (n + 1)) - ((seq_id (c₁ . u)) . (n + 1))) is V33() real ext-real Element of REAL
(((y . m) - ((seq_id (c₁ . u)) . (n + 1))) * (((seq_id (c₁ . m)) . (n + 1)) - ((seq_id (c₁ . u)) . (n + 1)))) + (v . m) is V33() real ext-real Element of REAL
((y . m) - ((seq_id (c₁ . u)) . (n + 1))) * ((y . m) - ((seq_id (c₁ . u)) . (n + 1))) is V33() real ext-real Element of REAL
(((y . m) - ((seq_id (c₁ . u)) . (n + 1))) * ((y . m) - ((seq_id (c₁ . u)) . (n + 1)))) + (v . m) is V33() real ext-real Element of REAL
(tseq . (n + 1)) + (- ((seq_id (c₁ . u)) . (n + 1))) is V33() real ext-real Element of REAL
(tseq . (n + 1)) - ((seq_id (c₁ . u)) . (n + 1)) is V33() real ext-real Element of REAL
((tseq . (n + 1)) + (- ((seq_id (c₁ . u)) . (n + 1)))) * ((tseq . (n + 1)) - ((seq_id (c₁ . u)) . (n + 1))) is V33() real ext-real Element of REAL
lim v is V33() real ext-real Element of REAL
(((tseq . (n + 1)) + (- ((seq_id (c₁ . u)) . (n + 1)))) * ((tseq . (n + 1)) - ((seq_id (c₁ . u)) . (n + 1)))) + (lim v) is V33() real ext-real Element of REAL
(tseq . (n + 1)) + ((- (seq_id (c₁ . u))) . (n + 1)) is V33() real ext-real Element of REAL
((tseq . (n + 1)) + ((- (seq_id (c₁ . u))) . (n + 1))) * ((tseq . (n + 1)) + (- ((seq_id (c₁ . u)) . (n + 1)))) is V33() real ext-real Element of REAL
(((tseq . (n + 1)) + ((- (seq_id (c₁ . u))) . (n + 1))) * ((tseq . (n + 1)) + (- ((seq_id (c₁ . u)) . (n + 1))))) + (lim v) is V33() real ext-real Element of REAL
((tseq . (n + 1)) + ((- (seq_id (c₁ . u))) . (n + 1))) * ((tseq . (n + 1)) + ((- (seq_id (c₁ . u))) . (n + 1))) is V33() real ext-real Element of REAL
(((tseq . (n + 1)) + ((- (seq_id (c₁ . u))) . (n + 1))) * ((tseq . (n + 1)) + ((- (seq_id (c₁ . u))) . (n + 1)))) + (lim v) is V33() real ext-real Element of REAL
tseq + (- (seq_id (c₁ . u))) is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
(tseq + (- (seq_id (c₁ . u)))) . (n + 1) is V33() real ext-real Element of REAL
((tseq + (- (seq_id (c₁ . u)))) . (n + 1)) * ((tseq . (n + 1)) + ((- (seq_id (c₁ . u))) . (n + 1))) is V33() real ext-real Element of REAL
(((tseq + (- (seq_id (c₁ . u)))) . (n + 1)) * ((tseq . (n + 1)) + ((- (seq_id (c₁ . u))) . (n + 1)))) + (lim v) is V33() real ext-real Element of REAL
((tseq + (- (seq_id (c₁ . u)))) . (n + 1)) * ((tseq + (- (seq_id (c₁ . u)))) . (n + 1)) is V33() real ext-real Element of REAL
(((tseq + (- (seq_id (c₁ . u)))) . (n + 1)) * ((tseq + (- (seq_id (c₁ . u)))) . (n + 1))) + (lim v) is V33() real ext-real Element of REAL
tseq - (seq_id (c₁ . u)) is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
(tseq - (seq_id (c₁ . u))) . (n + 1) is V33() real ext-real Element of REAL
((tseq - (seq_id (c₁ . u))) . (n + 1)) * ((tseq + (- (seq_id (c₁ . u)))) . (n + 1)) is V33() real ext-real Element of REAL
(((tseq - (seq_id (c₁ . u))) . (n + 1)) * ((tseq + (- (seq_id (c₁ . u)))) . (n + 1))) + (lim v) is V33() real ext-real Element of REAL
((tseq - (seq_id (c₁ . u))) . (n + 1)) * ((tseq - (seq_id (c₁ . u))) . (n + 1)) is V33() real ext-real Element of REAL
(((tseq - (seq_id (c₁ . u))) . (n + 1)) * ((tseq - (seq_id (c₁ . u))) . (n + 1))) + (lim v) is V33() real ext-real Element of REAL
(tseq - (seq_id (c₁ . u))) (#) (tseq - (seq_id (c₁ . u))) is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
((tseq - (seq_id (c₁ . u))) (#) (tseq - (seq_id (c₁ . u)))) . (n + 1) is V33() real ext-real Element of REAL
(((tseq - (seq_id (c₁ . u))) (#) (tseq - (seq_id (c₁ . u)))) . (n + 1)) + (lim v) is V33() real ext-real Element of REAL
(((tseq - (seq_id (c₁ . u))) (#) (tseq - (seq_id (c₁ . u)))) . (n + 1)) + ((Partial_Sums (((seq_id tseq) - (seq_id (c₁ . u))) (#) ((seq_id tseq) - (seq_id (c₁ . u))))) . n) is V33() real ext-real Element of REAL
(tseq - (seq_id (c₁ . u))) (#) ((seq_id tseq) - (seq_id (c₁ . u))) is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
((tseq - (seq_id (c₁ . u))) (#) ((seq_id tseq) - (seq_id (c₁ . u)))) . (n + 1) is V33() real ext-real Element of REAL
(((tseq - (seq_id (c₁ . u))) (#) ((seq_id tseq) - (seq_id (c₁ . u)))) . (n + 1)) + ((Partial_Sums (((seq_id tseq) - (seq_id (c₁ . u))) (#) ((seq_id tseq) - (seq_id (c₁ . u))))) . n) is V33() real ext-real Element of REAL
(((seq_id tseq) - (seq_id (c₁ . u))) (#) ((seq_id tseq) - (seq_id (c₁ . u)))) . (n + 1) is V33() real ext-real Element of REAL
((((seq_id tseq) - (seq_id (c₁ . u))) (#) ((seq_id tseq) - (seq_id (c₁ . u)))) . (n + 1)) + ((Partial_Sums (((seq_id tseq) - (seq_id (c₁ . u))) (#) ((seq_id tseq) - (seq_id (c₁ . u))))) . n) is V33() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V33() real ext-real non negative V38() V57() V58() V59() V60() V61() V62() V63() Element of NAT
(Partial_Sums (((seq_id tseq) - (seq_id (c₁ . u))) (#) ((seq_id tseq) - (seq_id (c₁ . u))))) . n is V33() real ext-real Element of REAL
v is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
n + 1 is V11() epsilon-transitive epsilon-connected ordinal natural V33() real ext-real positive non negative V38() V57() V58() V59() V60() V61() V62() V63() Element of NAT
lim v is V33() real ext-real Element of REAL
(Partial_Sums (((seq_id tseq) - (seq_id (c₁ . u))) (#) ((seq_id tseq) - (seq_id (c₁ . u))))) . (n + 1) is V33() real ext-real Element of REAL
n is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
lim n is V33() real ext-real Element of REAL
(Partial_Sums (((seq_id tseq) - (seq_id (c₁ . u))) (#) ((seq_id tseq) - (seq_id (c₁ . u))))) . 0 is V33() real ext-real Element of REAL
tseq . 0 is V33() real ext-real Element of REAL
v is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
lim v is V33() real ext-real Element of REAL
y is epsilon-transitive epsilon-connected ordinal natural V33() real ext-real non negative V38() V57() V58() V59() V60() V61() V62() V63() Element of NAT
n . y is V33() real ext-real Element of REAL
c₁ . y is Element of the carrier of l2_Space
(c₁ . y) - (c₁ . u) is Element of the carrier of l2_Space
- (c₁ . u) is Element of the carrier of l2_Space
(c₁ . y) + (- (c₁ . u)) is Element of the carrier of l2_Space
the addF of l2_Space is Relation-like [: the carrier of l2_Space, the carrier of l2_Space:] -defined the carrier of l2_Space -valued Function-like V14([: the carrier of l2_Space, the carrier of l2_Space:]) V18([: the carrier of l2_Space, the carrier of l2_Space:], the carrier of l2_Space) Element of bool [:[: the carrier of l2_Space, the carrier of l2_Space:], the carrier of l2_Space:]
[: the carrier of l2_Space, the carrier of l2_Space:] is set
[:[: the carrier of l2_Space, the carrier of l2_Space:], the carrier of l2_Space:] is set
bool [:[: the carrier of l2_Space, the carrier of l2_Space:], the carrier of l2_Space:] is set
the addF of l2_Space . ((c₁ . y),(- (c₁ . u))) is Element of the carrier of l2_Space
[(c₁ . y),(- (c₁ . u))] is set
the addF of l2_Space . [(c₁ . y),(- (c₁ . u))] is set
seq_id ((c₁ . y) - (c₁ . u)) is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
(seq_id ((c₁ . y) - (c₁ . u))) (#) (seq_id ((c₁ . y) - (c₁ . u))) is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
Partial_Sums ((seq_id ((c₁ . y) - (c₁ . u))) (#) (seq_id ((c₁ . y) - (c₁ . u)))) is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
(Partial_Sums ((seq_id ((c₁ . y) - (c₁ . u))) (#) (seq_id ((c₁ . y) - (c₁ . u))))) . 0 is V33() real ext-real Element of REAL
((seq_id ((c₁ . y) - (c₁ . u))) (#) (seq_id ((c₁ . y) - (c₁ . u)))) . 0 is V33() real ext-real Element of REAL
seq_id (c₁ . y) is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
(seq_id (c₁ . y)) - (seq_id (c₁ . u)) is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
((seq_id (c₁ . y)) - (seq_id (c₁ . u))) (#) (seq_id ((c₁ . y) - (c₁ . u))) is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
(((seq_id (c₁ . y)) - (seq_id (c₁ . u))) (#) (seq_id ((c₁ . y) - (c₁ . u)))) . 0 is V33() real ext-real Element of REAL
((seq_id (c₁ . y)) - (seq_id (c₁ . u))) (#) ((seq_id (c₁ . y)) - (seq_id (c₁ . u))) is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
(((seq_id (c₁ . y)) - (seq_id (c₁ . u))) (#) ((seq_id (c₁ . y)) - (seq_id (c₁ . u)))) . 0 is V33() real ext-real Element of REAL
((seq_id (c₁ . y)) - (seq_id (c₁ . u))) . 0 is V33() real ext-real Element of REAL
(((seq_id (c₁ . y)) - (seq_id (c₁ . u))) . 0) * (((seq_id (c₁ . y)) - (seq_id (c₁ . u))) . 0) is V33() real ext-real Element of REAL
- (seq_id (c₁ . u)) is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
(seq_id (c₁ . y)) + (- (seq_id (c₁ . u))) is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
((seq_id (c₁ . y)) + (- (seq_id (c₁ . u)))) . 0 is V33() real ext-real Element of REAL
(((seq_id (c₁ . y)) + (- (seq_id (c₁ . u)))) . 0) * (((seq_id (c₁ . y)) - (seq_id (c₁ . u))) . 0) is V33() real ext-real Element of REAL
(((seq_id (c₁ . y)) + (- (seq_id (c₁ . u)))) . 0) * (((seq_id (c₁ . y)) + (- (seq_id (c₁ . u)))) . 0) is V33() real ext-real Element of REAL
(seq_id (c₁ . y)) . 0 is V33() real ext-real Element of REAL
(- (seq_id (c₁ . u))) . 0 is V33() real ext-real Element of REAL
((seq_id (c₁ . y)) . 0) + ((- (seq_id (c₁ . u))) . 0) is V33() real ext-real Element of REAL
(((seq_id (c₁ . y)) . 0) + ((- (seq_id (c₁ . u))) . 0)) * (((seq_id (c₁ . y)) + (- (seq_id (c₁ . u)))) . 0) is V33() real ext-real Element of REAL
(((seq_id (c₁ . y)) . 0) + ((- (seq_id (c₁ . u))) . 0)) * (((seq_id (c₁ . y)) . 0) + ((- (seq_id (c₁ . u))) . 0)) is V33() real ext-real Element of REAL
(seq_id (c₁ . u)) . 0 is V33() real ext-real Element of REAL
- ((seq_id (c₁ . u)) . 0) is V33() real ext-real Element of REAL
((seq_id (c₁ . y)) . 0) + (- ((seq_id (c₁ . u)) . 0)) is V33() real ext-real Element of REAL
(((seq_id (c₁ . y)) . 0) + (- ((seq_id (c₁ . u)) . 0))) * (((seq_id (c₁ . y)) . 0) + ((- (seq_id (c₁ . u))) . 0)) is V33() real ext-real Element of REAL
((seq_id (c₁ . y)) . 0) - ((seq_id (c₁ . u)) . 0) is V33() real ext-real Element of REAL
(((seq_id (c₁ . y)) . 0) - ((seq_id (c₁ . u)) . 0)) * (((seq_id (c₁ . y)) . 0) + (- ((seq_id (c₁ . u)) . 0))) is V33() real ext-real Element of REAL
v . y is V33() real ext-real Element of REAL
(v . y) - ((seq_id (c₁ . u)) . 0) is V33() real ext-real Element of REAL
((v . y) - ((seq_id (c₁ . u)) . 0)) * (((seq_id (c₁ . y)) . 0) - ((seq_id (c₁ . u)) . 0)) is V33() real ext-real Element of REAL
((v . y) - ((seq_id (c₁ . u)) . 0)) * ((v . y) - ((seq_id (c₁ . u)) . 0)) is V33() real ext-real Element of REAL
(tseq . 0) + (- ((seq_id (c₁ . u)) . 0)) is V33() real ext-real Element of REAL
(tseq . 0) - ((seq_id (c₁ . u)) . 0) is V33() real ext-real Element of REAL
((tseq . 0) + (- ((seq_id (c₁ . u)) . 0))) * ((tseq . 0) - ((seq_id (c₁ . u)) . 0)) is V33() real ext-real Element of REAL
(tseq . 0) + ((- (seq_id (c₁ . u))) . 0) is V33() real ext-real Element of REAL
((tseq . 0) + ((- (seq_id (c₁ . u))) . 0)) * ((tseq . 0) + (- ((seq_id (c₁ . u)) . 0))) is V33() real ext-real Element of REAL
((tseq . 0) + ((- (seq_id (c₁ . u))) . 0)) * ((tseq . 0) + ((- (seq_id (c₁ . u))) . 0)) is V33() real ext-real Element of REAL
tseq + (- (seq_id (c₁ . u))) is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
(tseq + (- (seq_id (c₁ . u)))) . 0 is V33() real ext-real Element of REAL
((tseq + (- (seq_id (c₁ . u)))) . 0) * ((tseq . 0) + ((- (seq_id (c₁ . u))) . 0)) is V33() real ext-real Element of REAL
((tseq + (- (seq_id (c₁ . u)))) . 0) * ((tseq + (- (seq_id (c₁ . u)))) . 0) is V33() real ext-real Element of REAL
tseq - (seq_id (c₁ . u)) is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
(tseq - (seq_id (c₁ . u))) . 0 is V33() real ext-real Element of REAL
((tseq - (seq_id (c₁ . u))) . 0) * ((tseq + (- (seq_id (c₁ . u)))) . 0) is V33() real ext-real Element of REAL
((tseq - (seq_id (c₁ . u))) . 0) * ((tseq - (seq_id (c₁ . u))) . 0) is V33() real ext-real Element of REAL
(tseq - (seq_id (c₁ . u))) (#) (tseq - (seq_id (c₁ . u))) is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
((tseq - (seq_id (c₁ . u))) (#) (tseq - (seq_id (c₁ . u)))) . 0 is V33() real ext-real Element of REAL
Partial_Sums ((tseq - (seq_id (c₁ . u))) (#) (tseq - (seq_id (c₁ . u)))) is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
(Partial_Sums ((tseq - (seq_id (c₁ . u))) (#) (tseq - (seq_id (c₁ . u))))) . 0 is V33() real ext-real Element of REAL
((seq_id tseq) - (seq_id (c₁ . u))) (#) (tseq - (seq_id (c₁ . u))) is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
Partial_Sums (((seq_id tseq) - (seq_id (c₁ . u))) (#) (tseq - (seq_id (c₁ . u)))) is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
(Partial_Sums (((seq_id tseq) - (seq_id (c₁ . u))) (#) (tseq - (seq_id (c₁ . u))))) . 0 is V33() real ext-real Element of REAL
n is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
lim n is V33() real ext-real Element of REAL
v is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
n is epsilon-transitive epsilon-connected ordinal natural V33() real ext-real non negative V38() V57() V58() V59() V60() V61() V62() V63() Element of NAT
lim v is V33() real ext-real Element of REAL
(Partial_Sums (((seq_id tseq) - (seq_id (c₁ . u))) (#) ((seq_id tseq) - (seq_id (c₁ . u))))) . n is V33() real ext-real Element of REAL
u is epsilon-transitive epsilon-connected ordinal natural V33() real ext-real non negative V38() V57() V58() V59() V60() V61() V62() V63() Element of NAT
c₁ . u is Element of the carrier of l2_Space
seq_id (c₁ . u) is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
(seq_id tseq) - (seq_id (c₁ . u)) is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
((seq_id tseq) - (seq_id (c₁ . u))) (#) ((seq_id tseq) - (seq_id (c₁ . u))) is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
Sum (((seq_id tseq) - (seq_id (c₁ . u))) (#) ((seq_id tseq) - (seq_id (c₁ . u)))) is V33() real ext-real Element of REAL
Partial_Sums (((seq_id tseq) - (seq_id (c₁ . u))) (#) ((seq_id tseq) - (seq_id (c₁ . u)))) is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
n is epsilon-transitive epsilon-connected ordinal natural V33() real ext-real non negative V38() V57() V58() V59() V60() V61() V62() V63() Element of NAT
(Partial_Sums (((seq_id tseq) - (seq_id (c₁ . u))) (#) ((seq_id tseq) - (seq_id (c₁ . u))))) . n is V33() real ext-real Element of REAL
v is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
y is epsilon-transitive epsilon-connected ordinal natural V33() real ext-real non negative V38() V57() V58() V59() V60() V61() V62() V63() Element of NAT
v . y is V33() real ext-real Element of REAL
c₁ . y is Element of the carrier of l2_Space
(c₁ . y) - (c₁ . u) is Element of the carrier of l2_Space
- (c₁ . u) is Element of the carrier of l2_Space
(c₁ . y) + (- (c₁ . u)) is Element of the carrier of l2_Space
the addF of l2_Space is Relation-like [: the carrier of l2_Space, the carrier of l2_Space:] -defined the carrier of l2_Space -valued Function-like V14([: the carrier of l2_Space, the carrier of l2_Space:]) V18([: the carrier of l2_Space, the carrier of l2_Space:], the carrier of l2_Space) Element of bool [:[: the carrier of l2_Space, the carrier of l2_Space:], the carrier of l2_Space:]
[: the carrier of l2_Space, the carrier of l2_Space:] is set
[:[: the carrier of l2_Space, the carrier of l2_Space:], the carrier of l2_Space:] is set
bool [:[: the carrier of l2_Space, the carrier of l2_Space:], the carrier of l2_Space:] is set
the addF of l2_Space . ((c₁ . y),(- (c₁ . u))) is Element of the carrier of l2_Space
[(c₁ . y),(- (c₁ . u))] is set
the addF of l2_Space . [(c₁ . y),(- (c₁ . u))] is set
seq_id ((c₁ . y) - (c₁ . u)) is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
(seq_id ((c₁ . y) - (c₁ . u))) (#) (seq_id ((c₁ . y) - (c₁ . u))) is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
rseq is epsilon-transitive epsilon-connected ordinal natural V33() real ext-real non negative V38() V57() V58() V59() V60() V61() V62() V63() Element of NAT
((seq_id ((c₁ . y) - (c₁ . u))) (#) (seq_id ((c₁ . y) - (c₁ . u)))) . rseq is V33() real ext-real Element of REAL
Partial_Sums ((seq_id ((c₁ . y) - (c₁ . u))) (#) (seq_id ((c₁ . y) - (c₁ . u)))) is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
(Partial_Sums ((seq_id ((c₁ . y) - (c₁ . u))) (#) (seq_id ((c₁ . y) - (c₁ . u))))) . n is V33() real ext-real Element of REAL
Sum ((seq_id ((c₁ . y) - (c₁ . u))) (#) (seq_id ((c₁ . y) - (c₁ . u)))) is V33() real ext-real Element of REAL
lim v is V33() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V33() real ext-real non negative V38() V57() V58() V59() V60() V61() V62() V63() Element of NAT
(Partial_Sums (((seq_id tseq) - (seq_id (c₁ . u))) (#) ((seq_id tseq) - (seq_id (c₁ . u))))) . n is V33() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V33() real ext-real non negative V38() V57() V58() V59() V60() V61() V62() V63() Element of NAT
(((seq_id tseq) - (seq_id (c₁ . u))) (#) ((seq_id tseq) - (seq_id (c₁ . u)))) . n is V33() real ext-real Element of REAL
((seq_id tseq) - (seq_id (c₁ . u))) . n is V33() real ext-real Element of REAL
(((seq_id tseq) - (seq_id (c₁ . u))) . n) * (((seq_id tseq) - (seq_id (c₁ . u))) . n) is V33() real ext-real Element of REAL
lim (Partial_Sums (((seq_id tseq) - (seq_id (c₁ . u))) (#) ((seq_id tseq) - (seq_id (c₁ . u))))) is V33() real ext-real Element of REAL
(seq_id tseq) (#) (seq_id tseq) is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
e is epsilon-transitive epsilon-connected ordinal natural V33() real ext-real non negative V38() V57() V58() V59() V60() V61() V62() V63() Element of NAT
((seq_id tseq) (#) (seq_id tseq)) . e is V33() real ext-real Element of REAL
(seq_id tseq) . e is V33() real ext-real Element of REAL
((seq_id tseq) . e) * ((seq_id tseq) . e) is V33() real ext-real Element of REAL
1 * 1 is epsilon-transitive epsilon-connected ordinal natural V33() real ext-real non negative V38() V57() V58() V59() V60() V61() V62() V63() Element of NAT
e is epsilon-transitive epsilon-connected ordinal natural V33() real ext-real non negative V38() V57() V58() V59() V60() V61() V62() V63() Element of NAT
c₁ . e is Element of the carrier of l2_Space
seq_id (c₁ . e) is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
(seq_id (c₁ . e)) (#) (seq_id (c₁ . e)) is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
(seq_id tseq) - (seq_id (c₁ . e)) is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
((seq_id tseq) - (seq_id (c₁ . e))) (#) ((seq_id tseq) - (seq_id (c₁ . e))) is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
2 (#) ((seq_id (c₁ . e)) (#) (seq_id (c₁ . e))) is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
2 (#) (((seq_id tseq) - (seq_id (c₁ . e))) (#) ((seq_id tseq) - (seq_id (c₁ . e)))) is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
(2 (#) (((seq_id tseq) - (seq_id (c₁ . e))) (#) ((seq_id tseq) - (seq_id (c₁ . e))))) + (2 (#) ((seq_id (c₁ . e)) (#) (seq_id (c₁ . e)))) is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
n is epsilon-transitive epsilon-connected ordinal natural V33() real ext-real non negative V38() V57() V58() V59() V60() V61() V62() V63() Element of NAT
((seq_id tseq) (#) (seq_id tseq)) . n is V33() real ext-real Element of REAL
((2 (#) (((seq_id tseq) - (seq_id (c₁ . e))) (#) ((seq_id tseq) - (seq_id (c₁ . e))))) + (2 (#) ((seq_id (c₁ . e)) (#) (seq_id (c₁ . e))))) . n is V33() real ext-real Element of REAL
(seq_id tseq) . n is V33() real ext-real Element of REAL
(seq_id (c₁ . e)) . n is V33() real ext-real Element of REAL
((seq_id (c₁ . e)) (#) (seq_id (c₁ . e))) . n is V33() real ext-real Element of REAL
2 * (((seq_id (c₁ . e)) (#) (seq_id (c₁ . e))) . n) is V33() real ext-real Element of REAL
((seq_id (c₁ . e)) . n) * ((seq_id (c₁ . e)) . n) is V33() real ext-real Element of REAL
2 * (((seq_id (c₁ . e)) . n) * ((seq_id (c₁ . e)) . n)) is V33() real ext-real Element of REAL
2 * ((seq_id (c₁ . e)) . n) is V33() real ext-real Element of REAL
(2 * ((seq_id (c₁ . e)) . n)) * ((seq_id (c₁ . e)) . n) is V33() real ext-real Element of REAL
((seq_id tseq) - (seq_id (c₁ . e))) . n is V33() real ext-real Element of REAL
- (seq_id (c₁ . e)) is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
(seq_id tseq) + (- (seq_id (c₁ . e))) is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
((seq_id tseq) + (- (seq_id (c₁ . e)))) . n is V33() real ext-real Element of REAL
(- (seq_id (c₁ . e))) . n is V33() real ext-real Element of REAL
((seq_id tseq) . n) + ((- (seq_id (c₁ . e))) . n) is V33() real ext-real Element of REAL
- ((seq_id (c₁ . e)) . n) is V33() real ext-real Element of REAL
((seq_id tseq) . n) + (- ((seq_id (c₁ . e)) . n)) is V33() real ext-real Element of REAL
((seq_id tseq) . n) - ((seq_id (c₁ . e)) . n) is V33() real ext-real Element of REAL
(((seq_id tseq) - (seq_id (c₁ . e))) (#) ((seq_id tseq) - (seq_id (c₁ . e)))) . n is V33() real ext-real Element of REAL
(((seq_id tseq) . n) - ((seq_id (c₁ . e)) . n)) * (((seq_id tseq) . n) - ((seq_id (c₁ . e)) . n)) is V33() real ext-real Element of REAL
((seq_id tseq) . n) * ((seq_id tseq) . n) is V33() real ext-real Element of REAL
2 * ((((seq_id tseq) - (seq_id (c₁ . e))) (#) ((seq_id tseq) - (seq_id (c₁ . e)))) . n) is V33() real ext-real Element of REAL
2 * (((seq_id tseq) . n) - ((seq_id (c₁ . e)) . n)) is V33() real ext-real Element of REAL
(2 * (((seq_id tseq) . n) - ((seq_id (c₁ . e)) . n))) * (((seq_id tseq) . n) - ((seq_id (c₁ . e)) . n)) is V33() real ext-real Element of REAL
(2 (#) (((seq_id tseq) - (seq_id (c₁ . e))) (#) ((seq_id tseq) - (seq_id (c₁ . e))))) . n is V33() real ext-real Element of REAL
(2 (#) ((seq_id (c₁ . e)) (#) (seq_id (c₁ . e)))) . n is V33() real ext-real Element of REAL
((2 (#) (((seq_id tseq) - (seq_id (c₁ . e))) (#) ((seq_id tseq) - (seq_id (c₁ . e))))) . n) + ((2 (#) ((seq_id (c₁ . e)) (#) (seq_id (c₁ . e)))) . n) is V33() real ext-real Element of REAL
(2 * ((((seq_id tseq) - (seq_id (c₁ . e))) (#) ((seq_id tseq) - (seq_id (c₁ . e)))) . n)) + ((2 (#) ((seq_id (c₁ . e)) (#) (seq_id (c₁ . e)))) . n) is V33() real ext-real Element of REAL
(2 * ((((seq_id tseq) - (seq_id (c₁ . e))) (#) ((seq_id tseq) - (seq_id (c₁ . e)))) . n)) + (2 * (((seq_id (c₁ . e)) (#) (seq_id (c₁ . e))) . n)) is V33() real ext-real Element of REAL
tv is Element of the carrier of l2_Space
e is V33() real ext-real Element of REAL
e * e is V33() real ext-real Element of REAL
m is epsilon-transitive epsilon-connected ordinal natural V33() real ext-real non negative V38() V57() V58() V59() V60() V61() V62() V63() Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V33() real ext-real non negative V38() V57() V58() V59() V60() V61() V62() V63() Element of NAT
c₁ . n is Element of the carrier of l2_Space
seq_id (c₁ . n) is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
(seq_id tseq) - (seq_id (c₁ . n)) is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
((seq_id tseq) - (seq_id (c₁ . n))) (#) ((seq_id tseq) - (seq_id (c₁ . n))) is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
Sum (((seq_id tseq) - (seq_id (c₁ . n))) (#) ((seq_id tseq) - (seq_id (c₁ . n)))) is V33() real ext-real Element of REAL
u is Element of the carrier of l2_Space
v is Element of the carrier of l2_Space
u - v is Element of the carrier of l2_Space
- v is Element of the carrier of l2_Space
u + (- v) is Element of the carrier of l2_Space
the addF of l2_Space is Relation-like [: the carrier of l2_Space, the carrier of l2_Space:] -defined the carrier of l2_Space -valued Function-like V14([: the carrier of l2_Space, the carrier of l2_Space:]) V18([: the carrier of l2_Space, the carrier of l2_Space:], the carrier of l2_Space) Element of bool [:[: the carrier of l2_Space, the carrier of l2_Space:], the carrier of l2_Space:]
[: the carrier of l2_Space, the carrier of l2_Space:] is set
[:[: the carrier of l2_Space, the carrier of l2_Space:], the carrier of l2_Space:] is set
bool [:[: the carrier of l2_Space, the carrier of l2_Space:], the carrier of l2_Space:] is set
the addF of l2_Space . (u,(- v)) is Element of the carrier of l2_Space
[u,(- v)] is set
the addF of l2_Space . [u,(- v)] is set
seq_id (u - v) is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
(u - v) .|. (u - v) is V33() real ext-real Element of REAL
(c₁ . n) - tv is Element of the carrier of l2_Space
- tv is Element of the carrier of l2_Space
(c₁ . n) + (- tv) is Element of the carrier of l2_Space
the addF of l2_Space . ((c₁ . n),(- tv)) is Element of the carrier of l2_Space
[(c₁ . n),(- tv)] is set
the addF of l2_Space . [(c₁ . n),(- tv)] is set
||.((c₁ . n) - tv).|| is V33() real ext-real Element of REAL
tv - (c₁ . n) is Element of the carrier of l2_Space
- (c₁ . n) is Element of the carrier of l2_Space
tv + (- (c₁ . n)) is Element of the carrier of l2_Space
the addF of l2_Space . (tv,(- (c₁ . n))) is Element of the carrier of l2_Space
[tv,(- (c₁ . n))] is set
the addF of l2_Space . [tv,(- (c₁ . n))] is set
- (tv - (c₁ . n)) is Element of the carrier of l2_Space
||.(- (tv - (c₁ . n))).|| is V33() real ext-real Element of REAL
||.(tv - (c₁ . n)).|| is V33() real ext-real Element of REAL
sqrt ((u - v) .|. (u - v)) is V33() real ext-real Element of REAL
e ^2 is V33() real ext-real Element of REAL
e * e is V33() real ext-real set
sqrt (e ^2) is V33() real ext-real Element of REAL
c₁ is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
Partial_Sums c₁ is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
f is epsilon-transitive epsilon-connected ordinal natural V33() real ext-real non negative V38() V57() V58() V59() V60() V61() V62() V63() Element of NAT
(Partial_Sums c₁) . f is V33() real ext-real Element of REAL
tseq is epsilon-transitive epsilon-connected ordinal natural V33() real ext-real non negative V38() V57() V58() V59() V60() V61() V62() V63() Element of NAT
c₁ . tseq is V33() real ext-real Element of REAL
(Partial_Sums c₁) . tseq is V33() real ext-real Element of REAL
tv is epsilon-transitive epsilon-connected ordinal natural V33() real ext-real non negative V38() V57() V58() V59() V60() V61() V62() V63() Element of NAT
(Partial_Sums c₁) . tv is V33() real ext-real Element of REAL
Sum c₁ is V33() real ext-real Element of REAL
e is epsilon-transitive epsilon-connected ordinal natural V33() real ext-real non negative V38() V57() V58() V59() V60() V61() V62() V63() Element of NAT
c₁ . e is V33() real ext-real Element of REAL
c₁ is V33() real ext-real Element of REAL
f is V33() real ext-real Element of REAL
c₁ + f is V33() real ext-real Element of REAL
(c₁ + f) * (c₁ + f) is V33() real ext-real Element of REAL
2 * c₁ is V33() real ext-real Element of REAL
(2 * c₁) * c₁ is V33() real ext-real Element of REAL
2 * f is V33() real ext-real Element of REAL
(2 * f) * f is V33() real ext-real Element of REAL
((2 * c₁) * c₁) + ((2 * f) * f) is V33() real ext-real Element of REAL
tseq is V33() real ext-real Element of REAL
tseq * tseq is V33() real ext-real Element of REAL
tv is V33() real ext-real Element of REAL
tseq - tv is V33() real ext-real Element of REAL
2 * (tseq - tv) is V33() real ext-real Element of REAL
(2 * (tseq - tv)) * (tseq - tv) is V33() real ext-real Element of REAL
2 * tv is V33() real ext-real Element of REAL
(2 * tv) * tv is V33() real ext-real Element of REAL
((2 * (tseq - tv)) * (tseq - tv)) + ((2 * tv) * tv) is V33() real ext-real Element of REAL
f is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
tseq is epsilon-transitive epsilon-connected ordinal natural V33() real ext-real non negative V38() V57() V58() V59() V60() V61() V62() V63() Element of NAT
c₁ is V33() real ext-real Element of REAL
lim f is V33() real ext-real Element of REAL
f is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
tseq is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
c₁ is V33() real ext-real Element of REAL
lim tseq is V33() real ext-real Element of REAL
lim f is V33() real ext-real Element of REAL
(lim f) - c₁ is V33() real ext-real Element of REAL
((lim f) - c₁) * ((lim f) - c₁) is V33() real ext-real Element of REAL
f is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
tseq is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
tv is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) V40() V41() V42() Element of bool [:NAT,REAL:]
c₁ is V33() real ext-real Element of REAL
lim tv is V33() real ext-real Element of REAL
lim f is V33() real ext-real Element of REAL
(lim f) - c₁ is V33() real ext-real Element of REAL
((lim f) - c₁) * ((lim f) - c₁) is V33() real ext-real Element of REAL
lim tseq is V33() real ext-real Element of REAL
(((lim f) - c₁) * ((lim f) - c₁)) + (lim tseq) is V33() real ext-real Element of REAL