REAL is non empty V30() V115() V116() V117() V121() set
NAT is non empty epsilon-transitive epsilon-connected ordinal V115() V116() V117() V118() V119() V120() V121() Element of bool REAL
bool REAL is non empty set
COMPLEX is non empty V30() V115() V121() set
omega is non empty epsilon-transitive epsilon-connected ordinal V115() V116() V117() V118() V119() V120() V121() set
bool omega is non empty set
bool NAT is non empty set
ExtREAL is non empty V116() set
[:NAT,REAL:] is non empty Relation-like V105() V106() V107() set
bool [:NAT,REAL:] is non empty set
the_set_of_RealSequences is non empty set
[:the_set_of_RealSequences,the_set_of_RealSequences:] is non empty Relation-like set
[:[:the_set_of_RealSequences,the_set_of_RealSequences:],the_set_of_RealSequences:] is non empty Relation-like set
bool [:[:the_set_of_RealSequences,the_set_of_RealSequences:],the_set_of_RealSequences:] is non empty set
[:REAL,the_set_of_RealSequences:] is non empty Relation-like set
[:[:REAL,the_set_of_RealSequences:],the_set_of_RealSequences:] is non empty Relation-like set
bool [:[:REAL,the_set_of_RealSequences:],the_set_of_RealSequences:] is non empty set
Linear_Space_of_RealSequences is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() RLSStruct
the carrier of Linear_Space_of_RealSequences is non empty set
bool the carrier of Linear_Space_of_RealSequences is non empty set
the_set_of_l2RealSequences is non empty linearly-closed Element of bool the carrier of Linear_Space_of_RealSequences
[:the_set_of_l2RealSequences,the_set_of_l2RealSequences:] is non empty Relation-like set
[:[:the_set_of_l2RealSequences,the_set_of_l2RealSequences:],REAL:] is non empty Relation-like V105() V106() V107() set
bool [:[:the_set_of_l2RealSequences,the_set_of_l2RealSequences:],REAL:] is non empty set
the_set_of_l1RealSequences is non empty linearly-closed Element of bool the carrier of Linear_Space_of_RealSequences
[:the_set_of_l1RealSequences,REAL:] is non empty Relation-like V105() V106() V107() set
bool [:the_set_of_l1RealSequences,REAL:] is non empty set
RAT is non empty V30() V115() V116() V117() V118() V121() set
INT is non empty V30() V115() V116() V117() V118() V119() V121() set
[:REAL,REAL:] is non empty Relation-like V105() V106() V107() set
bool [:REAL,REAL:] is non empty set
[:COMPLEX,COMPLEX:] is non empty Relation-like V105() set
bool [:COMPLEX,COMPLEX:] is non empty set
[:COMPLEX,REAL:] is non empty Relation-like V105() V106() V107() set
bool [:COMPLEX,REAL:] is non empty set
[:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty Relation-like V105() set
bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty set
[:[:REAL,REAL:],REAL:] is non empty Relation-like V105() V106() V107() set
bool [:[:REAL,REAL:],REAL:] is non empty set
[:RAT,RAT:] is non empty Relation-like RAT -valued V105() V106() V107() set
bool [:RAT,RAT:] is non empty set
[:[:RAT,RAT:],RAT:] is non empty Relation-like RAT -valued V105() V106() V107() set
bool [:[:RAT,RAT:],RAT:] is non empty set
[:INT,INT:] is non empty Relation-like RAT -valued INT -valued V105() V106() V107() set
bool [:INT,INT:] is non empty set
[:[:INT,INT:],INT:] is non empty Relation-like RAT -valued INT -valued V105() V106() V107() set
bool [:[:INT,INT:],INT:] is non empty set
[:NAT,NAT:] is non empty Relation-like RAT -valued INT -valued V105() V106() V107() V108() set
[:[:NAT,NAT:],NAT:] is non empty Relation-like RAT -valued INT -valued V105() V106() V107() V108() set
bool [:[:NAT,NAT:],NAT:] is non empty set
{} is set
the empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real Relation-like non-empty empty-yielding RAT -valued ext-real non positive non negative V105() V106() V107() V108() V115() V116() V117() V118() V119() V120() V121() set is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real Relation-like non-empty empty-yielding RAT -valued ext-real non positive non negative V105() V106() V107() V108() V115() V116() V117() V118() V119() V120() V121() set
1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V115() V116() V117() V118() V119() V120() V145() V168() Element of NAT
0 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V115() V116() V117() V118() V119() V120() V145() V168() Element of NAT
- 1 is V11() real ext-real non positive Element of REAL
Zeroseq is Element of the_set_of_RealSequences
l_add is non empty Relation-like [:the_set_of_RealSequences,the_set_of_RealSequences:] -defined the_set_of_RealSequences -valued Function-like V23([:the_set_of_RealSequences,the_set_of_RealSequences:]) quasi_total Element of bool [:[:the_set_of_RealSequences,the_set_of_RealSequences:],the_set_of_RealSequences:]
l_mult is non empty Relation-like [:REAL,the_set_of_RealSequences:] -defined the_set_of_RealSequences -valued Function-like V23([:REAL,the_set_of_RealSequences:]) quasi_total Element of bool [:[:REAL,the_set_of_RealSequences:],the_set_of_RealSequences:]
RLSStruct(# the_set_of_RealSequences,Zeroseq,l_add,l_mult #) is non empty strict Abelian RLSStruct
the carrier of RLSStruct(# the_set_of_RealSequences,Zeroseq,l_add,l_mult #) is non empty set
2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V115() V116() V117() V118() V119() V120() V145() V168() Element of NAT
X is non empty Relation-like NAT -defined REAL -valued Function-like V23( NAT ) quasi_total V105() V106() V107() Element of bool [:NAT,REAL:]
rng X is non empty V115() V116() V117() Element of bool REAL
upper_bound (rng X) is V11() real ext-real Element of REAL
Y is V11() real ext-real set
vseq is V11() real ext-real set
f is set
X . f is V11() real ext-real Element of REAL
X is non empty Relation-like NAT -defined REAL -valued Function-like V23( NAT ) quasi_total V105() V106() V107() Element of bool [:NAT,REAL:]
rng X is non empty V115() V116() V117() Element of bool REAL
upper_bound (rng X) is V11() real ext-real Element of REAL
Y is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V115() V116() V117() V118() V119() V120() V145() V168() Element of NAT
X . Y is V11() real ext-real Element of REAL
dom X is non empty V115() V116() V117() V118() V119() V120() Element of bool NAT
X is set
Y is set
bool the_set_of_RealSequences is non empty set
X is Element of bool the carrier of Linear_Space_of_RealSequences
Y is Element of bool the carrier of Linear_Space_of_RealSequences
vseq is set
seq_id vseq is non empty Relation-like NAT -defined REAL -valued Function-like V23( NAT ) quasi_total V105() V106() V107() Element of bool [:NAT,REAL:]
vseq is set
seq_id vseq is non empty Relation-like NAT -defined REAL -valued Function-like V23( NAT ) quasi_total V105() V106() V107() Element of bool [:NAT,REAL:]
() is Element of bool the carrier of Linear_Space_of_RealSequences
seq_id Zeroseq is non empty Relation-like NAT -defined REAL -valued Function-like V23( NAT ) quasi_total V105() V106() V107() Element of bool [:NAT,REAL:]
X is non empty Relation-like NAT -defined REAL -valued Function-like V23( NAT ) quasi_total V105() V106() V107() Element of bool [:NAT,REAL:]
Y is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real set
X . Y is V11() real ext-real Element of REAL
Y is V11() real ext-real Element of REAL
vseq is Element of the carrier of Linear_Space_of_RealSequences
Y * vseq is Element of the carrier of Linear_Space_of_RealSequences
the Mult of Linear_Space_of_RealSequences is non empty Relation-like [:REAL, the carrier of Linear_Space_of_RealSequences:] -defined the carrier of Linear_Space_of_RealSequences -valued Function-like V23([:REAL, the carrier of Linear_Space_of_RealSequences:]) quasi_total 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 non empty Relation-like set
[:[:REAL, the carrier of Linear_Space_of_RealSequences:], the carrier of Linear_Space_of_RealSequences:] is non empty Relation-like set
bool [:[:REAL, the carrier of Linear_Space_of_RealSequences:], the carrier of Linear_Space_of_RealSequences:] is non empty set
K580( the Mult of Linear_Space_of_RealSequences,Y,vseq) is set
[Y,vseq] is set
{Y,vseq} is set
{Y} is V115() V116() V117() set
{{Y,vseq},{Y}} is set
the Mult of Linear_Space_of_RealSequences . [Y,vseq] is set
seq_id vseq is non empty Relation-like NAT -defined REAL -valued Function-like V23( NAT ) quasi_total V105() V106() V107() Element of bool [:NAT,REAL:]
seq_id (Y * vseq) is non empty Relation-like NAT -defined REAL -valued Function-like V23( NAT ) quasi_total V105() V106() V107() Element of bool [:NAT,REAL:]
Y (#) (seq_id vseq) is non empty Relation-like NAT -defined REAL -valued Function-like V23( NAT ) quasi_total V105() V106() V107() Element of bool [:NAT,REAL:]
seq_id (Y (#) (seq_id vseq)) is non empty Relation-like NAT -defined REAL -valued Function-like V23( NAT ) quasi_total V105() V106() V107() Element of bool [:NAT,REAL:]
Y is Element of the carrier of Linear_Space_of_RealSequences
vseq is Element of the carrier of Linear_Space_of_RealSequences
Y + vseq is Element of the carrier of Linear_Space_of_RealSequences
the addF of Linear_Space_of_RealSequences is non empty 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 V23([: the carrier of Linear_Space_of_RealSequences, the carrier of Linear_Space_of_RealSequences:]) quasi_total 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 non empty Relation-like set
[:[: the carrier of Linear_Space_of_RealSequences, the carrier of Linear_Space_of_RealSequences:], the carrier of Linear_Space_of_RealSequences:] is non empty Relation-like set
bool [:[: the carrier of Linear_Space_of_RealSequences, the carrier of Linear_Space_of_RealSequences:], the carrier of Linear_Space_of_RealSequences:] is non empty set
K584( the carrier of Linear_Space_of_RealSequences, the addF of Linear_Space_of_RealSequences,Y,vseq) is Element of the carrier of Linear_Space_of_RealSequences
[Y,vseq] is set
{Y,vseq} is set
{Y} is set
{{Y,vseq},{Y}} is set
the addF of Linear_Space_of_RealSequences . [Y,vseq] is set
seq_id Y is non empty Relation-like NAT -defined REAL -valued Function-like V23( NAT ) quasi_total V105() V106() V107() Element of bool [:NAT,REAL:]
seq_id vseq is non empty Relation-like NAT -defined REAL -valued Function-like V23( NAT ) quasi_total V105() V106() V107() Element of bool [:NAT,REAL:]
seq_id (Y + vseq) is non empty Relation-like NAT -defined REAL -valued Function-like V23( NAT ) quasi_total V105() V106() V107() Element of bool [:NAT,REAL:]
(seq_id Y) + (seq_id vseq) is non empty Relation-like NAT -defined REAL -valued Function-like V23( NAT ) quasi_total V105() V106() V107() Element of bool [:NAT,REAL:]
seq_id ((seq_id Y) + (seq_id vseq)) is non empty Relation-like NAT -defined REAL -valued Function-like V23( NAT ) quasi_total V105() V106() V107() Element of bool [:NAT,REAL:]
Zero_ ((),Linear_Space_of_RealSequences) is Element of ()
Add_ ((),Linear_Space_of_RealSequences) is non empty Relation-like [:(),():] -defined () -valued Function-like V23([:(),():]) quasi_total Element of bool [:[:(),():],():]
[:(),():] is non empty Relation-like set
[:[:(),():],():] is non empty Relation-like set
bool [:[:(),():],():] is non empty set
Mult_ ((),Linear_Space_of_RealSequences) is non empty Relation-like [:REAL,():] -defined () -valued Function-like V23([:REAL,():]) quasi_total Element of bool [:[:REAL,():],():]
[:REAL,():] is non empty Relation-like set
[:[:REAL,():],():] is non empty Relation-like set
bool [:[:REAL,():],():] is non empty set
RLSStruct(# (),(Zero_ ((),Linear_Space_of_RealSequences)),(Add_ ((),Linear_Space_of_RealSequences)),(Mult_ ((),Linear_Space_of_RealSequences)) #) is non empty strict RLSStruct
[:(),REAL:] is non empty Relation-like V105() V106() V107() set
bool [:(),REAL:] is non empty set
X is set
seq_id X is non empty Relation-like NAT -defined REAL -valued Function-like V23( NAT ) quasi_total V105() V106() V107() Element of bool [:NAT,REAL:]
abs (seq_id X) is non empty Relation-like NAT -defined REAL -valued Function-like V23( NAT ) quasi_total V105() V106() V107() bounded_below Element of bool [:NAT,REAL:]
rng (abs (seq_id X)) is non empty V115() V116() V117() Element of bool REAL
upper_bound (rng (abs (seq_id X))) is V11() real ext-real Element of REAL
X is non empty Relation-like () -defined REAL -valued Function-like V23(()) quasi_total V105() V106() V107() Element of bool [:(),REAL:]
X is non empty Relation-like () -defined REAL -valued Function-like V23(()) quasi_total V105() V106() V107() Element of bool [:(),REAL:]
Y is non empty Relation-like () -defined REAL -valued Function-like V23(()) quasi_total V105() V106() V107() Element of bool [:(),REAL:]
vseq is set
X . vseq is V11() real ext-real Element of REAL
Y . vseq is V11() real ext-real Element of REAL
seq_id vseq is non empty Relation-like NAT -defined REAL -valued Function-like V23( NAT ) quasi_total V105() V106() V107() Element of bool [:NAT,REAL:]
abs (seq_id vseq) is non empty Relation-like NAT -defined REAL -valued Function-like V23( NAT ) quasi_total V105() V106() V107() bounded_below Element of bool [:NAT,REAL:]
rng (abs (seq_id vseq)) is non empty V115() V116() V117() Element of bool REAL
upper_bound (rng (abs (seq_id vseq))) is V11() real ext-real Element of REAL
dom X is non empty Element of bool ()
bool () is non empty set
dom Y is non empty Element of bool ()
() is non empty Relation-like () -defined REAL -valued Function-like V23(()) quasi_total V105() V106() V107() Element of bool [:(),REAL:]
X is non empty Relation-like NAT -defined REAL -valued Function-like V23( NAT ) quasi_total V105() V106() V107() Element of bool [:NAT,REAL:]
abs X is non empty Relation-like NAT -defined REAL -valued Function-like V23( NAT ) quasi_total V105() V106() V107() bounded_below Element of bool [:NAT,REAL:]
rng (abs X) is non empty V115() V116() V117() Element of bool REAL
upper_bound (rng (abs X)) is V11() real ext-real Element of REAL
Y is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real set
(abs X) . Y is V11() real ext-real Element of REAL
X . Y is V11() real ext-real Element of REAL
abs (X . Y) is V11() real ext-real Element of REAL
{0} is V115() V116() V117() V118() V119() V120() Element of bool REAL
Y is set
vseq is set
(abs X) . vseq is V11() real ext-real Element of REAL
X is non empty Relation-like NAT -defined REAL -valued Function-like V23( NAT ) quasi_total V105() V106() V107() Element of bool [:NAT,REAL:]
abs X is non empty Relation-like NAT -defined REAL -valued Function-like V23( NAT ) quasi_total V105() V106() V107() bounded_below Element of bool [:NAT,REAL:]
rng (abs X) is non empty V115() V116() V117() Element of bool REAL
upper_bound (rng (abs X)) is V11() real ext-real Element of REAL
Y is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real set
X . Y is V11() real ext-real Element of REAL
abs (X . Y) is V11() real ext-real Element of REAL
(abs X) . Y is V11() real ext-real Element of REAL
X is non empty Relation-like NAT -defined REAL -valued Function-like V23( NAT ) quasi_total V105() V106() V107() Element of bool [:NAT,REAL:]
abs X is non empty Relation-like NAT -defined REAL -valued Function-like V23( NAT ) quasi_total V105() V106() V107() bounded_below Element of bool [:NAT,REAL:]
rng (abs X) is non empty V115() V116() V117() Element of bool REAL
upper_bound (rng (abs X)) is V11() real ext-real Element of REAL
Y is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real set
X . Y is V11() real ext-real Element of REAL
vseq is non empty Relation-like NAT -defined REAL -valued Function-like V23( NAT ) quasi_total V105() V106() V107() Element of bool [:NAT,REAL:]
abs vseq is non empty Relation-like NAT -defined REAL -valued Function-like V23( NAT ) quasi_total V105() V106() V107() bounded_below Element of bool [:NAT,REAL:]
rng (abs vseq) is non empty V115() V116() V117() Element of bool REAL
upper_bound (rng (abs vseq)) is V11() real ext-real Element of REAL
NORMSTR(# (),(Zero_ ((),Linear_Space_of_RealSequences)),(Add_ ((),Linear_Space_of_RealSequences)),(Mult_ ((),Linear_Space_of_RealSequences)),() #) is non empty strict NORMSTR
() is non empty NORMSTR
the carrier of () is non empty set
0. () is V49(()) Element of the carrier of ()
the ZeroF of () is Element of the carrier of ()
0. Linear_Space_of_RealSequences is V49( 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
Y is set
seq_id Y is non empty Relation-like NAT -defined REAL -valued Function-like V23( NAT ) quasi_total V105() V106() V107() Element of bool [:NAT,REAL:]
Y is Element of the carrier of ()
vseq is Element of the carrier of ()
Y + vseq is Element of the carrier of ()
the addF of () is non empty Relation-like [: the carrier of (), the carrier of ():] -defined the carrier of () -valued Function-like V23([: the carrier of (), the carrier of ():]) quasi_total Element of bool [:[: the carrier of (), the carrier of ():], the carrier of ():]
[: the carrier of (), the carrier of ():] is non empty Relation-like set
[:[: the carrier of (), the carrier of ():], the carrier of ():] is non empty Relation-like set
bool [:[: the carrier of (), the carrier of ():], the carrier of ():] is non empty set
K584( the carrier of (), the addF of (),Y,vseq) is Element of the carrier of ()
[Y,vseq] is set
{Y,vseq} is set
{Y} is set
{{Y,vseq},{Y}} is set
the addF of () . [Y,vseq] is set
seq_id Y is non empty Relation-like NAT -defined REAL -valued Function-like V23( NAT ) quasi_total V105() V106() V107() Element of bool [:NAT,REAL:]
seq_id vseq is non empty Relation-like NAT -defined REAL -valued Function-like V23( NAT ) quasi_total V105() V106() V107() Element of bool [:NAT,REAL:]
(seq_id Y) + (seq_id vseq) is non empty Relation-like NAT -defined REAL -valued Function-like V23( NAT ) quasi_total V105() V106() V107() Element of bool [:NAT,REAL:]
[: the carrier of Linear_Space_of_RealSequences, the carrier of Linear_Space_of_RealSequences:] is non empty Relation-like set
the addF of Linear_Space_of_RealSequences is non empty 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 V23([: the carrier of Linear_Space_of_RealSequences, the carrier of Linear_Space_of_RealSequences:]) quasi_total 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:], the carrier of Linear_Space_of_RealSequences:] is non empty Relation-like set
bool [:[: the carrier of Linear_Space_of_RealSequences, the carrier of Linear_Space_of_RealSequences:], the carrier of Linear_Space_of_RealSequences:] is non empty set
dom the addF of Linear_Space_of_RealSequences is non empty Relation-like the carrier of Linear_Space_of_RealSequences -defined the carrier of Linear_Space_of_RealSequences -valued Element of bool [: the carrier of Linear_Space_of_RealSequences, the carrier of Linear_Space_of_RealSequences:]
bool [: the carrier of Linear_Space_of_RealSequences, the carrier of Linear_Space_of_RealSequences:] is non empty set
the addF of Linear_Space_of_RealSequences || () is Relation-like Function-like set
the addF of Linear_Space_of_RealSequences | [:(),():] is Relation-like [:(),():] -defined [: the carrier of Linear_Space_of_RealSequences, the carrier of Linear_Space_of_RealSequences:] -defined the carrier of Linear_Space_of_RealSequences -valued set
dom ( the addF of Linear_Space_of_RealSequences || ()) is set
[:(),():] is non empty Relation-like the carrier of Linear_Space_of_RealSequences -defined the carrier of Linear_Space_of_RealSequences -valued Element of bool [: the carrier of Linear_Space_of_RealSequences, the carrier of Linear_Space_of_RealSequences:]
[Y,vseq] is Element of [: the carrier of (), the carrier of ():]
( the addF of Linear_Space_of_RealSequences || ()) . [Y,vseq] is set
f is Element of the carrier of Linear_Space_of_RealSequences
tseq is Element of the carrier of Linear_Space_of_RealSequences
f + tseq is Element of the carrier of Linear_Space_of_RealSequences
K584( the carrier of Linear_Space_of_RealSequences, the addF of Linear_Space_of_RealSequences,f,tseq) is Element of the carrier of Linear_Space_of_RealSequences
[f,tseq] is set
{f,tseq} is set
{f} is set
{{f,tseq},{f}} is set
the addF of Linear_Space_of_RealSequences . [f,tseq] is set
Y is V11() real ext-real Element of REAL
vseq is Element of the carrier of ()
Y * vseq is Element of the carrier of ()
the Mult of () is non empty Relation-like [:REAL, the carrier of ():] -defined the carrier of () -valued Function-like V23([:REAL, the carrier of ():]) quasi_total Element of bool [:[:REAL, the carrier of ():], the carrier of ():]
[:REAL, the carrier of ():] is non empty Relation-like set
[:[:REAL, the carrier of ():], the carrier of ():] is non empty Relation-like set
bool [:[:REAL, the carrier of ():], the carrier of ():] is non empty set
K580( the Mult of (),Y,vseq) is set
[Y,vseq] is set
{Y,vseq} is set
{Y} is V115() V116() V117() set
{{Y,vseq},{Y}} is set
the Mult of () . [Y,vseq] is set
seq_id vseq is non empty Relation-like NAT -defined REAL -valued Function-like V23( NAT ) quasi_total V105() V106() V107() Element of bool [:NAT,REAL:]
Y (#) (seq_id vseq) is non empty Relation-like NAT -defined REAL -valued Function-like V23( NAT ) quasi_total V105() V106() V107() Element of bool [:NAT,REAL:]
[:REAL, the carrier of Linear_Space_of_RealSequences:] is non empty Relation-like set
the Mult of Linear_Space_of_RealSequences is non empty Relation-like [:REAL, the carrier of Linear_Space_of_RealSequences:] -defined the carrier of Linear_Space_of_RealSequences -valued Function-like V23([:REAL, the carrier of Linear_Space_of_RealSequences:]) quasi_total 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:], the carrier of Linear_Space_of_RealSequences:] is non empty Relation-like set
bool [:[:REAL, the carrier of Linear_Space_of_RealSequences:], the carrier of Linear_Space_of_RealSequences:] is non empty set
dom the Mult of Linear_Space_of_RealSequences is non empty Relation-like REAL -defined the carrier of Linear_Space_of_RealSequences -valued Element of bool [:REAL, the carrier of Linear_Space_of_RealSequences:]
bool [:REAL, the carrier of Linear_Space_of_RealSequences:] is non empty set
the Mult of Linear_Space_of_RealSequences | [:REAL,():] is Relation-like [:REAL,():] -defined [:REAL, the carrier of Linear_Space_of_RealSequences:] -defined the carrier of Linear_Space_of_RealSequences -valued Function-like Element of bool [:[:REAL, the carrier of Linear_Space_of_RealSequences:], the carrier of Linear_Space_of_RealSequences:]
dom ( the Mult of Linear_Space_of_RealSequences | [:REAL,():]) is Relation-like REAL -defined () -valued Element of bool [:REAL,():]
bool [:REAL,():] is non empty set
[Y,vseq] is Element of [:REAL, the carrier of ():]
( the Mult of Linear_Space_of_RealSequences | [:REAL,():]) . [Y,vseq] is set
f is Element of the carrier of Linear_Space_of_RealSequences
Y * f is Element of the carrier of Linear_Space_of_RealSequences
K580( the Mult of Linear_Space_of_RealSequences,Y,f) is set
[Y,f] is set
{Y,f} is set
{{Y,f},{Y}} is set
the Mult of Linear_Space_of_RealSequences . [Y,f] is set
Y is Element of the carrier of ()
seq_id Y is non empty Relation-like NAT -defined REAL -valued Function-like V23( NAT ) quasi_total V105() V106() V107() Element of bool [:NAT,REAL:]
Y is Element of the carrier of ()
- Y is Element of the carrier of ()
seq_id Y is non empty Relation-like NAT -defined REAL -valued Function-like V23( NAT ) quasi_total V105() V106() V107() Element of bool [:NAT,REAL:]
- (seq_id Y) is non empty Relation-like NAT -defined REAL -valued Function-like V23( NAT ) quasi_total V105() V106() V107() Element of bool [:NAT,REAL:]
K38(1) is V11() real ext-real non positive set
K38(1) (#) (seq_id Y) is Relation-like NAT -defined Function-like V23( NAT ) V105() V106() V107() set
seq_id (- Y) is non empty Relation-like NAT -defined REAL -valued Function-like V23( NAT ) quasi_total V105() V106() V107() Element of bool [:NAT,REAL:]
(- 1) * Y is Element of the carrier of ()
the Mult of () is non empty Relation-like [:REAL, the carrier of ():] -defined the carrier of () -valued Function-like V23([:REAL, the carrier of ():]) quasi_total Element of bool [:[:REAL, the carrier of ():], the carrier of ():]
[:REAL, the carrier of ():] is non empty Relation-like set
[:[:REAL, the carrier of ():], the carrier of ():] is non empty Relation-like set
bool [:[:REAL, the carrier of ():], the carrier of ():] is non empty set
K580( the Mult of (),(- 1),Y) is set
[(- 1),Y] is set
{(- 1),Y} is set
{(- 1)} is V115() V116() V117() set
{{(- 1),Y},{(- 1)}} is set
the Mult of () . [(- 1),Y] is set
Y is Element of the carrier of ()
vseq is Element of the carrier of ()
Y - vseq is Element of the carrier of ()
- vseq is Element of the carrier of ()
Y + (- vseq) is Element of the carrier of ()
the addF of () is non empty Relation-like [: the carrier of (), the carrier of ():] -defined the carrier of () -valued Function-like V23([: the carrier of (), the carrier of ():]) quasi_total Element of bool [:[: the carrier of (), the carrier of ():], the carrier of ():]
[: the carrier of (), the carrier of ():] is non empty Relation-like set
[:[: the carrier of (), the carrier of ():], the carrier of ():] is non empty Relation-like set
bool [:[: the carrier of (), the carrier of ():], the carrier of ():] is non empty set
K584( the carrier of (), the addF of (),Y,(- vseq)) is Element of the carrier of ()
[Y,(- vseq)] is set
{Y,(- vseq)} is set
{Y} is set
{{Y,(- vseq)},{Y}} is set
the addF of () . [Y,(- vseq)] is set
seq_id Y is non empty Relation-like NAT -defined REAL -valued Function-like V23( NAT ) quasi_total V105() V106() V107() Element of bool [:NAT,REAL:]
seq_id vseq is non empty Relation-like NAT -defined REAL -valued Function-like V23( NAT ) quasi_total V105() V106() V107() Element of bool [:NAT,REAL:]
(seq_id Y) - (seq_id vseq) is non empty Relation-like NAT -defined REAL -valued Function-like V23( NAT ) quasi_total V105() V106() V107() Element of bool [:NAT,REAL:]
- (seq_id vseq) is Relation-like NAT -defined Function-like V23( NAT ) V105() V106() V107() set
K38(1) is V11() real ext-real non positive set
K38(1) (#) (seq_id vseq) is Relation-like NAT -defined Function-like V23( NAT ) V105() V106() V107() set
(seq_id Y) + (- (seq_id vseq)) is Relation-like NAT -defined Function-like V23( NAT ) V105() V106() V107() set
seq_id (- vseq) is non empty Relation-like NAT -defined REAL -valued Function-like V23( NAT ) quasi_total V105() V106() V107() Element of bool [:NAT,REAL:]
(seq_id Y) + (seq_id (- vseq)) is non empty Relation-like NAT -defined REAL -valued Function-like V23( NAT ) quasi_total V105() V106() V107() Element of bool [:NAT,REAL:]
Y is set
seq_id Y is non empty Relation-like NAT -defined REAL -valued Function-like V23( NAT ) quasi_total V105() V106() V107() Element of bool [:NAT,REAL:]
vseq is set
seq_id vseq is non empty Relation-like NAT -defined REAL -valued Function-like V23( NAT ) quasi_total V105() V106() V107() Element of bool [:NAT,REAL:]
f is Element of the carrier of ()
seq_id f is non empty Relation-like NAT -defined REAL -valued Function-like V23( NAT ) quasi_total V105() V106() V107() Element of bool [:NAT,REAL:]
tseq is Element of the carrier of ()
tseq is Element of the carrier of ()
tseq + tseq is Element of the carrier of ()
the addF of () is non empty Relation-like [: the carrier of (), the carrier of ():] -defined the carrier of () -valued Function-like V23([: the carrier of (), the carrier of ():]) quasi_total Element of bool [:[: the carrier of (), the carrier of ():], the carrier of ():]
[: the carrier of (), the carrier of ():] is non empty Relation-like set
[:[: the carrier of (), the carrier of ():], the carrier of ():] is non empty Relation-like set
bool [:[: the carrier of (), the carrier of ():], the carrier of ():] is non empty set
K584( the carrier of (), the addF of (),tseq,tseq) is Element of the carrier of ()
[tseq,tseq] is set
{tseq,tseq} is set
{tseq} is set
{{tseq,tseq},{tseq}} is set
the addF of () . [tseq,tseq] is set
seq_id tseq is non empty Relation-like NAT -defined REAL -valued Function-like V23( NAT ) quasi_total V105() V106() V107() Element of bool [:NAT,REAL:]
seq_id tseq is non empty Relation-like NAT -defined REAL -valued Function-like V23( NAT ) quasi_total V105() V106() V107() Element of bool [:NAT,REAL:]
(seq_id tseq) + (seq_id tseq) is non empty Relation-like NAT -defined REAL -valued Function-like V23( NAT ) quasi_total V105() V106() V107() Element of bool [:NAT,REAL:]
e is Element of the carrier of ()
tv is V11() real ext-real Element of REAL
tv * e is Element of the carrier of ()
the Mult of () is non empty Relation-like [:REAL, the carrier of ():] -defined the carrier of () -valued Function-like V23([:REAL, the carrier of ():]) quasi_total Element of bool [:[:REAL, the carrier of ():], the carrier of ():]
[:REAL, the carrier of ():] is non empty Relation-like set
[:[:REAL, the carrier of ():], the carrier of ():] is non empty Relation-like set
bool [:[:REAL, the carrier of ():], the carrier of ():] is non empty set
K580( the Mult of (),tv,e) is set
[tv,e] is set
{tv,e} is set
{tv} is V115() V116() V117() set
{{tv,e},{tv}} is set
the Mult of () . [tv,e] is set
seq_id e is non empty Relation-like NAT -defined REAL -valued Function-like V23( NAT ) quasi_total V105() V106() V107() Element of bool [:NAT,REAL:]
tv (#) (seq_id e) is non empty Relation-like NAT -defined REAL -valued Function-like V23( NAT ) quasi_total V105() V106() V107() Element of bool [:NAT,REAL:]
m is Element of the carrier of ()
- m is Element of the carrier of ()
seq_id m is non empty Relation-like NAT -defined REAL -valued Function-like V23( NAT ) quasi_total V105() V106() V107() Element of bool [:NAT,REAL:]
- (seq_id m) is non empty Relation-like NAT -defined REAL -valued Function-like V23( NAT ) quasi_total V105() V106() V107() Element of bool [:NAT,REAL:]
K38(1) is V11() real ext-real non positive set
K38(1) (#) (seq_id m) is Relation-like NAT -defined Function-like V23( NAT ) V105() V106() V107() set
n is Element of the carrier of ()
- n is Element of the carrier of ()
seq_id (- n) is non empty Relation-like NAT -defined REAL -valued Function-like V23( NAT ) quasi_total V105() V106() V107() Element of bool [:NAT,REAL:]
seq_id n is non empty Relation-like NAT -defined REAL -valued Function-like V23( NAT ) quasi_total V105() V106() V107() Element of bool [:NAT,REAL:]
- (seq_id n) is non empty Relation-like NAT -defined REAL -valued Function-like V23( NAT ) quasi_total V105() V106() V107() Element of bool [:NAT,REAL:]
K38(1) (#) (seq_id n) is Relation-like NAT -defined Function-like V23( NAT ) V105() V106() V107() set
n is Element of the carrier of ()
h1 is Element of the carrier of ()
n - h1 is Element of the carrier of ()
- h1 is Element of the carrier of ()
n + (- h1) is Element of the carrier of ()
K584( the carrier of (), the addF of (),n,(- h1)) is Element of the carrier of ()
[n,(- h1)] is set
{n,(- h1)} is set
{n} is set
{{n,(- h1)},{n}} is set
the addF of () . [n,(- h1)] is set
seq_id n is non empty Relation-like NAT -defined REAL -valued Function-like V23( NAT ) quasi_total V105() V106() V107() Element of bool [:NAT,REAL:]
seq_id h1 is non empty Relation-like NAT -defined REAL -valued Function-like V23( NAT ) quasi_total V105() V106() V107() Element of bool [:NAT,REAL:]
(seq_id n) - (seq_id h1) is non empty Relation-like NAT -defined REAL -valued Function-like V23( NAT ) quasi_total V105() V106() V107() Element of bool [:NAT,REAL:]
- (seq_id h1) is Relation-like NAT -defined Function-like V23( NAT ) V105() V106() V107() set
K38(1) (#) (seq_id h1) is Relation-like NAT -defined Function-like V23( NAT ) V105() V106() V107() set
(seq_id n) + (- (seq_id h1)) is Relation-like NAT -defined Function-like V23( NAT ) V105() V106() V107() set
f1 is Element of the carrier of ()
seq_id f1 is non empty Relation-like NAT -defined REAL -valued Function-like V23( NAT ) quasi_total V105() V106() V107() Element of bool [:NAT,REAL:]
r is Element of the carrier of ()
||.r.|| is V11() real ext-real Element of REAL
the normF of () is non empty Relation-like the carrier of () -defined REAL -valued Function-like V23( the carrier of ()) quasi_total V105() V106() V107() Element of bool [: the carrier of (),REAL:]
[: the carrier of (),REAL:] is non empty Relation-like V105() V106() V107() set
bool [: the carrier of (),REAL:] is non empty set
the normF of () . r is V11() real ext-real Element of REAL
seq_id r is non empty Relation-like NAT -defined REAL -valued Function-like V23( NAT ) quasi_total V105() V106() V107() Element of bool [:NAT,REAL:]
abs (seq_id r) is non empty Relation-like NAT -defined REAL -valued Function-like V23( NAT ) quasi_total V105() V106() V107() bounded_below Element of bool [:NAT,REAL:]
rng (abs (seq_id r)) is non empty V115() V116() V117() Element of bool REAL
upper_bound (rng (abs (seq_id r))) is V11() real ext-real Element of REAL
X is Element of the carrier of ()
||.X.|| is V11() real ext-real Element of REAL
the normF of () is non empty Relation-like the carrier of () -defined REAL -valued Function-like V23( the carrier of ()) quasi_total V105() V106() V107() Element of bool [: the carrier of (),REAL:]
[: the carrier of (),REAL:] is non empty Relation-like V105() V106() V107() set
bool [: the carrier of (),REAL:] is non empty set
the normF of () . X is V11() real ext-real Element of REAL
Y is Element of the carrier of ()
X + Y is Element of the carrier of ()
the addF of () is non empty Relation-like [: the carrier of (), the carrier of ():] -defined the carrier of () -valued Function-like V23([: the carrier of (), the carrier of ():]) quasi_total Element of bool [:[: the carrier of (), the carrier of ():], the carrier of ():]
[: the carrier of (), the carrier of ():] is non empty Relation-like set
[:[: the carrier of (), the carrier of ():], the carrier of ():] is non empty Relation-like set
bool [:[: the carrier of (), the carrier of ():], the carrier of ():] is non empty set
K584( the carrier of (), the addF of (),X,Y) is Element of the carrier of ()
[X,Y] is set
{X,Y} is set
{X} is set
{{X,Y},{X}} is set
the addF of () . [X,Y] is set
||.(X + Y).|| is V11() real ext-real Element of REAL
the normF of () . (X + Y) is V11() real ext-real Element of REAL
||.Y.|| is V11() real ext-real Element of REAL
the normF of () . Y is V11() real ext-real Element of REAL
||.X.|| + ||.Y.|| is V11() real ext-real Element of REAL
vseq is V11() real ext-real Element of REAL
vseq * X is Element of the carrier of ()
the Mult of () is non empty Relation-like [:REAL, the carrier of ():] -defined the carrier of () -valued Function-like V23([:REAL, the carrier of ():]) quasi_total Element of bool [:[:REAL, the carrier of ():], the carrier of ():]
[:REAL, the carrier of ():] is non empty Relation-like set
[:[:REAL, the carrier of ():], the carrier of ():] is non empty Relation-like set
bool [:[:REAL, the carrier of ():], the carrier of ():] is non empty set
K580( the Mult of (),vseq,X) is set
[vseq,X] is set
{vseq,X} is set
{vseq} is V115() V116() V117() set
{{vseq,X},{vseq}} is set
the Mult of () . [vseq,X] is set
||.(vseq * X).|| is V11() real ext-real Element of REAL
the normF of () . (vseq * X) is V11() real ext-real Element of REAL
abs vseq is V11() real ext-real Element of REAL
(abs vseq) * ||.X.|| is V11() real ext-real Element of REAL
seq_id X is non empty Relation-like NAT -defined REAL -valued Function-like V23( NAT ) quasi_total V105() V106() V107() Element of bool [:NAT,REAL:]
vseq (#) (seq_id X) is non empty Relation-like NAT -defined REAL -valued Function-like V23( NAT ) quasi_total V105() V106() V107() Element of bool [:NAT,REAL:]
abs (vseq (#) (seq_id X)) is non empty Relation-like NAT -defined REAL -valued Function-like V23( NAT ) quasi_total V105() V106() V107() bounded_below Element of bool [:NAT,REAL:]
abs (seq_id X) is non empty Relation-like NAT -defined REAL -valued Function-like V23( NAT ) quasi_total V105() V106() V107() bounded_below Element of bool [:NAT,REAL:]
f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V115() V116() V117() V118() V119() V120() V145() V168() Element of NAT
(abs (vseq (#) (seq_id X))) . f is V11() real ext-real Element of REAL
(abs (seq_id X)) . f is V11() real ext-real Element of REAL
(abs vseq) * ((abs (seq_id X)) . f) is V11() real ext-real Element of REAL
(vseq (#) (seq_id X)) . f is V11() real ext-real Element of REAL
abs ((vseq (#) (seq_id X)) . f) is V11() real ext-real Element of REAL
(seq_id X) . f is V11() real ext-real Element of REAL
vseq * ((seq_id X) . f) is V11() real ext-real Element of REAL
abs (vseq * ((seq_id X) . f)) is V11() real ext-real Element of REAL
abs ((seq_id X) . f) is V11() real ext-real Element of REAL
(abs vseq) * (abs ((seq_id X) . f)) is V11() real ext-real Element of REAL
(abs (seq_id X)) . 1 is V11() real ext-real Element of REAL
(seq_id X) . 1 is V11() real ext-real Element of REAL
abs ((seq_id X) . 1) is V11() real ext-real Element of REAL
seq_id (X + Y) is non empty Relation-like NAT -defined REAL -valued Function-like V23( NAT ) quasi_total V105() V106() V107() Element of bool [:NAT,REAL:]
abs (seq_id (X + Y)) is non empty Relation-like NAT -defined REAL -valued Function-like V23( NAT ) quasi_total V105() V106() V107() bounded_below Element of bool [:NAT,REAL:]
seq_id Y is non empty Relation-like NAT -defined REAL -valued Function-like V23( NAT ) quasi_total V105() V106() V107() Element of bool [:NAT,REAL:]
f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V115() V116() V117() V118() V119() V120() V145() V168() Element of NAT
(abs (seq_id (X + Y))) . f is V11() real ext-real Element of REAL
(seq_id X) . f is V11() real ext-real Element of REAL
(seq_id Y) . f is V11() real ext-real Element of REAL
((seq_id X) . f) + ((seq_id Y) . f) is V11() real ext-real Element of REAL
abs (((seq_id X) . f) + ((seq_id Y) . f)) is V11() real ext-real Element of REAL
(seq_id X) + (seq_id Y) is non empty Relation-like NAT -defined REAL -valued Function-like V23( NAT ) quasi_total V105() V106() V107() Element of bool [:NAT,REAL:]
seq_id ((seq_id X) + (seq_id Y)) is non empty Relation-like NAT -defined REAL -valued Function-like V23( NAT ) quasi_total V105() V106() V107() Element of bool [:NAT,REAL:]
abs (seq_id ((seq_id X) + (seq_id Y))) is non empty Relation-like NAT -defined REAL -valued Function-like V23( NAT ) quasi_total V105() V106() V107() bounded_below Element of bool [:NAT,REAL:]
(abs (seq_id ((seq_id X) + (seq_id Y)))) . f is V11() real ext-real Element of REAL
abs ((seq_id X) + (seq_id Y)) is non empty Relation-like NAT -defined REAL -valued Function-like V23( NAT ) quasi_total V105() V106() V107() bounded_below Element of bool [:NAT,REAL:]
(abs ((seq_id X) + (seq_id Y))) . f is V11() real ext-real Element of REAL
((seq_id X) + (seq_id Y)) . f is V11() real ext-real Element of REAL
abs (((seq_id X) + (seq_id Y)) . f) is V11() real ext-real Element of REAL
abs (seq_id Y) is non empty Relation-like NAT -defined REAL -valued Function-like V23( NAT ) quasi_total V105() V106() V107() bounded_below Element of bool [:NAT,REAL:]
f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V115() V116() V117() V118() V119() V120() V145() V168() Element of NAT
(abs (seq_id (X + Y))) . f is V11() real ext-real Element of REAL
(abs (seq_id X)) . f is V11() real ext-real Element of REAL
(abs (seq_id Y)) . f is V11() real ext-real Element of REAL
((abs (seq_id X)) . f) + ((abs (seq_id Y)) . f) is V11() real ext-real Element of REAL
(seq_id X) . f is V11() real ext-real Element of REAL
(seq_id Y) . f is V11() real ext-real Element of REAL
((seq_id X) . f) + ((seq_id Y) . f) is V11() real ext-real Element of REAL
abs (((seq_id X) . f) + ((seq_id Y) . f)) is V11() real ext-real Element of REAL
abs ((seq_id X) . f) is V11() real ext-real Element of REAL
abs ((seq_id Y) . f) is V11() real ext-real Element of REAL
(abs ((seq_id X) . f)) + (abs ((seq_id Y) . f)) is V11() real ext-real Element of REAL
((abs (seq_id X)) . f) + (abs ((seq_id Y) . f)) is V11() real ext-real Element of REAL
(abs (seq_id X)) + (abs (seq_id Y)) is non empty Relation-like NAT -defined REAL -valued Function-like V23( NAT ) quasi_total V105() V106() V107() bounded_below Element of bool [:NAT,REAL:]
f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V115() V116() V117() V118() V119() V120() V145() V168() Element of NAT
(abs (seq_id (X + Y))) . f is V11() real ext-real Element of REAL
((abs (seq_id X)) + (abs (seq_id Y))) . f is V11() real ext-real Element of REAL
(abs (seq_id X)) . f is V11() real ext-real Element of REAL
(abs (seq_id Y)) . f is V11() real ext-real Element of REAL
((abs (seq_id X)) . f) + ((abs (seq_id Y)) . f) is V11() real ext-real Element of REAL
f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real set
(seq_id X) . f is V11() real ext-real Element of REAL
rng (abs (seq_id X)) is non empty V115() V116() V117() Element of bool REAL
upper_bound (rng (abs (seq_id X))) is V11() real ext-real Element of REAL
f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V115() V116() V117() V118() V119() V120() V145() V168() Element of NAT
(seq_id X) . f is V11() real ext-real Element of REAL
f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V115() V116() V117() V118() V119() V120() V145() V168() Element of NAT
(abs (seq_id Y)) . f is V11() real ext-real Element of REAL
rng (abs (seq_id Y)) is non empty V115() V116() V117() Element of bool REAL
upper_bound (rng (abs (seq_id Y))) is V11() real ext-real Element of REAL
((abs (seq_id X)) + (abs (seq_id Y))) . f is V11() real ext-real Element of REAL
(abs (seq_id X)) . f is V11() real ext-real Element of REAL
((abs (seq_id X)) . f) + ((abs (seq_id Y)) . f) is V11() real ext-real Element of REAL
(upper_bound (rng (abs (seq_id X)))) + (upper_bound (rng (abs (seq_id Y)))) is V11() real ext-real Element of REAL
(abs (seq_id (X + Y))) . f is V11() real ext-real Element of REAL
rng (abs (seq_id (X + Y))) is non empty V115() V116() V117() Element of bool REAL
upper_bound (rng (abs (seq_id (X + Y)))) is V11() real ext-real Element of REAL
seq_id (vseq * X) is non empty Relation-like NAT -defined REAL -valued Function-like V23( NAT ) quasi_total V105() V106() V107() Element of bool [:NAT,REAL:]
abs (seq_id (vseq * X)) is non empty Relation-like NAT -defined REAL -valued Function-like V23( NAT ) quasi_total V105() V106() V107() bounded_below Element of bool [:NAT,REAL:]
rng (abs (seq_id (vseq * X))) is non empty V115() V116() V117() Element of bool REAL
upper_bound (rng (abs (seq_id (vseq * X)))) is V11() real ext-real Element of REAL
seq_id (vseq (#) (seq_id X)) is non empty Relation-like NAT -defined REAL -valued Function-like V23( NAT ) quasi_total V105() V106() V107() Element of bool [:NAT,REAL:]
abs (seq_id (vseq (#) (seq_id X))) is non empty Relation-like NAT -defined REAL -valued Function-like V23( NAT ) quasi_total V105() V106() V107() bounded_below Element of bool [:NAT,REAL:]
rng (abs (seq_id (vseq (#) (seq_id X)))) is non empty V115() V116() V117() Element of bool REAL
upper_bound (rng (abs (seq_id (vseq (#) (seq_id X))))) is V11() real ext-real Element of REAL
rng (abs (vseq (#) (seq_id X))) is non empty V115() V116() V117() Element of bool REAL
upper_bound (rng (abs (vseq (#) (seq_id X)))) is V11() real ext-real Element of REAL
(abs vseq) (#) (abs (seq_id X)) is non empty Relation-like NAT -defined REAL -valued Function-like V23( NAT ) quasi_total V105() V106() V107() Element of bool [:NAT,REAL:]
rng ((abs vseq) (#) (abs (seq_id X))) is non empty V115() V116() V117() Element of bool REAL
upper_bound (rng ((abs vseq) (#) (abs (seq_id X)))) is V11() real ext-real Element of REAL
(abs vseq) ** (rng (abs (seq_id X))) is V115() V116() V117() Element of bool REAL
upper_bound ((abs vseq) ** (rng (abs (seq_id X)))) is V11() real ext-real Element of REAL
(abs vseq) * (upper_bound (rng (abs (seq_id X)))) is V11() real ext-real Element of REAL
||.(0. ()).|| is V11() real ext-real Element of REAL
the normF of () is non empty Relation-like the carrier of () -defined REAL -valued Function-like V23( the carrier of ()) quasi_total V105() V106() V107() Element of bool [: the carrier of (),REAL:]
[: the carrier of (),REAL:] is non empty Relation-like V105() V106() V107() set
bool [: the carrier of (),REAL:] is non empty set
the normF of () . (0. ()) is V11() real ext-real Element of REAL
[:NAT, the carrier of ():] is non empty Relation-like set
bool [:NAT, the carrier of ():] is non empty set
X is non empty Relation-like NAT -defined the carrier of () -valued Function-like V23( NAT ) quasi_total Element of bool [:NAT, the carrier of ():]
Y is set
vseq is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V115() V116() V117() V118() V119() V120() V145() V168() Element of NAT
f is non empty Relation-like NAT -defined REAL -valued Function-like V23( NAT ) quasi_total V105() V106() V107() Element of bool [:NAT,REAL:]
lim f is V11() real ext-real Element of REAL
tseq is V11() real ext-real set
tseq is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V115() V116() V117() V118() V119() V120() V145() V168() Element of NAT
f . tseq is V11() real ext-real Element of REAL
tv is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V115() V116() V117() V118() V119() V120() V145() V168() Element of NAT
f . tv is V11() real ext-real Element of REAL
(f . tv) - (f . tseq) is V11() real ext-real Element of REAL
abs ((f . tv) - (f . tseq)) is V11() real ext-real Element of REAL
X . tv is Element of the carrier of ()
X . tseq is Element of the carrier of ()
(X . tv) - (X . tseq) is Element of the carrier of ()
- (X . tseq) is Element of the carrier of ()
(X . tv) + (- (X . tseq)) is Element of the carrier of ()
the addF of () is non empty Relation-like [: the carrier of (), the carrier of ():] -defined the carrier of () -valued Function-like V23([: the carrier of (), the carrier of ():]) quasi_total Element of bool [:[: the carrier of (), the carrier of ():], the carrier of ():]
[: the carrier of (), the carrier of ():] is non empty Relation-like set
[:[: the carrier of (), the carrier of ():], the carrier of ():] is non empty Relation-like set
bool [:[: the carrier of (), the carrier of ():], the carrier of ():] is non empty set
K584( the carrier of (), the addF of (),(X . tv),(- (X . tseq))) is Element of the carrier of ()
[(X . tv),(- (X . tseq))] is set
{(X . tv),(- (X . tseq))} is set
{(X . tv)} is set
{{(X . tv),(- (X . tseq))},{(X . tv)}} is set
the addF of () . [(X . tv),(- (X . tseq))] is set
seq_id ((X . tv) - (X . tseq)) is non empty Relation-like NAT -defined REAL -valued Function-like V23( NAT ) quasi_total V105() V106() V107() Element of bool [:NAT,REAL:]
abs (seq_id ((X . tv) - (X . tseq))) is non empty Relation-like NAT -defined REAL -valued Function-like V23( NAT ) quasi_total V105() V106() V107() bounded_below Element of bool [:NAT,REAL:]
(abs (seq_id ((X . tv) - (X . tseq)))) . vseq is V11() real ext-real Element of REAL
rng (abs (seq_id ((X . tv) - (X . tseq)))) is non empty V115() V116() V117() Element of bool REAL
upper_bound (rng (abs (seq_id ((X . tv) - (X . tseq))))) is V11() real ext-real Element of REAL
seq_id (X . tv) is non empty Relation-like NAT -defined REAL -valued Function-like V23( NAT ) quasi_total V105() V106() V107() Element of bool [:NAT,REAL:]
seq_id (X . tseq) is non empty Relation-like NAT -defined REAL -valued Function-like V23( NAT ) quasi_total V105() V106() V107() Element of bool [:NAT,REAL:]
(seq_id (X . tv)) - (seq_id (X . tseq)) is non empty Relation-like NAT -defined REAL -valued Function-like V23( NAT ) quasi_total V105() V106() V107() Element of bool [:NAT,REAL:]
- (seq_id (X . tseq)) is Relation-like NAT -defined Function-like V23( NAT ) V105() V106() V107() set
K38(1) is V11() real ext-real non positive set
K38(1) (#) (seq_id (X . tseq)) is Relation-like NAT -defined Function-like V23( NAT ) V105() V106() V107() set
(seq_id (X . tv)) + (- (seq_id (X . tseq))) is Relation-like NAT -defined Function-like V23( NAT ) V105() V106() V107() set
seq_id ((seq_id (X . tv)) - (seq_id (X . tseq))) is non empty Relation-like NAT -defined REAL -valued Function-like V23( NAT ) quasi_total V105() V106() V107() Element of bool [:NAT,REAL:]
- (seq_id (X . tseq)) is non empty Relation-like NAT -defined REAL -valued Function-like V23( NAT ) quasi_total V105() V106() V107() Element of bool [:NAT,REAL:]
(seq_id (X . tv)) + (- (seq_id (X . tseq))) is non empty Relation-like NAT -defined REAL -valued Function-like V23( NAT ) quasi_total V105() V106() V107() Element of bool [:NAT,REAL:]
(seq_id ((X . tv) - (X . tseq))) . vseq is V11() real ext-real Element of REAL
(seq_id (X . tv)) . vseq is V11() real ext-real Element of REAL
(- (seq_id (X . tseq))) . vseq is V11() real ext-real Element of REAL
((seq_id (X . tv)) . vseq) + ((- (seq_id (X . tseq))) . vseq) is V11() real ext-real Element of REAL
(seq_id (X . tseq)) . vseq is V11() real ext-real Element of REAL
- ((seq_id (X . tseq)) . vseq) is V11() real ext-real Element of REAL
((seq_id (X . tv)) . vseq) + (- ((seq_id (X . tseq)) . vseq)) is V11() real ext-real Element of REAL
((seq_id (X . tv)) . vseq) - ((seq_id (X . tseq)) . vseq) is V11() real ext-real Element of REAL
(f . tv) - ((seq_id (X . tseq)) . vseq) is V11() real ext-real Element of REAL
||.((X . tv) - (X . tseq)).|| is V11() real ext-real non negative Element of REAL
the normF of () is non empty Relation-like the carrier of () -defined REAL -valued Function-like V23( the carrier of ()) quasi_total V105() V106() V107() Element of bool [: the carrier of (),REAL:]
[: the carrier of (),REAL:] is non empty Relation-like V105() V106() V107() set
bool [: the carrier of (),REAL:] is non empty set
the normF of () . ((X . tv) - (X . tseq)) is V11() real ext-real Element of REAL
Y is non empty Relation-like NAT -defined REAL -valued Function-like V23( NAT ) quasi_total V105() V106() V107() Element of bool [:NAT,REAL:]
f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V115() V116() V117() V118() V119() V120() V145() V168() Element of NAT
tseq is set
Y . tseq is V11() real ext-real Element of REAL
vseq is non empty Relation-like NAT -defined REAL -valued Function-like V23( NAT ) quasi_total V105() V106() V107() Element of bool [:NAT,REAL:]
vseq . f is V11() real ext-real Element of REAL
tseq is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V115() V116() V117() V118() V119() V120() V145() V168() Element of NAT
tv is non empty Relation-like NAT -defined REAL -valued Function-like V23( NAT ) quasi_total V105() V106() V107() Element of bool [:NAT,REAL:]
lim tv is V11() real ext-real Element of REAL
seq_id vseq is non empty Relation-like NAT -defined REAL -valued Function-like V23( NAT ) quasi_total V105() V106() V107() Element of bool [:NAT,REAL:]
f is V11() real ext-real Element of REAL
tseq is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V115() V116() V117() V118() V119() V120() V145() V168() Element of NAT
tv is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V115() V116() V117() V118() V119() V120() V145() V168() Element of NAT
tseq is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V115() V116() V117() V118() V119() V120() V145() V168() Element of NAT
X . tv is Element of the carrier of ()
X . tseq is Element of the carrier of ()
(X . tv) - (X . tseq) is Element of the carrier of ()
- (X . tseq) is Element of the carrier of ()
(X . tv) + (- (X . tseq)) is Element of the carrier of ()
the addF of () is non empty Relation-like [: the carrier of (), the carrier of ():] -defined the carrier of () -valued Function-like V23([: the carrier of (), the carrier of ():]) quasi_total Element of bool [:[: the carrier of (), the carrier of ():], the carrier of ():]
[: the carrier of (), the carrier of ():] is non empty Relation-like set
[:[: the carrier of (), the carrier of ():], the carrier of ():] is non empty Relation-like set
bool [:[: the carrier of (), the carrier of ():], the carrier of ():] is non empty set
K584( the carrier of (), the addF of (),(X . tv),(- (X . tseq))) is Element of the carrier of ()
[(X . tv),(- (X . tseq))] is set
{(X . tv),(- (X . tseq))} is set
{(X . tv)} is set
{{(X . tv),(- (X . tseq))},{(X . tv)}} is set
the addF of () . [(X . tv),(- (X . tseq))] is set
seq_id ((X . tv) - (X . tseq)) is non empty Relation-like NAT -defined REAL -valued Function-like V23( NAT ) quasi_total V105() V106() V107() Element of bool [:NAT,REAL:]
abs (seq_id ((X . tv) - (X . tseq))) is non empty Relation-like NAT -defined REAL -valued Function-like V23( NAT ) quasi_total V105() V106() V107() bounded_below Element of bool [:NAT,REAL:]
rng (abs (seq_id ((X . tv) - (X . tseq)))) is non empty V115() V116() V117() Element of bool REAL
upper_bound (rng (abs (seq_id ((X . tv) - (X . tseq))))) is V11() real ext-real Element of REAL
||.((X . tv) - (X . tseq)).|| is V11() real ext-real non negative Element of REAL
the normF of () is non empty Relation-like the carrier of () -defined REAL -valued Function-like V23( the carrier of ()) quasi_total V105() V106() V107() Element of bool [: the carrier of (),REAL:]
[: the carrier of (),REAL:] is non empty Relation-like V105() V106() V107() set
bool [: the carrier of (),REAL:] is non empty set
the normF of () . ((X . tv) - (X . tseq)) is V11() real ext-real Element of REAL
tseq is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V115() V116() V117() V118() V119() V120() V145() V168() Element of NAT
X . tseq is Element of the carrier of ()
seq_id (X . tseq) is non empty Relation-like NAT -defined REAL -valued Function-like V23( NAT ) quasi_total V105() V106() V107() Element of bool [:NAT,REAL:]
(seq_id vseq) - (seq_id (X . tseq)) is non empty Relation-like NAT -defined REAL -valued Function-like V23( NAT ) quasi_total V105() V106() V107() Element of bool [:NAT,REAL:]
- (seq_id (X . tseq)) is Relation-like NAT -defined Function-like V23( NAT ) V105() V106() V107() set
K38(1) is V11() real ext-real non positive set
K38(1) (#) (seq_id (X . tseq)) is Relation-like NAT -defined Function-like V23( NAT ) V105() V106() V107() set
(seq_id vseq) + (- (seq_id (X . tseq))) is Relation-like NAT -defined Function-like V23( NAT ) V105() V106() V107() set
abs ((seq_id vseq) - (seq_id (X . tseq))) is non empty Relation-like NAT -defined REAL -valued Function-like V23( NAT ) quasi_total V105() V106() V107() bounded_below Element of bool [:NAT,REAL:]
tv is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V115() V116() V117() V118() V119() V120() V145() V168() Element of NAT
X . tv is Element of the carrier of ()
e is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V115() V116() V117() V118() V119() V120() V145() V168() Element of NAT
X . e is Element of the carrier of ()
(X . tv) - (X . e) is Element of the carrier of ()
- (X . e) is Element of the carrier of ()
(X . tv) + (- (X . e)) is Element of the carrier of ()
the addF of () is non empty Relation-like [: the carrier of (), the carrier of ():] -defined the carrier of () -valued Function-like V23([: the carrier of (), the carrier of ():]) quasi_total Element of bool [:[: the carrier of (), the carrier of ():], the carrier of ():]
[: the carrier of (), the carrier of ():] is non empty Relation-like set
[:[: the carrier of (), the carrier of ():], the carrier of ():] is non empty Relation-like set
bool [:[: the carrier of (), the carrier of ():], the carrier of ():] is non empty set
K584( the carrier of (), the addF of (),(X . tv),(- (X . e))) is Element of the carrier of ()
[(X . tv),(- (X . e))] is set
{(X . tv),(- (X . e))} is set
{(X . tv)} is set
{{(X . tv),(- (X . e))},{(X . tv)}} is set
the addF of () . [(X . tv),(- (X . e))] is set
seq_id ((X . tv) - (X . e)) is non empty Relation-like NAT -defined REAL -valued Function-like V23( NAT ) quasi_total V105() V106() V107() Element of bool [:NAT,REAL:]
seq_id (X . tv) is non empty Relation-like NAT -defined REAL -valued Function-like V23( NAT ) quasi_total V105() V106() V107() Element of bool [:NAT,REAL:]
seq_id (X . e) is non empty Relation-like NAT -defined REAL -valued Function-like V23( NAT ) quasi_total V105() V106() V107() Element of bool [:NAT,REAL:]
(seq_id (X . tv)) - (seq_id (X . e)) is non empty Relation-like NAT -defined REAL -valued Function-like V23( NAT ) quasi_total V105() V106() V107() Element of bool [:NAT,REAL:]
- (seq_id (X . e)) is Relation-like NAT -defined Function-like V23( NAT ) V105() V106() V107() set
K38(1) (#) (seq_id (X . e)) is Relation-like NAT -defined Function-like V23( NAT ) V105() V106() V107() set
(seq_id (X . tv)) + (- (seq_id (X . e))) is Relation-like NAT -defined Function-like V23( NAT ) V105() V106() V107() set
seq_id ((seq_id (X . tv)) - (seq_id (X . e))) is non empty Relation-like NAT -defined REAL -valued Function-like V23( NAT ) quasi_total V105() V106() V107() Element of bool [:NAT,REAL:]
tv is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V115() V116() V117() V118() V119() V120() V145() V168() Element of NAT
vseq . tv is V11() real ext-real Element of REAL
e is non empty Relation-like NAT -defined REAL -valued Function-like V23( NAT ) quasi_total V105() V106() V107() Element of bool [:NAT,REAL:]
lim e is V11() real ext-real Element of REAL
m is non empty Relation-like NAT -defined REAL -valued Function-like V23( NAT ) quasi_total V105() V106() V107() Element of bool [:NAT,REAL:]
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V115() V116() V117() V118() V119() V120() V145() V168() Element of NAT
X . n is Element of the carrier of ()
(X . n) - (X . tseq) is Element of the carrier of ()
- (X . tseq) is Element of the carrier of ()
(X . n) + (- (X . tseq)) is Element of the carrier of ()
the addF of () is non empty Relation-like [: the carrier of (), the carrier of ():] -defined the carrier of () -valued Function-like V23([: the carrier of (), the carrier of ():]) quasi_total Element of bool [:[: the carrier of (), the carrier of ():], the carrier of ():]
[: the carrier of (), the carrier of ():] is non empty Relation-like set
[:[: the carrier of (), the carrier of ():], the carrier of ():] is non empty Relation-like set
bool [:[: the carrier of (), the carrier of ():], the carrier of ():] is non empty set
K584( the carrier of (), the addF of (),(X . n),(- (X . tseq))) is Element of the carrier of ()
[(X . n),(- (X . tseq))] is set
{(X . n),(- (X . tseq))} is set
{(X . n)} is set
{{(X . n),(- (X . tseq))},{(X . n)}} is set
the addF of () . [(X . n),(- (X . tseq))] is set
seq_id ((X . n) - (X . tseq)) is non empty Relation-like NAT -defined REAL -valued Function-like V23( NAT ) quasi_total V105() V106() V107() Element of bool [:NAT,REAL:]
seq_id (X . n) is non empty Relation-like NAT -defined REAL -valued Function-like V23( NAT ) quasi_total V105() V106() V107() Element of bool [:NAT,REAL:]
(seq_id (X . n)) - (seq_id (X . tseq)) is non empty Relation-like NAT -defined REAL -valued Function-like V23( NAT ) quasi_total V105() V106() V107() Element of bool [:NAT,REAL:]
(seq_id (X . n)) + (- (seq_id (X . tseq))) is Relation-like NAT -defined Function-like V23( NAT ) V105() V106() V107() set
m . n is V11() real ext-real Element of REAL
abs (seq_id ((X . n) - (X . tseq))) is non empty Relation-like NAT -defined REAL -valued Function-like V23( NAT ) quasi_total V105() V106() V107() bounded_below Element of bool [:NAT,REAL:]
(abs (seq_id ((X . n) - (X . tseq)))) . tv is V11() real ext-real Element of REAL
(seq_id ((X . n) - (X . tseq))) . tv is V11() real ext-real Element of REAL
abs ((seq_id ((X . n) - (X . tseq))) . tv) is V11() real ext-real Element of REAL
(seq_id (X . n)) . tv is V11() real ext-real Element of REAL
(seq_id (X . tseq)) . tv is V11() real ext-real Element of REAL
((seq_id (X . n)) . tv) - ((seq_id (X . tseq)) . tv) is V11() real ext-real Element of REAL
abs (((seq_id (X . n)) . tv) - ((seq_id (X . tseq)) . tv)) is V11() real ext-real Element of REAL
e . n is V11() real ext-real Element of REAL
(e . n) - ((seq_id (X . tseq)) . tv) is V11() real ext-real Element of REAL
abs ((e . n) - ((seq_id (X . tseq)) . tv)) is V11() real ext-real Element of REAL
(vseq . tv) - ((seq_id (X . tseq)) . tv) is V11() real ext-real Element of REAL
abs ((vseq . tv) - ((seq_id (X . tseq)) . tv)) is V11() real ext-real Element of REAL
vseq - (seq_id (X . tseq)) is non empty Relation-like NAT -defined REAL -valued Function-like V23( NAT ) quasi_total V105() V106() V107() Element of bool [:NAT,REAL:]
vseq + (- (seq_id (X . tseq))) is Relation-like NAT -defined Function-like V23( NAT ) V105() V106() V107() set
(vseq - (seq_id (X . tseq))) . tv is V11() real ext-real Element of REAL
abs ((vseq - (seq_id (X . tseq))) . tv) is V11() real ext-real Element of REAL
((seq_id vseq) - (seq_id (X . tseq))) . tv is V11() real ext-real Element of REAL
abs (((seq_id vseq) - (seq_id (X . tseq))) . tv) is V11() real ext-real Element of REAL
(abs ((seq_id vseq) - (seq_id (X . tseq)))) . tv is V11() real ext-real Element of REAL
lim m is V11() real ext-real Element of REAL
m is non