:: RSSPACE4 semantic presentation

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 empty Relation-like NAT -defined REAL -valued Function-like V23( NAT ) quasi_total V105() V106() V107() Element of bool [:NAT,REAL:]
lim m 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:]
tv is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V115() V116() V117() V118() V119() V120() V145() V168() Element of NAT
lim e 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
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:]
rng (abs ((seq_id vseq) - (seq_id (X . tseq)))) is non empty V115() V116() V117() Element of bool REAL
upper_bound (rng (abs ((seq_id vseq) - (seq_id (X . 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
(abs ((seq_id vseq) - (seq_id (X . tseq)))) . 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:]
m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V115() V116() V117() V118() V119() V120() V145() V168() Element of NAT
e . m is V11() real ext-real Element of REAL
X . m is Element of the carrier of ()
(X . m) - (X . tseq) is Element of the carrier of ()
- (X . tseq) is Element of the carrier of ()
(X . m) + (- (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 . m),(- (X . tseq))) is Element of the carrier of ()
[(X . m),(- (X . tseq))] is set
{(X . m),(- (X . tseq))} is set
{(X . m)} is set
{{(X . m),(- (X . tseq))},{(X . m)}} is set
the addF of () . [(X . m),(- (X . tseq))] is set
seq_id ((X . m) - (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 . m) - (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 . m) - (X . tseq)))) . tv is V11() real ext-real Element of REAL
rng (abs (seq_id ((X . m) - (X . tseq)))) is non empty V115() V116() V117() Element of bool REAL
upper_bound (rng (abs (seq_id ((X . m) - (X . tseq))))) is V11() real ext-real Element of REAL
lim e is V11() real ext-real Element of REAL
1 + f is V11() real ext-real Element of REAL
0 + f 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
(abs ((seq_id 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
f + 1 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
X . f is Element of the carrier of ()
seq_id (X . f) 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 . f)) 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 . f)) 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 . f)) is Relation-like NAT -defined Function-like V23( NAT ) V105() V106() V107() set
(seq_id vseq) + (- (seq_id (X . f))) is Relation-like NAT -defined Function-like V23( NAT ) V105() V106() V107() set
abs ((seq_id vseq) - (seq_id (X . f))) 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 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:]
abs (seq_id (X . f)) 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 vseq) - (seq_id (X . f)))) + (abs (seq_id (X . f))) 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:]
e 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 vseq)) . e is V11() real ext-real Element of REAL
((abs ((seq_id vseq) - (seq_id (X . f)))) + (abs (seq_id (X . f)))) . e is V11() real ext-real Element of REAL
(abs (seq_id (X . f))) . e is V11() real ext-real Element of REAL
(seq_id (X . f)) . e is V11() real ext-real Element of REAL
abs ((seq_id (X . f)) . e) is V11() real ext-real Element of REAL
(seq_id vseq) . e is V11() real ext-real Element of REAL
abs ((seq_id vseq) . e) is V11() real ext-real Element of REAL
(abs ((seq_id vseq) - (seq_id (X . f)))) . e is V11() real ext-real Element of REAL
- (seq_id (X . f)) 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 . f))) 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 . f)))) . e is V11() real ext-real Element of REAL
abs (((seq_id vseq) + (- (seq_id (X . f)))) . e) is V11() real ext-real Element of REAL
(- (seq_id (X . f))) . e is V11() real ext-real Element of REAL
((seq_id vseq) . e) + ((- (seq_id (X . f))) . e) is V11() real ext-real Element of REAL
abs (((seq_id vseq) . e) + ((- (seq_id (X . f))) . e)) is V11() real ext-real Element of REAL
- ((seq_id (X . f)) . e) is V11() real ext-real Element of REAL
((seq_id vseq) . e) + (- ((seq_id (X . f)) . e)) is V11() real ext-real Element of REAL
abs (((seq_id vseq) . e) + (- ((seq_id (X . f)) . e))) is V11() real ext-real Element of REAL
((seq_id vseq) . e) - ((seq_id (X . f)) . e) is V11() real ext-real Element of REAL
abs (((seq_id vseq) . e) - ((seq_id (X . f)) . e)) is V11() real ext-real Element of REAL
((abs (seq_id vseq)) . e) - ((abs (seq_id (X . f))) . e) is V11() real ext-real Element of REAL
(((abs (seq_id vseq)) . e) - ((abs (seq_id (X . f))) . e)) + ((abs (seq_id (X . f))) . e) is V11() real ext-real Element of REAL
((abs ((seq_id vseq) - (seq_id (X . f)))) . e) + ((abs (seq_id (X . f))) . e) is V11() real ext-real Element of REAL
rng ((abs ((seq_id vseq) - (seq_id (X . f)))) + (abs (seq_id (X . f)))) is non empty V115() V116() V117() Element of bool REAL
upper_bound (rng ((abs ((seq_id vseq) - (seq_id (X . f)))) + (abs (seq_id (X . f))))) is V11() real ext-real Element of REAL
(upper_bound (rng ((abs ((seq_id vseq) - (seq_id (X . f)))) + (abs (seq_id (X . f)))))) + 1 is V11() real ext-real Element of REAL
(abs (seq_id (X . f))) . 1 is V11() real ext-real Element of REAL
(seq_id (X . f)) . 1 is V11() real ext-real Element of REAL
abs ((seq_id (X . f)) . 1) is V11() real ext-real Element of REAL
(upper_bound (rng ((abs ((seq_id vseq) - (seq_id (X . f)))) + (abs (seq_id (X . f)))))) + 0 is V11() real ext-real Element of REAL
m 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 vseq)) . m is V11() real ext-real Element of REAL
((abs ((seq_id vseq) - (seq_id (X . f)))) + (abs (seq_id (X . f)))) . m is V11() real ext-real Element of REAL
(seq_id vseq) . m is V11() real ext-real Element of REAL
abs ((seq_id vseq) . m) is V11() real ext-real Element of REAL
e is V11() real ext-real set
(abs ((seq_id vseq) - (seq_id (X . f)))) . 1 is V11() real ext-real Element of REAL
((seq_id vseq) - (seq_id (X . f))) . 1 is V11() real ext-real Element of REAL
abs (((seq_id vseq) - (seq_id (X . f))) . 1) is V11() real ext-real Element of REAL
((abs ((seq_id vseq) - (seq_id (X . f)))) + (abs (seq_id (X . f)))) . 1 is V11() real ext-real Element of REAL
((abs ((seq_id vseq) - (seq_id (X . f)))) . 1) + ((abs (seq_id (X . f))) . 1) is V11() real ext-real Element of REAL
f is Element of the carrier of ()
tseq is V11() real ext-real Element of REAL
tseq / 2 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
m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V115() V116() V117() V118() V119() V120() V145() V168() Element of NAT
X . m is Element of the carrier of ()
seq_id (X . 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 vseq) - (seq_id (X . 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 (X . m)) 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 . m)) is Relation-like NAT -defined Function-like V23( NAT ) V105() V106() V107() set
(seq_id vseq) + (- (seq_id (X . m))) is Relation-like NAT -defined Function-like V23( NAT ) V105() V106() V107() set
abs ((seq_id vseq) - (seq_id (X . m))) 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 . m)))) is non empty V115() V116() V117() Element of bool REAL
upper_bound (rng (abs ((seq_id vseq) - (seq_id (X . m))))) is V11() real ext-real Element of REAL
e is Element of the carrier of ()
n is Element of the carrier of ()
e - n is Element of the carrier of ()
- n is Element of the carrier of ()
e + (- n) 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 (),e,(- n)) is Element of the carrier of ()
[e,(- n)] is set
{e,(- n)} is set
{e} is set
{{e,(- n)},{e}} is set
the addF of () . [e,(- n)] is set
seq_id (e - n) 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 (e - n)) 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 (e - n))) is non empty V115() V116() V117() Element of bool REAL
upper_bound (rng (abs (seq_id (e - n)))) 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 () . (e - n) is V11() real ext-real Element of REAL
(X . m) - f is Element of the carrier of ()
- f is Element of the carrier of ()
(X . m) + (- f) is Element of the carrier of ()
K584( the carrier of (), the addF of (),(X . m),(- f)) is Element of the carrier of ()
[(X . m),(- f)] is set
{(X . m),(- f)} is set
{(X . m)} is set
{{(X . m),(- f)},{(X . m)}} is set
the addF of () . [(X . m),(- f)] is set
||.((X . m) - f).|| is V11() real ext-real non negative Element of REAL
the normF of () . ((X . m) - f) is V11() real ext-real Element of REAL
f - (X . m) is Element of the carrier of ()
- (X . m) is Element of the carrier of ()
f + (- (X . m)) is Element of the carrier of ()
K584( the carrier of (), the addF of (),f,(- (X . m))) is Element of the carrier of ()
[f,(- (X . m))] is set
{f,(- (X . m))} is set
{f} is set
{{f,(- (X . m))},{f}} is set
the addF of () . [f,(- (X . m))] is set
- (f - (X . m)) is Element of the carrier of ()
||.(- (f - (X . m))).|| is V11() real ext-real non negative Element of REAL
the normF of () . (- (f - (X . m))) is V11() real ext-real Element of REAL
||.(f - (X . m)).|| is V11() real ext-real non negative Element of REAL
the normF of () . (f - (X . m)) is V11() real ext-real Element of REAL
X is non empty set
Y is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like NORMSTR
the carrier of Y is non empty set
[:X, the carrier of Y:] is non empty Relation-like set
bool [:X, the carrier of Y:] is non empty set
X is non empty set
Y is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like NORMSTR
the carrier of Y is non empty set
[:X, the carrier of Y:] is non empty Relation-like set
bool [:X, the carrier of Y:] is non empty set
0. Y is V49(Y) Element of the carrier of Y
the ZeroF of Y is Element of the carrier of Y
vseq is non empty Relation-like X -defined the carrier of Y -valued Function-like V23(X) quasi_total Element of bool [:X, the carrier of Y:]
f is Element of X
vseq . f is Element of the carrier of Y
||.(vseq . f).|| is V11() real ext-real non negative Element of REAL
the normF of Y is non empty Relation-like the carrier of Y -defined REAL -valued Function-like V23( the carrier of Y) quasi_total V105() V106() V107() Element of bool [: the carrier of Y,REAL:]
[: the carrier of Y,REAL:] is non empty Relation-like V105() V106() V107() set
bool [: the carrier of Y,REAL:] is non empty set
the normF of Y . (vseq . f) is V11() real ext-real Element of REAL
||.(0. Y).|| 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() Element of REAL
the normF of Y . (0. Y) is V11() real ext-real Element of REAL
f is Element of X
vseq . f is Element of the carrier of Y
||.(vseq . f).|| is V11() real ext-real non negative Element of REAL
the normF of Y . (vseq . f) is V11() real ext-real Element of REAL
X is non empty set
Y is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like NORMSTR
the carrier of Y is non empty set
[:X, the carrier of Y:] is non empty Relation-like set
bool [:X, the carrier of Y:] is non empty set
0. Y is V49(Y) Element of the carrier of Y
the ZeroF of Y is Element of the carrier of Y
X --> (0. Y) is non empty Relation-like X -defined the carrier of Y -valued Function-like constant V23(X) quasi_total Element of bool [:X, the carrier of Y:]
f is non empty Relation-like X -defined the carrier of Y -valued Function-like V23(X) quasi_total Element of bool [:X, the carrier of Y:]
tseq is Element of X
f . tseq is Element of the carrier of Y
X is non empty set
Y is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like NORMSTR
RealVectSpace (X,Y) is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() RLSStruct
the carrier of (RealVectSpace (X,Y)) is non empty set
bool the carrier of (RealVectSpace (X,Y)) is non empty set
the carrier of Y is non empty set
[:X, the carrier of Y:] is non empty Relation-like set
bool [:X, the carrier of Y:] is non empty set
Funcs (X, the carrier of Y) is non empty functional FUNCTION_DOMAIN of X, the carrier of Y
FuncZero (X,Y) is Relation-like X -defined the carrier of Y -valued Function-like V23(X) quasi_total Element of Funcs (X, the carrier of Y)
FuncAdd (X,Y) is non empty Relation-like [:(Funcs (X, the carrier of Y)),(Funcs (X, the carrier of Y)):] -defined Funcs (X, the carrier of Y) -valued Function-like V23([:(Funcs (X, the carrier of Y)),(Funcs (X, the carrier of Y)):]) quasi_total Function-yielding V144() Element of bool [:[:(Funcs (X, the carrier of Y)),(Funcs (X, the carrier of Y)):],(Funcs (X, the carrier of Y)):]
[:(Funcs (X, the carrier of Y)),(Funcs (X, the carrier of Y)):] is non empty Relation-like set
[:[:(Funcs (X, the carrier of Y)),(Funcs (X, the carrier of Y)):],(Funcs (X, the carrier of Y)):] is non empty Relation-like set
bool [:[:(Funcs (X, the carrier of Y)),(Funcs (X, the carrier of Y)):],(Funcs (X, the carrier of Y)):] is non empty set
FuncExtMult (X,Y) is non empty Relation-like [:REAL,(Funcs (X, the carrier of Y)):] -defined Funcs (X, the carrier of Y) -valued Function-like V23([:REAL,(Funcs (X, the carrier of Y)):]) quasi_total Function-yielding V144() Element of bool [:[:REAL,(Funcs (X, the carrier of Y)):],(Funcs (X, the carrier of Y)):]
[:REAL,(Funcs (X, the carrier of Y)):] is non empty Relation-like set
[:[:REAL,(Funcs (X, the carrier of Y)):],(Funcs (X, the carrier of Y)):] is non empty Relation-like set
bool [:[:REAL,(Funcs (X, the carrier of Y)):],(Funcs (X, the carrier of Y)):] is non empty set
RLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(FuncExtMult (X,Y)) #) is non empty strict RLSStruct
vseq is set
f is set
f is set
vseq is Element of bool the carrier of (RealVectSpace (X,Y))
f is Element of bool the carrier of (RealVectSpace (X,Y))
tseq is set
tseq is set
X is non empty set
Y is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like NORMSTR
(X,Y) is Element of bool the carrier of (RealVectSpace (X,Y))
RealVectSpace (X,Y) is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() RLSStruct
the carrier of (RealVectSpace (X,Y)) is non empty set
bool the carrier of (RealVectSpace (X,Y)) is non empty set
the carrier of Y is non empty set
0. Y is V49(Y) Element of the carrier of Y
the ZeroF of Y is Element of the carrier of Y
X --> (0. Y) is non empty Relation-like X -defined the carrier of Y -valued Function-like constant V23(X) quasi_total Element of bool [:X, the carrier of Y:]
[:X, the carrier of Y:] is non empty Relation-like set
bool [:X, the carrier of Y:] is non empty set
f is non empty Relation-like X -defined the carrier of Y -valued Function-like V23(X) quasi_total Element of bool [:X, the carrier of Y:]
tseq is Element of X
f . tseq is Element of the carrier of Y
X is non empty set
Y is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like NORMSTR
RealVectSpace (X,Y) is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() RLSStruct
(X,Y) is non empty Element of bool the carrier of (RealVectSpace (X,Y))
the carrier of (RealVectSpace (X,Y)) is non empty set
bool the carrier of (RealVectSpace (X,Y)) is non empty set
the carrier of Y is non empty set
Funcs (X, the carrier of Y) is non empty functional FUNCTION_DOMAIN of X, the carrier of Y
FuncZero (X,Y) is Relation-like X -defined the carrier of Y -valued Function-like V23(X) quasi_total Element of Funcs (X, the carrier of Y)
FuncAdd (X,Y) is non empty Relation-like [:(Funcs (X, the carrier of Y)),(Funcs (X, the carrier of Y)):] -defined Funcs (X, the carrier of Y) -valued Function-like V23([:(Funcs (X, the carrier of Y)),(Funcs (X, the carrier of Y)):]) quasi_total Function-yielding V144() Element of bool [:[:(Funcs (X, the carrier of Y)),(Funcs (X, the carrier of Y)):],(Funcs (X, the carrier of Y)):]
[:(Funcs (X, the carrier of Y)),(Funcs (X, the carrier of Y)):] is non empty Relation-like set
[:[:(Funcs (X, the carrier of Y)),(Funcs (X, the carrier of Y)):],(Funcs (X, the carrier of Y)):] is non empty Relation-like set
bool [:[:(Funcs (X, the carrier of Y)),(Funcs (X, the carrier of Y)):],(Funcs (X, the carrier of Y)):] is non empty set
FuncExtMult (X,Y) is non empty Relation-like [:REAL,(Funcs (X, the carrier of Y)):] -defined Funcs (X, the carrier of Y) -valued Function-like V23([:REAL,(Funcs (X, the carrier of Y)):]) quasi_total Function-yielding V144() Element of bool [:[:REAL,(Funcs (X, the carrier of Y)):],(Funcs (X, the carrier of Y)):]
[:REAL,(Funcs (X, the carrier of Y)):] is non empty Relation-like set
[:[:REAL,(Funcs (X, the carrier of Y)):],(Funcs (X, the carrier of Y)):] is non empty Relation-like set
bool [:[:REAL,(Funcs (X, the carrier of Y)):],(Funcs (X, the carrier of Y)):] is non empty set
RLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(FuncExtMult (X,Y)) #) is non empty strict RLSStruct
f is Element of the carrier of (RealVectSpace (X,Y))
tseq is Element of the carrier of (RealVectSpace (X,Y))
f + tseq is Element of the carrier of (RealVectSpace (X,Y))
the addF of (RealVectSpace (X,Y)) is non empty Relation-like [: the carrier of (RealVectSpace (X,Y)), the carrier of (RealVectSpace (X,Y)):] -defined the carrier of (RealVectSpace (X,Y)) -valued Function-like V23([: the carrier of (RealVectSpace (X,Y)), the carrier of (RealVectSpace (X,Y)):]) quasi_total Element of bool [:[: the carrier of (RealVectSpace (X,Y)), the carrier of (RealVectSpace (X,Y)):], the carrier of (RealVectSpace (X,Y)):]
[: the carrier of (RealVectSpace (X,Y)), the carrier of (RealVectSpace (X,Y)):] is non empty Relation-like set
[:[: the carrier of (RealVectSpace (X,Y)), the carrier of (RealVectSpace (X,Y)):], the carrier of (RealVectSpace (X,Y)):] is non empty Relation-like set
bool [:[: the carrier of (RealVectSpace (X,Y)), the carrier of (RealVectSpace (X,Y)):], the carrier of (RealVectSpace (X,Y)):] is non empty set
K584( the carrier of (RealVectSpace (X,Y)), the addF of (RealVectSpace (X,Y)),f,tseq) is Element of the carrier of (RealVectSpace (X,Y))
[f,tseq] is set
{f,tseq} is set
{f} is set
{{f,tseq},{f}} is set
the addF of (RealVectSpace (X,Y)) . [f,tseq] is set
[:X, the carrier of Y:] is non empty Relation-like set
bool [:X, the carrier of Y:] is non empty set
tseq is non empty Relation-like X -defined the carrier of Y -valued Function-like V23(X) quasi_total Element of bool [:X, the carrier of Y:]
tv is non empty Relation-like X -defined the carrier of Y -valued Function-like V23(X) quasi_total (X,Y) Element of bool [:X, the carrier of Y:]
e is V11() real ext-real Element of REAL
m is non empty Relation-like X -defined the carrier of Y -valued Function-like V23(X) quasi_total (X,Y) Element of bool [:X, the carrier of Y:]
n is V11() real ext-real Element of REAL
n + e is V11() real ext-real Element of REAL
n is V11() real ext-real Element of REAL
h1 is Element of X
m . h1 is Element of the carrier of Y
||.(m . h1).|| is V11() real ext-real non negative Element of REAL
the normF of Y is non empty Relation-like the carrier of Y -defined REAL -valued Function-like V23( the carrier of Y) quasi_total V105() V106() V107() Element of bool [: the carrier of Y,REAL:]
[: the carrier of Y,REAL:] is non empty Relation-like V105() V106() V107() set
bool [: the carrier of Y,REAL:] is non empty set
the normF of Y . (m . h1) is V11() real ext-real Element of REAL
tv . h1 is Element of the carrier of Y
||.(tv . h1).|| is V11() real ext-real non negative Element of REAL
the normF of Y . (tv . h1) is V11() real ext-real Element of REAL
||.(m . h1).|| + ||.(tv . h1).|| is V11() real ext-real non negative Element of REAL
tseq . h1 is Element of the carrier of Y
||.(tseq . h1).|| is V11() real ext-real non negative Element of REAL
the normF of Y . (tseq . h1) is V11() real ext-real Element of REAL
(tv . h1) + (m . h1) is Element of the carrier of Y
the addF of Y is non empty Relation-like [: the carrier of Y, the carrier of Y:] -defined the carrier of Y -valued Function-like V23([: the carrier of Y, the carrier of Y:]) quasi_total Element of bool [:[: the carrier of Y, the carrier of Y:], the carrier of Y:]
[: the carrier of Y, the carrier of Y:] is non empty Relation-like set
[:[: the carrier of Y, the carrier of Y:], the carrier of Y:] is non empty Relation-like set
bool [:[: the carrier of Y, the carrier of Y:], the carrier of Y:] is non empty set
K584( the carrier of Y, the addF of Y,(tv . h1),(m . h1)) is Element of the carrier of Y
[(tv . h1),(m . h1)] is set
{(tv . h1),(m . h1)} is set
{(tv . h1)} is set
{{(tv . h1),(m . h1)},{(tv . h1)}} is set
the addF of Y . [(tv . h1),(m . h1)] is set
||.((tv . h1) + (m . h1)).|| is V11() real ext-real non negative Element of REAL
the normF of Y . ((tv . h1) + (m . h1)) is V11() real ext-real Element of REAL
(m . h1) + (tv . h1) is Element of the carrier of Y
K584( the carrier of Y, the addF of Y,(m . h1),(tv . h1)) is Element of the carrier of Y
[(m . h1),(tv . h1)] is set
{(m . h1),(tv . h1)} is set
{(m . h1)} is set
{{(m . h1),(tv . h1)},{(m . h1)}} is set
the addF of Y . [(m . h1),(tv . h1)] is set
||.((m . h1) + (tv . h1)).|| is V11() real ext-real non negative Element of REAL
the normF of Y . ((m . h1) + (tv . h1)) is V11() real ext-real Element of REAL
h1 is Element of X
tseq . h1 is Element of the carrier of Y
||.(tseq . h1).|| is V11() real ext-real non negative Element of REAL
the normF of Y . (tseq . h1) is V11() real ext-real Element of REAL
f is V11() real ext-real Element of REAL
tseq is Element of the carrier of (RealVectSpace (X,Y))
f * tseq is Element of the carrier of (RealVectSpace (X,Y))
the Mult of (RealVectSpace (X,Y)) is non empty Relation-like [:REAL, the carrier of (RealVectSpace (X,Y)):] -defined the carrier of (RealVectSpace (X,Y)) -valued Function-like V23([:REAL, the carrier of (RealVectSpace (X,Y)):]) quasi_total Element of bool [:[:REAL, the carrier of (RealVectSpace (X,Y)):], the carrier of (RealVectSpace (X,Y)):]
[:REAL, the carrier of (RealVectSpace (X,Y)):] is non empty Relation-like set
[:[:REAL, the carrier of (RealVectSpace (X,Y)):], the carrier of (RealVectSpace (X,Y)):] is non empty Relation-like set
bool [:[:REAL, the carrier of (RealVectSpace (X,Y)):], the carrier of (RealVectSpace (X,Y)):] is non empty set
K580( the Mult of (RealVectSpace (X,Y)),f,tseq) is set
[f,tseq] is set
{f,tseq} is set
{f} is V115() V116() V117() set
{{f,tseq},{f}} is set
the Mult of (RealVectSpace (X,Y)) . [f,tseq] is set
[:X, the carrier of Y:] is non empty Relation-like set
bool [:X, the carrier of Y:] is non empty set
tseq is non empty Relation-like X -defined the carrier of Y -valued Function-like V23(X) quasi_total Element of bool [:X, the carrier of Y:]
tv is non empty Relation-like X -defined the carrier of Y -valued Function-like V23(X) quasi_total (X,Y) Element of bool [:X, the carrier of Y:]
e is V11() real ext-real Element of REAL
abs f is V11() real ext-real Element of REAL
(abs f) * e is V11() real ext-real Element of REAL
m is Element of X
tseq . m is Element of the carrier of Y
||.(tseq . m).|| is V11() real ext-real non negative Element of REAL
the normF of Y is non empty Relation-like the carrier of Y -defined REAL -valued Function-like V23( the carrier of Y) quasi_total V105() V106() V107() Element of bool [: the carrier of Y,REAL:]
[: the carrier of Y,REAL:] is non empty Relation-like V105() V106() V107() set
bool [: the carrier of Y,REAL:] is non empty set
the normF of Y . (tseq . m) is V11() real ext-real Element of REAL
tv . m is Element of the carrier of Y
f * (tv . m) is Element of the carrier of Y
the Mult of Y is non empty Relation-like [:REAL, the carrier of Y:] -defined the carrier of Y -valued Function-like V23([:REAL, the carrier of Y:]) quasi_total Element of bool [:[:REAL, the carrier of Y:], the carrier of Y:]
[:REAL, the carrier of Y:] is non empty Relation-like set
[:[:REAL, the carrier of Y:], the carrier of Y:] is non empty Relation-like set
bool [:[:REAL, the carrier of Y:], the carrier of Y:] is non empty set
K580( the Mult of Y,f,(tv . m)) is set
[f,(tv . m)] is set
{f,(tv . m)} is set
{{f,(tv . m)},{f}} is set
the Mult of Y . [f,(tv . m)] is set
||.(f * (tv . m)).|| is V11() real ext-real non negative Element of REAL
the normF of Y . (f * (tv . m)) is V11() real ext-real Element of REAL
||.(tv . m).|| is V11() real ext-real non negative Element of REAL
the normF of Y . (tv . m) is V11() real ext-real Element of REAL
(abs f) * ||.(tv . m).|| is V11() real ext-real Element of REAL
m is Element of X
tseq . m is Element of the carrier of Y
||.(tseq . m).|| is V11() real ext-real non negative Element of REAL
the normF of Y . (tseq . m) is V11() real ext-real Element of REAL
X is non empty set
Y is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like NORMSTR
(X,Y) is non empty Element of bool the carrier of (RealVectSpace (X,Y))
RealVectSpace (X,Y) is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() RLSStruct
the carrier of (RealVectSpace (X,Y)) is non empty set
bool the carrier of (RealVectSpace (X,Y)) is non empty set
Zero_ ((X,Y),(RealVectSpace (X,Y))) is Element of (X,Y)
Add_ ((X,Y),(RealVectSpace (X,Y))) is non empty Relation-like [:(X,Y),(X,Y):] -defined (X,Y) -valued Function-like V23([:(X,Y),(X,Y):]) quasi_total Element of bool [:[:(X,Y),(X,Y):],(X,Y):]
[:(X,Y),(X,Y):] is non empty Relation-like set
[:[:(X,Y),(X,Y):],(X,Y):] is non empty Relation-like set
bool [:[:(X,Y),(X,Y):],(X,Y):] is non empty set
Mult_ ((X,Y),(RealVectSpace (X,Y))) is non empty Relation-like [:REAL,(X,Y):] -defined (X,Y) -valued Function-like V23([:REAL,(X,Y):]) quasi_total Element of bool [:[:REAL,(X,Y):],(X,Y):]
[:REAL,(X,Y):] is non empty Relation-like set
[:[:REAL,(X,Y):],(X,Y):] is non empty Relation-like set
bool [:[:REAL,(X,Y):],(X,Y):] is non empty set
RLSStruct(# (X,Y),(Zero_ ((X,Y),(RealVectSpace (X,Y)))),(Add_ ((X,Y),(RealVectSpace (X,Y)))),(Mult_ ((X,Y),(RealVectSpace (X,Y)))) #) is non empty strict RLSStruct
X is non empty set
Y is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like NORMSTR
(X,Y) is non empty Element of bool the carrier of (RealVectSpace (X,Y))
RealVectSpace (X,Y) is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() RLSStruct
the carrier of (RealVectSpace (X,Y)) is non empty set
bool the carrier of (RealVectSpace (X,Y)) is non empty set
Zero_ ((X,Y),(RealVectSpace (X,Y))) is Element of (X,Y)
Add_ ((X,Y),(RealVectSpace (X,Y))) is non empty Relation-like [:(X,Y),(X,Y):] -defined (X,Y) -valued Function-like V23([:(X,Y),(X,Y):]) quasi_total Element of bool [:[:(X,Y),(X,Y):],(X,Y):]
[:(X,Y),(X,Y):] is non empty Relation-like set
[:[:(X,Y),(X,Y):],(X,Y):] is non empty Relation-like set
bool [:[:(X,Y),(X,Y):],(X,Y):] is non empty set
Mult_ ((X,Y),(RealVectSpace (X,Y))) is non empty Relation-like [:REAL,(X,Y):] -defined (X,Y) -valued Function-like V23([:REAL,(X,Y):]) quasi_total Element of bool [:[:REAL,(X,Y):],(X,Y):]
[:REAL,(X,Y):] is non empty Relation-like set
[:[:REAL,(X,Y):],(X,Y):] is non empty Relation-like set
bool [:[:REAL,(X,Y):],(X,Y):] is non empty set
RLSStruct(# (X,Y),(Zero_ ((X,Y),(RealVectSpace (X,Y)))),(Add_ ((X,Y),(RealVectSpace (X,Y)))),(Mult_ ((X,Y),(RealVectSpace (X,Y)))) #) is non empty strict RLSStruct
X is non empty set
Y is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like NORMSTR
(X,Y) is non empty Element of bool the carrier of (RealVectSpace (X,Y))
RealVectSpace (X,Y) is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() RLSStruct
the carrier of (RealVectSpace (X,Y)) is non empty set
bool the carrier of (RealVectSpace (X,Y)) is non empty set
Zero_ ((X,Y),(RealVectSpace (X,Y))) is Element of (X,Y)
Add_ ((X,Y),(RealVectSpace (X,Y))) is non empty Relation-like [:(X,Y),(X,Y):] -defined (X,Y) -valued Function-like V23([:(X,Y),(X,Y):]) quasi_total Element of bool [:[:(X,Y),(X,Y):],(X,Y):]
[:(X,Y),(X,Y):] is non empty Relation-like set
[:[:(X,Y),(X,Y):],(X,Y):] is non empty Relation-like set
bool [:[:(X,Y),(X,Y):],(X,Y):] is non empty set
Mult_ ((X,Y),(RealVectSpace (X,Y))) is non empty Relation-like [:REAL,(X,Y):] -defined (X,Y) -valued Function-like V23([:REAL,(X,Y):]) quasi_total Element of bool [:[:REAL,(X,Y):],(X,Y):]
[:REAL,(X,Y):] is non empty Relation-like set
[:[:REAL,(X,Y):],(X,Y):] is non empty Relation-like set
bool [:[:REAL,(X,Y):],(X,Y):] is non empty set
RLSStruct(# (X,Y),(Zero_ ((X,Y),(RealVectSpace (X,Y)))),(Add_ ((X,Y),(RealVectSpace (X,Y)))),(Mult_ ((X,Y),(RealVectSpace (X,Y)))) #) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() RLSStruct
X is non empty set
Y is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like NORMSTR
(X,Y) is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() RLSStruct
(X,Y) is non empty Element of bool the carrier of (RealVectSpace (X,Y))
RealVectSpace (X,Y) is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() RLSStruct
the carrier of (RealVectSpace (X,Y)) is non empty set
bool the carrier of (RealVectSpace (X,Y)) is non empty set
Zero_ ((X,Y),(RealVectSpace (X,Y))) is Element of (X,Y)
Add_ ((X,Y),(RealVectSpace (X,Y))) is non empty Relation-like [:(X,Y),(X,Y):] -defined (X,Y) -valued Function-like V23([:(X,Y),(X,Y):]) quasi_total Element of bool [:[:(X,Y),(X,Y):],(X,Y):]
[:(X,Y),(X,Y):] is non empty Relation-like set
[:[:(X,Y),(X,Y):],(X,Y):] is non empty Relation-like set
bool [:[:(X,Y),(X,Y):],(X,Y):] is non empty set
Mult_ ((X,Y),(RealVectSpace (X,Y))) is non empty Relation-like [:REAL,(X,Y):] -defined (X,Y) -valued Function-like V23([:REAL,(X,Y):]) quasi_total Element of bool [:[:REAL,(X,Y):],(X,Y):]
[:REAL,(X,Y):] is non empty Relation-like set
[:[:REAL,(X,Y):],(X,Y):] is non empty Relation-like set
bool [:[:REAL,(X,Y):],(X,Y):] is non empty set
RLSStruct(# (X,Y),(Zero_ ((X,Y),(RealVectSpace (X,Y)))),(Add_ ((X,Y),(RealVectSpace (X,Y)))),(Mult_ ((X,Y),(RealVectSpace (X,Y)))) #) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() RLSStruct
X is non empty set
Y is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like NORMSTR
(X,Y) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() RLSStruct
(X,Y) is non empty Element of bool the carrier of (RealVectSpace (X,Y))
RealVectSpace (X,Y) is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() RLSStruct
the carrier of (RealVectSpace (X,Y)) is non empty set
bool the carrier of (RealVectSpace (X,Y)) is non empty set
Zero_ ((X,Y),(RealVectSpace (X,Y))) is Element of (X,Y)
Add_ ((X,Y),(RealVectSpace (X,Y))) is non empty Relation-like [:(X,Y),(X,Y):] -defined (X,Y) -valued Function-like V23([:(X,Y),(X,Y):]) quasi_total Element of bool [:[:(X,Y),(X,Y):],(X,Y):]
[:(X,Y),(X,Y):] is non empty Relation-like set
[:[:(X,Y),(X,Y):],(X,Y):] is non empty Relation-like set
bool [:[:(X,Y),(X,Y):],(X,Y):] is non empty set
Mult_ ((X,Y),(RealVectSpace (X,Y))) is non empty Relation-like [:REAL,(X,Y):] -defined (X,Y) -valued Function-like V23([:REAL,(X,Y):]) quasi_total Element of bool [:[:REAL,(X,Y):],(X,Y):]
[:REAL,(X,Y):] is non empty Relation-like set
[:[:REAL,(X,Y):],(X,Y):] is non empty Relation-like set
bool [:[:REAL,(X,Y):],(X,Y):] is non empty set
RLSStruct(# (X,Y),(Zero_ ((X,Y),(RealVectSpace (X,Y)))),(Add_ ((X,Y),(RealVectSpace (X,Y)))),(Mult_ ((X,Y),(RealVectSpace (X,Y)))) #) 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 (X,Y) is non empty set
the carrier of Y is non empty set
[:X, the carrier of Y:] is non empty Relation-like set
bool [:X, the carrier of Y:] is non empty set
vseq is Element of the carrier of (X,Y)
f is Element of the carrier of (X,Y)
tseq is Element of the carrier of (X,Y)
vseq + f is Element of the carrier of (X,Y)
the addF of (X,Y) is non empty Relation-like [: the carrier of (X,Y), the carrier of (X,Y):] -defined the carrier of (X,Y) -valued Function-like V23([: the carrier of (X,Y), the carrier of (X,Y):]) quasi_total Element of bool [:[: the carrier of (X,Y), the carrier of (X,Y):], the carrier of (X,Y):]
[: the carrier of (X,Y), the carrier of (X,Y):] is non empty Relation-like set
[:[: the carrier of (X,Y), the carrier of (X,Y):], the carrier of (X,Y):] is non empty Relation-like set
bool [:[: the carrier of (X,Y), the carrier of (X,Y):], the carrier of (X,Y):] is non empty set
K584( the carrier of (X,Y), the addF of (X,Y),vseq,f) is Element of the carrier of (X,Y)
[vseq,f] is set
{vseq,f} is set
{vseq} is set
{{vseq,f},{vseq}} is set
the addF of (X,Y) . [vseq,f] is set
m is non empty Relation-like X -defined the carrier of Y -valued Function-like V23(X) quasi_total (X,Y) Element of bool [:X, the carrier of Y:]
n is non empty Relation-like X -defined the carrier of Y -valued Function-like V23(X) quasi_total (X,Y) Element of bool [:X, the carrier of Y:]
n is non empty Relation-like X -defined the carrier of Y -valued Function-like V23(X) quasi_total (X,Y) Element of bool [:X, the carrier of Y:]
tv is Element of the carrier of (RealVectSpace (X,Y))
tseq is Element of the carrier of (RealVectSpace (X,Y))
e is Element of the carrier of (RealVectSpace (X,Y))
tseq + e is Element of the carrier of (RealVectSpace (X,Y))
the addF of (RealVectSpace (X,Y)) is non empty Relation-like [: the carrier of (RealVectSpace (X,Y)), the carrier of (RealVectSpace (X,Y)):] -defined the carrier of (RealVectSpace (X,Y)) -valued Function-like V23([: the carrier of (RealVectSpace (X,Y)), the carrier of (RealVectSpace (X,Y)):]) quasi_total Element of bool [:[: the carrier of (RealVectSpace (X,Y)), the carrier of (RealVectSpace (X,Y)):], the carrier of (RealVectSpace (X,Y)):]
[: the carrier of (RealVectSpace (X,Y)), the carrier of (RealVectSpace (X,Y)):] is non empty Relation-like set
[:[: the carrier of (RealVectSpace (X,Y)), the carrier of (RealVectSpace (X,Y)):], the carrier of (RealVectSpace (X,Y)):] is non empty Relation-like set
bool [:[: the carrier of (RealVectSpace (X,Y)), the carrier of (RealVectSpace (X,Y)):], the carrier of (RealVectSpace (X,Y)):] is non empty set
K584( the carrier of (RealVectSpace (X,Y)), the addF of (RealVectSpace (X,Y)),tseq,e) is Element of the carrier of (RealVectSpace (X,Y))
[tseq,e] is set
{tseq,e} is set
{tseq} is set
{{tseq,e},{tseq}} is set
the addF of (RealVectSpace (X,Y)) . [tseq,e] is set
h1 is Element of X
n . h1 is Element of the carrier of Y
m . h1 is Element of the carrier of Y
n . h1 is Element of the carrier of Y
(m . h1) + (n . h1) is Element of the carrier of Y
the addF of Y is non empty Relation-like [: the carrier of Y, the carrier of Y:] -defined the carrier of Y -valued Function-like V23([: the carrier of Y, the carrier of Y:]) quasi_total Element of bool [:[: the carrier of Y, the carrier of Y:], the carrier of Y:]
[: the carrier of Y, the carrier of Y:] is non empty Relation-like set
[:[: the carrier of Y, the carrier of Y:], the carrier of Y:] is non empty Relation-like set
bool [:[: the carrier of Y, the carrier of Y:], the carrier of Y:] is non empty set
K584( the carrier of Y, the addF of Y,(m . h1),(n . h1)) is Element of the carrier of Y
[(m . h1),(n . h1)] is set
{(m . h1),(n . h1)} is set
{(m . h1)} is set
{{(m . h1),(n . h1)},{(m . h1)}} is set
the addF of Y . [(m . h1),(n . h1)] is set
h1 is Element of X
n . h1 is Element of the carrier of Y
m . h1 is Element of the carrier of Y
n . h1 is Element of the carrier of Y
(m . h1) + (n . h1) is Element of the carrier of Y
K584( the carrier of Y, the addF of Y,(m . h1),(n . h1)) is Element of the carrier of Y
[(m . h1),(n . h1)] is set
{(m . h1),(n . h1)} is set
{(m . h1)} is set
{{(m . h1),(n . h1)},{(m . h1)}} is set
the addF of Y . [(m . h1),(n . h1)] is set
f1 is Element of X
n . f1 is Element of the carrier of Y
m . f1 is Element of the carrier of Y
n . f1 is Element of the carrier of Y
(m . f1) + (n . f1) is Element of the carrier of Y
K584( the carrier of Y, the addF of Y,(m . f1),(n . f1)) is Element of the carrier of Y
[(m . f1),(n . f1)] is set
{(m . f1),(n . f1)} is set
{(m . f1)} is set
{{(m . f1),(n . f1)},{(m . f1)}} is set
the addF of Y . [(m . f1),(n . f1)] is set
X is non empty set
Y is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like NORMSTR
(X,Y) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() RLSStruct
(X,Y) is non empty Element of bool the carrier of (RealVectSpace (X,Y))
RealVectSpace (X,Y) is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() RLSStruct
the carrier of (RealVectSpace (X,Y)) is non empty set
bool the carrier of (RealVectSpace (X,Y)) is non empty set
Zero_ ((X,Y),(RealVectSpace (X,Y))) is Element of (X,Y)
Add_ ((X,Y),(RealVectSpace (X,Y))) is non empty Relation-like [:(X,Y),(X,Y):] -defined (X,Y) -valued Function-like V23([:(X,Y),(X,Y):]) quasi_total Element of bool [:[:(X,Y),(X,Y):],(X,Y):]
[:(X,Y),(X,Y):] is non empty Relation-like set
[:[:(X,Y),(X,Y):],(X,Y):] is non empty Relation-like set
bool [:[:(X,Y),(X,Y):],(X,Y):] is non empty set
Mult_ ((X,Y),(RealVectSpace (X,Y))) is non empty Relation-like [:REAL,(X,Y):] -defined (X,Y) -valued Function-like V23([:REAL,(X,Y):]) quasi_total Element of bool [:[:REAL,(X,Y):],(X,Y):]
[:REAL,(X,Y):] is non empty Relation-like set
[:[:REAL,(X,Y):],(X,Y):] is non empty Relation-like set
bool [:[:REAL,(X,Y):],(X,Y):] is non empty set
RLSStruct(# (X,Y),(Zero_ ((X,Y),(RealVectSpace (X,Y)))),(Add_ ((X,Y),(RealVectSpace (X,Y)))),(Mult_ ((X,Y),(RealVectSpace (X,Y)))) #) 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 (X,Y) is non empty set
the carrier of Y is non empty set
[:X, the carrier of Y:] is non empty Relation-like set
bool [:X, the carrier of Y:] is non empty set
vseq is Element of the carrier of (X,Y)
f is Element of the carrier of (X,Y)
tseq is non empty Relation-like X -defined the carrier of Y -valued Function-like V23(X) quasi_total (X,Y) Element of bool [:X, the carrier of Y:]
tseq is non empty Relation-like X -defined the carrier of Y -valued Function-like V23(X) quasi_total (X,Y) Element of bool [:X, the carrier of Y:]
tv is V11() real ext-real Element of REAL
tv * vseq is Element of the carrier of (X,Y)
the Mult of (X,Y) is non empty Relation-like [:REAL, the carrier of (X,Y):] -defined the carrier of (X,Y) -valued Function-like V23([:REAL, the carrier of (X,Y):]) quasi_total Element of bool [:[:REAL, the carrier of (X,Y):], the carrier of (X,Y):]
[:REAL, the carrier of (X,Y):] is non empty Relation-like set
[:[:REAL, the carrier of (X,Y):], the carrier of (X,Y):] is non empty Relation-like set
bool [:[:REAL, the carrier of (X,Y):], the carrier of (X,Y):] is non empty set
K580( the Mult of (X,Y),tv,vseq) is set
[tv,vseq] is set
{tv,vseq} is set
{tv} is V115() V116() V117() set
{{tv,vseq},{tv}} is set
the Mult of (X,Y) . [tv,vseq] is set
m is Element of the carrier of (RealVectSpace (X,Y))
e is Element of the carrier of (RealVectSpace (X,Y))
tv * e is Element of the carrier of (RealVectSpace (X,Y))
the Mult of (RealVectSpace (X,Y)) is non empty Relation-like [:REAL, the carrier of (RealVectSpace (X,Y)):] -defined the carrier of (RealVectSpace (X,Y)) -valued Function-like V23([:REAL, the carrier of (RealVectSpace (X,Y)):]) quasi_total Element of bool [:[:REAL, the carrier of (RealVectSpace (X,Y)):], the carrier of (RealVectSpace (X,Y)):]
[:REAL, the carrier of (RealVectSpace (X,Y)):] is non empty Relation-like set
[:[:REAL, the carrier of (RealVectSpace (X,Y)):], the carrier of (RealVectSpace (X,Y)):] is non empty Relation-like set
bool [:[:REAL, the carrier of (RealVectSpace (X,Y)):], the carrier of (RealVectSpace (X,Y)):] is non empty set
K580( the Mult of (RealVectSpace (X,Y)),tv,e) is set
[tv,e] is set
{tv,e} is set
{{tv,e},{tv}} is set
the Mult of (RealVectSpace (X,Y)) . [tv,e] is set
n is Element of X
tseq . n is Element of the carrier of Y
tseq . n is Element of the carrier of Y
tv * (tseq . n) is Element of the carrier of Y
the Mult of Y is non empty Relation-like [:REAL, the carrier of Y:] -defined the carrier of Y -valued Function-like V23([:REAL, the carrier of Y:]) quasi_total Element of bool [:[:REAL, the carrier of Y:], the carrier of Y:]
[:REAL, the carrier of Y:] is non empty Relation-like set
[:[:REAL, the carrier of Y:], the carrier of Y:] is non empty Relation-like set
bool [:[:REAL, the carrier of Y:], the carrier of Y:] is non empty set
K580( the Mult of Y,tv,(tseq . n)) is set
[tv,(tseq . n)] is set
{tv,(tseq . n)} is set
{{tv,(tseq . n)},{tv}} is set
the Mult of Y . [tv,(tseq . n)] is set
n is Element of X
tseq . n is Element of the carrier of Y
tseq . n is Element of the carrier of Y
tv * (tseq . n) is Element of the carrier of Y
K580( the Mult of Y,tv,(tseq . n)) is set
[tv,(tseq . n)] is set
{tv,(tseq . n)} is set
{{tv,(tseq . n)},{tv}} is set
the Mult of Y . [tv,(tseq . n)] is set
n is Element of X
tseq . n is Element of the carrier of Y
tseq . n is Element of the carrier of Y
tv * (tseq . n) is Element of the carrier of Y
K580( the Mult of Y,tv,(tseq . n)) is set
[tv,(tseq . n)] is set
{tv,(tseq . n)} is set
{{tv,(tseq . n)},{tv}} is set
the Mult of Y . [tv,(tseq . n)] is set
X is non empty set
Y is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like NORMSTR
(X,Y) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() RLSStruct
(X,Y) is non empty Element of bool the carrier of (RealVectSpace (X,Y))
RealVectSpace (X,Y) is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() RLSStruct
the carrier of (RealVectSpace (X,Y)) is non empty set
bool the carrier of (RealVectSpace (X,Y)) is non empty set
Zero_ ((X,Y),(RealVectSpace (X,Y))) is Element of (X,Y)
Add_ ((X,Y),(RealVectSpace (X,Y))) is non empty Relation-like [:(X,Y),(X,Y):] -defined (X,Y) -valued Function-like V23([:(X,Y),(X,Y):]) quasi_total Element of bool [:[:(X,Y),(X,Y):],(X,Y):]
[:(X,Y),(X,Y):] is non empty Relation-like set
[:[:(X,Y),(X,Y):],(X,Y):] is non empty Relation-like set
bool [:[:(X,Y),(X,Y):],(X,Y):] is non empty set
Mult_ ((X,Y),(RealVectSpace (X,Y))) is non empty Relation-like [:REAL,(X,Y):] -defined (X,Y) -valued Function-like V23([:REAL,(X,Y):]) quasi_total Element of bool [:[:REAL,(X,Y):],(X,Y):]
[:REAL,(X,Y):] is non empty Relation-like set
[:[:REAL,(X,Y):],(X,Y):] is non empty Relation-like set
bool [:[:REAL,(X,Y):],(X,Y):] is non empty set
RLSStruct(# (X,Y),(Zero_ ((X,Y),(RealVectSpace (X,Y)))),(Add_ ((X,Y),(RealVectSpace (X,Y)))),(Mult_ ((X,Y),(RealVectSpace (X,Y)))) #) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() RLSStruct
0. (X,Y) is V49((X,Y)) Element of the carrier of (X,Y)
the carrier of (X,Y) is non empty set
the ZeroF of (X,Y) is Element of the carrier of (X,Y)
the carrier of Y is non empty set
0. Y is V49(Y) Element of the carrier of Y
the ZeroF of Y is Element of the carrier of Y
X --> (0. Y) is non empty Relation-like X -defined the carrier of Y -valued Function-like constant V23(X) quasi_total Element of bool [:X, the carrier of Y:]
[:X, the carrier of Y:] is non empty Relation-like set
bool [:X, the carrier of Y:] is non empty set
0. (RealVectSpace (X,Y)) is V49( RealVectSpace (X,Y)) Element of the carrier of (RealVectSpace (X,Y))
the ZeroF of (RealVectSpace (X,Y)) is Element of the carrier of (RealVectSpace (X,Y))
vseq is set
X is non empty set
Y is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like NORMSTR
(X,Y) is non empty Element of bool the carrier of (RealVectSpace (X,Y))
RealVectSpace (X,Y) is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() RLSStruct
the carrier of (RealVectSpace (X,Y)) is non empty set
bool the carrier of (RealVectSpace (X,Y)) is non empty set
the carrier of Y is non empty set
[:X, the carrier of Y:] is non empty Relation-like set
bool [:X, the carrier of Y:] is non empty set
X is non empty set
Y is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like NORMSTR
the carrier of Y is non empty set
[:X, the carrier of Y:] is non empty Relation-like set
bool [:X, the carrier of Y:] is non empty set
vseq is non empty Relation-like X -defined the carrier of Y -valued Function-like V23(X) quasi_total Element of bool [:X, the carrier of Y:]
{ ||.(vseq . b₁).|| where b₁ is Element of X : verum } is set
the Element of X is Element of X
tseq is set
tseq is Element of X
vseq . tseq is Element of the carrier of Y
||.(vseq . tseq).|| is V11() real ext-real non negative Element of REAL
the normF of Y is non empty Relation-like the carrier of Y -defined REAL -valued Function-like V23( the carrier of Y) quasi_total V105() V106() V107() Element of bool [: the carrier of Y,REAL:]
[: the carrier of Y,REAL:] is non empty Relation-like V105() V106() V107() set
bool [: the carrier of Y,REAL:] is non empty set
the normF of Y . (vseq . tseq) is V11() real ext-real Element of REAL
vseq . the Element of X is Element of the carrier of Y
||.(vseq . the Element of X).|| is V11() real ext-real non negative Element of REAL
the normF of Y is non empty Relation-like the carrier of Y -defined REAL -valued Function-like V23( the carrier of Y) quasi_total V105() V106() V107() Element of bool [: the carrier of Y,REAL:]
[: the carrier of Y,REAL:] is non empty Relation-like V105() V106() V107() set
bool [: the carrier of Y,REAL:] is non empty set
the normF of Y . (vseq . the Element of X) is V11() real ext-real Element of REAL
X is non empty set
Y is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like NORMSTR
the carrier of Y is non empty set
[:X, the carrier of Y:] is non empty Relation-like set
bool [:X, the carrier of Y:] is non empty set
vseq is non empty Relation-like X -defined the carrier of Y -valued Function-like V23(X) quasi_total (X,Y) Element of bool [:X, the carrier of Y:]
(X,Y,vseq) is non empty V115() V116() V117() Element of bool REAL
{ ||.(vseq . b₁).|| where b₁ is Element of X : verum } is set
f is V11() real ext-real Element of REAL
tseq is ext-real set
tseq is Element of X
vseq . tseq is Element of the carrier of Y
||.(vseq . tseq).|| is V11() real ext-real non negative Element of REAL
the normF of Y is non empty Relation-like the carrier of Y -defined REAL -valued Function-like V23( the carrier of Y) quasi_total V105() V106() V107() Element of bool [: the carrier of Y,REAL:]
[: the carrier of Y,REAL:] is non empty Relation-like V105() V106() V107() set
bool [: the carrier of Y,REAL:] is non empty set
the normF of Y . (vseq . tseq) is V11() real ext-real Element of REAL
X is non empty set
Y is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like NORMSTR
the carrier of Y is non empty set
[:X, the carrier of Y:] is non empty Relation-like set
bool [:X, the carrier of Y:] is non empty set
vseq is non empty Relation-like X -defined the carrier of Y -valued Function-like V23(X) quasi_total Element of bool [:X, the carrier of Y:]
(X,Y,vseq) is non empty V115() V116() V117() Element of bool REAL
{ ||.(vseq . b₁).|| where b₁ is Element of X : verum } is set
upper_bound (X,Y,vseq) is V11() real ext-real Element of REAL
f is V11() real ext-real Element of REAL
tseq is set
tv is V11() real ext-real Element of REAL
e is Element of X
vseq . e is Element of the carrier of Y
||.(vseq . e).|| is V11() real ext-real non negative Element of REAL
the normF of Y is non empty Relation-like the carrier of Y -defined REAL -valued Function-like V23( the carrier of Y) quasi_total V105() V106() V107() Element of bool [: the carrier of Y,REAL:]
[: the carrier of Y,REAL:] is non empty Relation-like V105() V106() V107() set
bool [: the carrier of Y,REAL:] is non empty set
the normF of Y . (vseq . e) is V11() real ext-real Element of REAL
tseq is V11() real ext-real Element of REAL
tseq is Element of X
vseq . tseq is Element of the carrier of Y
||.(vseq . tseq).|| is V11() real ext-real non negative Element of REAL
the normF of Y is non empty Relation-like the carrier of Y -defined REAL -valued Function-like V23( the carrier of Y) quasi_total V105() V106() V107() Element of bool [: the carrier of Y,REAL:]
[: the carrier of Y,REAL:] is non empty Relation-like V105() V106() V107() set
bool [: the carrier of Y,REAL:] is non empty set
the normF of Y . (vseq . tseq) is V11() real ext-real Element of REAL
tseq is V11() real ext-real Element of REAL
X is non empty set
Y is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like NORMSTR
(X,Y) is non empty Element of bool the carrier of (RealVectSpace (X,Y))
RealVectSpace (X,Y) is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() RLSStruct
the carrier of (RealVectSpace (X,Y)) is non empty set
bool the carrier of (RealVectSpace (X,Y)) is non empty set
[:(X,Y),REAL:] is non empty Relation-like V105() V106() V107() set
bool [:(X,Y),REAL:] is non empty set
vseq is set
(X,Y,vseq) is non empty Relation-like X -defined the carrier of Y -valued Function-like V23(X) quasi_total (X,Y) Element of bool [:X, the carrier of Y:]
the carrier of Y is non empty set
[:X, the carrier of Y:] is non empty Relation-like set
bool [:X, the carrier of Y:] is non empty set
(X,Y,(X,Y,vseq)) is non empty V115() V116() V117() Element of bool REAL
{ ||.((X,Y,vseq) . b₁).|| where b₁ is Element of X : verum } is set
upper_bound (X,Y,(X,Y,vseq)) is V11() real ext-real Element of REAL
vseq is non empty Relation-like (X,Y) -defined REAL -valued Function-like V23((X,Y)) quasi_total V105() V106() V107() Element of bool [:(X,Y),REAL:]
vseq is non empty Relation-like (X,Y) -defined REAL -valued Function-like V23((X,Y)) quasi_total V105() V106() V107() Element of bool [:(X,Y),REAL:]
f is non empty Relation-like (X,Y) -defined REAL -valued Function-like V23((X,Y)) quasi_total V105() V106() V107() Element of bool [:(X,Y),REAL:]
tseq is set
vseq . tseq is V11() real ext-real Element of REAL
f . tseq is V11() real ext-real Element of REAL
(X,Y,tseq) is non empty Relation-like X -defined the carrier of Y -valued Function-like V23(X) quasi_total (X,Y) Element of bool [:X, the carrier of Y:]
the carrier of Y is non empty set
[:X, the carrier of Y:] is non empty Relation-like set
bool [:X, the carrier of Y:] is non empty set
(X,Y,(X,Y,tseq)) is non empty V115() V116() V117() Element of bool REAL
{ ||.((X,Y,tseq) . b₁).|| where b₁ is Element of X : verum } is set
upper_bound (X,Y,(X,Y,tseq)) is V11() real ext-real Element of REAL
dom vseq is non empty Element of bool (X,Y)
bool (X,Y) is non empty set
dom f is non empty Element of bool (X,Y)
X is non empty set
Y is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like NORMSTR
the carrier of Y is non empty set
[:X, the carrier of Y:] is non empty Relation-like set
bool [:X, the carrier of Y:] is non empty set
vseq is non empty Relation-like X -defined the carrier of Y -valued Function-like V23(X) quasi_total (X,Y) Element of bool [:X, the carrier of Y:]
(X,Y,vseq) is non empty Relation-like X -defined the carrier of Y -valued Function-like V23(X) quasi_total (X,Y) Element of bool [:X, the carrier of Y:]
(X,Y) is non empty Element of bool the carrier of (RealVectSpace (X,Y))
RealVectSpace (X,Y) is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() RLSStruct
the carrier of (RealVectSpace (X,Y)) is non empty set
bool the carrier of (RealVectSpace (X,Y)) is non empty set
X is non empty set
Y is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like NORMSTR
the carrier of Y is non empty set
[:X, the carrier of Y:] is non empty Relation-like set
bool [:X, the carrier of Y:] is non empty set
(X,Y) is non empty Relation-like (X,Y) -defined REAL -valued Function-like V23((X,Y)) quasi_total V105() V106() V107() Element of bool [:(X,Y),REAL:]
(X,Y) is non empty Element of bool the carrier of (RealVectSpace (X,Y))
RealVectSpace (X,Y) is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() RLSStruct
the carrier of (RealVectSpace (X,Y)) is non empty set
bool the carrier of (RealVectSpace (X,Y)) is non empty set
[:(X,Y),REAL:] is non empty Relation-like V105() V106() V107() set
bool [:(X,Y),REAL:] is non empty set
vseq is non empty Relation-like X -defined the carrier of Y -valued Function-like V23(X) quasi_total (X,Y) Element of bool [:X, the carrier of Y:]
(X,Y) . vseq is V11() real ext-real Element of REAL
(X,Y,vseq) is non empty V115() V116() V117() Element of bool REAL
{ ||.(vseq . b₁).|| where b₁ is Element of X : verum } is set
upper_bound (X,Y,vseq) is V11() real ext-real Element of REAL
f is set
(X,Y,f) is non empty Relation-like X -defined the carrier of Y -valued Function-like V23(X) quasi_total (X,Y) Element of bool [:X, the carrier of Y:]
(X,Y,(X,Y,f)) is non empty V115() V116() V117() Element of bool REAL
{ ||.((X,Y,f) . b₁).|| where b₁ is Element of X : verum } is set
upper_bound (X,Y,(X,Y,f)) is V11() real ext-real Element of REAL
X is non empty set
Y is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like NORMSTR
(X,Y) is non empty Element of bool the carrier of (RealVectSpace (X,Y))
RealVectSpace (X,Y) is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() RLSStruct
the carrier of (RealVectSpace (X,Y)) is non empty set
bool the carrier of (RealVectSpace (X,Y)) is non empty set
Zero_ ((X,Y),(RealVectSpace (X,Y))) is Element of (X,Y)
Add_ ((X,Y),(RealVectSpace (X,Y))) is non empty Relation-like [:(X,Y),(X,Y):] -defined (X,Y) -valued Function-like V23([:(X,Y),(X,Y):]) quasi_total Element of bool [:[:(X,Y),(X,Y):],(X,Y):]
[:(X,Y),(X,Y):] is non empty Relation-like set
[:[:(X,Y),(X,Y):],(X,Y):] is non empty Relation-like set
bool [:[:(X,Y),(X,Y):],(X,Y):] is non empty set
Mult_ ((X,Y),(RealVectSpace (X,Y))) is non empty Relation-like [:REAL,(X,Y):] -defined (X,Y) -valued Function-like V23([:REAL,(X,Y):]) quasi_total Element of bool [:[:REAL,(X,Y):],(X,Y):]
[:REAL,(X,Y):] is non empty Relation-like set
[:[:REAL,(X,Y):],(X,Y):] is non empty Relation-like set
bool [:[:REAL,(X,Y):],(X,Y):] is non empty set
(X,Y) is non empty Relation-like (X,Y) -defined REAL -valued Function-like V23((X,Y)) quasi_total V105() V106() V107() Element of bool [:(X,Y),REAL:]
[:(X,Y),REAL:] is non empty Relation-like V105() V106() V107() set
bool [:(X,Y),REAL:] is non empty set
NORMSTR(# (X,Y),(Zero_ ((X,Y),(RealVectSpace (X,Y)))),(Add_ ((X,Y),(RealVectSpace (X,Y)))),(Mult_ ((X,Y),(RealVectSpace (X,Y)))),(X,Y) #) is non empty strict NORMSTR
X is non empty set
Y is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like NORMSTR
the carrier of Y is non empty set
0. Y is V49(Y) Element of the carrier of Y
the ZeroF of Y is Element of the carrier of Y
X --> (0. Y) is non empty Relation-like X -defined the carrier of Y -valued Function-like constant V23(X) quasi_total Element of bool [:X, the carrier of Y:]
[:X, the carrier of Y:] is non empty Relation-like set
bool [:X, the carrier of Y:] is non empty set
(X,Y) is non empty NORMSTR
(X,Y) is non empty Element of bool the carrier of (RealVectSpace (X,Y))
RealVectSpace (X,Y) is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() RLSStruct
the carrier of (RealVectSpace (X,Y)) is non empty set
bool the carrier of (RealVectSpace (X,Y)) is non empty set
Zero_ ((X,Y),(RealVectSpace (X,Y))) is Element of (X,Y)
Add_ ((X,Y),(RealVectSpace (X,Y))) is non empty Relation-like [:(X,Y),(X,Y):] -defined (X,Y) -valued Function-like V23([:(X,Y),(X,Y):]) quasi_total Element of bool [:[:(X,Y),(X,Y):],(X,Y):]
[:(X,Y),(X,Y):] is non empty Relation-like set
[:[:(X,Y),(X,Y):],(X,Y):] is non empty Relation-like set
bool [:[:(X,Y),(X,Y):],(X,Y):] is non empty set
Mult_ ((X,Y),(RealVectSpace (X,Y))) is non empty Relation-like [:REAL,(X,Y):] -defined (X,Y) -valued Function-like V23([:REAL,(X,Y):]) quasi_total Element of bool [:[:REAL,(X,Y):],(X,Y):]
[:REAL,(X,Y):] is non empty Relation-like set
[:[:REAL,(X,Y):],(X,Y):] is non empty Relation-like set
bool [:[:REAL,(X,Y):],(X,Y):] is non empty set
(X,Y) is non empty Relation-like (X,Y) -defined REAL -valued Function-like V23((X,Y)) quasi_total V105() V106() V107() Element of bool [:(X,Y),REAL:]
[:(X,Y),REAL:] is non empty Relation-like V105() V106() V107() set
bool [:(X,Y),REAL:] is non empty set
NORMSTR(# (X,Y),(Zero_ ((X,Y),(RealVectSpace (X,Y)))),(Add_ ((X,Y),(RealVectSpace (X,Y)))),(Mult_ ((X,Y),(RealVectSpace (X,Y)))),(X,Y) #) is non empty strict NORMSTR
0. (X,Y) is V49((X,Y)) Element of the carrier of (X,Y)
the carrier of (X,Y) is non empty set
the ZeroF of (X,Y) is Element of the carrier of (X,Y)
(X,Y) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() RLSStruct
RLSStruct(# (X,Y),(Zero_ ((X,Y),(RealVectSpace (X,Y)))),(Add_ ((X,Y),(RealVectSpace (X,Y)))),(Mult_ ((X,Y),(RealVectSpace (X,Y)))) #) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() RLSStruct
0. (X,Y) is V49((X,Y)) Element of the carrier of (X,Y)
the carrier of (X,Y) is non empty set
the ZeroF of (X,Y) is Element of the carrier of (X,Y)
X is non empty set
Y is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like NORMSTR
(X,Y) is non empty NORMSTR
(X,Y) is non empty Element of bool the carrier of (RealVectSpace (X,Y))
RealVectSpace (X,Y) is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() RLSStruct
the carrier of (RealVectSpace (X,Y)) is non empty set
bool the carrier of (RealVectSpace (X,Y)) is non empty set
Zero_ ((X,Y),(RealVectSpace (X,Y))) is Element of (X,Y)
Add_ ((X,Y),(RealVectSpace (X,Y))) is non empty Relation-like [:(X,Y),(X,Y):] -defined (X,Y) -valued Function-like V23([:(X,Y),(X,Y):]) quasi_total Element of bool [:[:(X,Y),(X,Y):],(X,Y):]
[:(X,Y),(X,Y):] is non empty Relation-like set
[:[:(X,Y),(X,Y):],(X,Y):] is non empty Relation-like set
bool [:[:(X,Y),(X,Y):],(X,Y):] is non empty set
Mult_ ((X,Y),(RealVectSpace (X,Y))) is non empty Relation-like [:REAL,(X,Y):] -defined (X,Y) -valued Function-like V23([:REAL,(X,Y):]) quasi_total Element of bool [:[:REAL,(X,Y):],(X,Y):]
[:REAL,(X,Y):] is non empty Relation-like set
[:[:REAL,(X,Y):],(X,Y):] is non empty Relation-like set
bool [:[:REAL,(X,Y):],(X,Y):] is non empty set
(X,Y) is non empty Relation-like (X,Y) -defined REAL -valued Function-like V23((X,Y)) quasi_total V105() V106() V107() Element of bool [:(X,Y),REAL:]
[:(X,Y),REAL:] is non empty Relation-like V105() V106() V107() set
bool [:(X,Y),REAL:] is non empty set
NORMSTR(# (X,Y),(Zero_ ((X,Y),(RealVectSpace (X,Y)))),(Add_ ((X,Y),(RealVectSpace (X,Y)))),(Mult_ ((X,Y),(RealVectSpace (X,Y)))),(X,Y) #) is non empty strict NORMSTR
the carrier of (X,Y) is non empty set
the carrier of Y is non empty set
[:X, the carrier of Y:] is non empty Relation-like set
bool [:X, the carrier of Y:] is non empty set
vseq is Element of the carrier of (X,Y)
||.vseq.|| is V11() real ext-real Element of REAL
the normF of (X,Y) is non empty Relation-like the carrier of (X,Y) -defined REAL -valued Function-like V23( the carrier of (X,Y)) quasi_total V105() V106() V107() Element of bool [: the carrier of (X,Y),REAL:]
[: the carrier of (X,Y),REAL:] is non empty Relation-like V105() V106() V107() set
bool [: the carrier of (X,Y),REAL:] is non empty set
the normF of (X,Y) . vseq is V11() real ext-real Element of REAL
f is non empty Relation-like X -defined the carrier of Y -valued Function-like V23(X) quasi_total (X,Y) Element of bool [:X, the carrier of Y:]
(X,Y,f) is non empty V115() V116() V117() Element of bool REAL
{ ||.(f . b₁).|| where b₁ is Element of X : verum } is set
tseq is Element of X
f . tseq is Element of the carrier of Y
||.(f . tseq).|| is V11() real ext-real non negative Element of REAL
the normF of Y is non empty Relation-like the carrier of Y -defined REAL -valued Function-like V23( the carrier of Y) quasi_total V105() V106() V107() Element of bool [: the carrier of Y,REAL:]
[: the carrier of Y,REAL:] is non empty Relation-like V105() V106() V107() set
bool [: the carrier of Y,REAL:] is non empty set
the normF of Y . (f . tseq) is V11() real ext-real Element of REAL
upper_bound (X,Y,f) is V11() real ext-real Element of REAL
tseq is Element of X
f . tseq is Element of the carrier of Y
||.(f . tseq).|| is V11() real ext-real non negative Element of REAL
the normF of Y . (f . tseq) is V11() real ext-real Element of REAL
X is non empty set
Y is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like NORMSTR
(X,Y) is non empty NORMSTR
(X,Y) is non empty Element of bool the carrier of (RealVectSpace (X,Y))
RealVectSpace (X,Y) is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() RLSStruct
the carrier of (RealVectSpace (X,Y)) is non empty set
bool the carrier of (RealVectSpace (X,Y)) is non empty set
Zero_ ((X,Y),(RealVectSpace (X,Y))) is Element of (X,Y)
Add_ ((X,Y),(RealVectSpace (X,Y))) is non empty Relation-like [:(X,Y),(X,Y):] -defined (X,Y) -valued Function-like V23([:(X,Y),(X,Y):]) quasi_total Element of bool [:[:(X,Y),(X,Y):],(X,Y):]
[:(X,Y),(X,Y):] is non empty Relation-like set
[:[:(X,Y),(X,Y):],(X,Y):] is non empty Relation-like set
bool [:[:(X,Y),(X,Y):],(X,Y):] is non empty set
Mult_ ((X,Y),(RealVectSpace (X,Y))) is non empty Relation-like [:REAL,(X,Y):] -defined (X,Y) -valued Function-like V23([:REAL,(X,Y):]) quasi_total Element of bool [:[:REAL,(X,Y):],(X,Y):]
[:REAL,(X,Y):] is non empty Relation-like set
[:[:REAL,(X,Y):],(X,Y):] is non empty Relation-like set
bool [:[:REAL,(X,Y):],(X,Y):] is non empty set
(X,Y) is non empty Relation-like (X,Y) -defined REAL -valued Function-like V23((X,Y)) quasi_total V105() V106() V107() Element of bool [:(X,Y),REAL:]
[:(X,Y),REAL:] is non empty Relation-like V105() V106() V107() set
bool [:(X,Y),REAL:] is non empty set
NORMSTR(# (X,Y),(Zero_ ((X,Y),(RealVectSpace (X,Y)))),(Add_ ((X,Y),(RealVectSpace (X,Y)))),(Mult_ ((X,Y),(RealVectSpace (X,Y)))),(X,Y) #) is non empty strict NORMSTR
the carrier of (X,Y) is non empty set
vseq is Element of the carrier of (X,Y)
||.vseq.|| is V11() real ext-real Element of REAL
the normF of (X,Y) is non empty Relation-like the carrier of (X,Y) -defined REAL -valued Function-like V23( the carrier of (X,Y)) quasi_total V105() V106() V107() Element of bool [: the carrier of (X,Y),REAL:]
[: the carrier of (X,Y),REAL:] is non empty Relation-like V105() V106() V107() set
bool [: the carrier of (X,Y),REAL:] is non empty set
the normF of (X,Y) . vseq is V11() real ext-real Element of REAL
the carrier of Y is non empty set
[:X, the carrier of Y:] is non empty Relation-like set
bool [:X, the carrier of Y:] is non empty set
f is non empty Relation-like X -defined the carrier of Y -valued Function-like V23(X) quasi_total (X,Y) Element of bool [:X, the carrier of Y:]
(X,Y,f) is non empty V115() V116() V117() Element of bool REAL
{ ||.(f . b₁).|| where b₁ is Element of X : verum } is set
tseq is set
tv is V11() real ext-real Element of REAL
e is Element of X
f . e is Element of the carrier of Y
||.(f . e).|| is V11() real ext-real non negative Element of REAL
the normF of Y is non empty Relation-like the carrier of Y -defined REAL -valued Function-like V23( the carrier of Y) quasi_total V105() V106() V107() Element of bool [: the carrier of Y,REAL:]
[: the carrier of Y,REAL:] is non empty Relation-like V105() V106() V107() set
bool [: the carrier of Y,REAL:] is non empty set
the normF of Y . (f . e) is V11() real ext-real Element of REAL
tseq is V11() real ext-real Element of REAL
upper_bound (X,Y,f) is V11() real ext-real Element of REAL
X is non empty set
Y is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like NORMSTR
(X,Y) is non empty NORMSTR
(X,Y) is non empty Element of bool the carrier of (RealVectSpace (X,Y))
RealVectSpace (X,Y) is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() RLSStruct
the carrier of (RealVectSpace (X,Y)) is non empty set
bool the carrier of (RealVectSpace (X,Y)) is non empty set
Zero_ ((X,Y),(RealVectSpace (X,Y))) is Element of (X,Y)
Add_ ((X,Y),(RealVectSpace (X,Y))) is non empty Relation-like [:(X,Y),(X,Y):] -defined (X,Y) -valued Function-like V23([:(X,Y),(X,Y):]) quasi_total Element of bool [:[:(X,Y),(X,Y):],(X,Y):]
[:(X,Y),(X,Y):] is non empty Relation-like set
[:[:(X,Y),(X,Y):],(X,Y):] is non empty Relation-like set
bool [:[:(X,Y),(X,Y):],(X,Y):] is non empty set
Mult_ ((X,Y),(RealVectSpace (X,Y))) is non empty Relation-like [:REAL,(X,Y):] -defined (X,Y) -valued Function-like V23([:REAL,(X,Y):]) quasi_total Element of bool [:[:REAL,(X,Y):],(X,Y):]
[:REAL,(X,Y):] is non empty Relation-like set
[:[:REAL,(X,Y):],(X,Y):] is non empty Relation-like set
bool [:[:REAL,(X,Y):],(X,Y):] is non empty set
(X,Y) is non empty Relation-like (X,Y) -defined REAL -valued Function-like V23((X,Y)) quasi_total V105() V106() V107() Element of bool [:(X,Y),REAL:]
[:(X,Y),REAL:] is non empty Relation-like V105() V106() V107() set
bool [:(X,Y),REAL:] is non empty set
NORMSTR(# (X,Y),(Zero_ ((X,Y),(RealVectSpace (X,Y)))),(Add_ ((X,Y),(RealVectSpace (X,Y)))),(Mult_ ((X,Y),(RealVectSpace (X,Y)))),(X,Y) #) is non empty strict NORMSTR
the carrier of (X,Y) is non empty set
0. (X,Y) is V49((X,Y)) Element of the carrier of (X,Y)
the ZeroF of (X,Y) is Element of the carrier of (X,Y)
vseq is Element of the carrier of (X,Y)
||.vseq.|| is V11() real ext-real Element of REAL
the normF of (X,Y) is non empty Relation-like the carrier of (X,Y) -defined REAL -valued Function-like V23( the carrier of (X,Y)) quasi_total V105() V106() V107() Element of bool [: the carrier of (X,Y),REAL:]
[: the carrier of (X,Y),REAL:] is non empty Relation-like V105() V106() V107() set
bool [: the carrier of (X,Y),REAL:] is non empty set
the normF of (X,Y) . vseq is V11() real ext-real Element of REAL
the carrier of Y is non empty set
[:X, the carrier of Y:] is non empty Relation-like set
bool [:X, the carrier of Y:] is non empty set
0. Y is V49(Y) Element of the carrier of Y
the ZeroF of Y is Element of the carrier of Y
X --> (0. Y) is non empty Relation-like X -defined the carrier of Y -valued Function-like constant V23(X) quasi_total Element of bool [:X, the carrier of Y:]
f is non empty Relation-like X -defined the carrier of Y -valued Function-like V23(X) quasi_total (X,Y) Element of bool [:X, the carrier of Y:]
(X,Y,f) is non empty V115() V116() V117() Element of bool REAL
{ ||.(f . b₁).|| where b₁ is Element of X : verum } is set
tv is set
upper_bound (X,Y,f) is V11() real ext-real Element of REAL
tseq is non empty Relation-like X -defined the carrier of Y -valued Function-like V23(X) quasi_total Element of bool [:X, the carrier of Y:]
m is V11() real ext-real Element of REAL
n is Element of X
f . n is Element of the carrier of Y
||.(f . n).|| is V11() real ext-real non negative Element of REAL
the normF of Y is non empty Relation-like the carrier of Y -defined REAL -valued Function-like V23( the carrier of Y) quasi_total V105() V106() V107() Element of bool [: the carrier of Y,REAL:]
[: the carrier of Y,REAL:] is non empty Relation-like V105() V106() V107() set
bool [: the carrier of Y,REAL:] is non empty set
the normF of Y . (f . n) is V11() real ext-real Element of REAL
||.(0. Y).|| 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() Element of REAL
the normF of Y . (0. Y) is V11() real ext-real Element of REAL
e is V11() real ext-real Element of REAL
m is V11() real ext-real set
X is non empty set
Y is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like NORMSTR
(X,Y) is non empty NORMSTR
(X,Y) is non empty Element of bool the carrier of (RealVectSpace (X,Y))
RealVectSpace (X,Y) is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() RLSStruct
the carrier of (RealVectSpace (X,Y)) is non empty set
bool the carrier of (RealVectSpace (X,Y)) is non empty set
Zero_ ((X,Y),(RealVectSpace (X,Y))) is Element of (X,Y)
Add_ ((X,Y),(RealVectSpace (X,Y))) is non empty Relation-like [:(X,Y),(X,Y):] -defined (X,Y) -valued Function-like V23([:(X,Y),(X,Y):]) quasi_total Element of bool [:[:(X,Y),(X,Y):],(X,Y):]
[:(X,Y),(X,Y):] is non empty Relation-like set
[:[:(X,Y),(X,Y):],(X,Y):] is non empty Relation-like set
bool [:[:(X,Y),(X,Y):],(X,Y):] is non empty set
Mult_ ((X,Y),(RealVectSpace (X,Y))) is non empty Relation-like [:REAL,(X,Y):] -defined (X,Y) -valued Function-like V23([:REAL,(X,Y):]) quasi_total Element of bool [:[:REAL,(X,Y):],(X,Y):]
[:REAL,(X,Y):] is non empty Relation-like set
[:[:REAL,(X,Y):],(X,Y):] is non empty Relation-like set
bool [:[:REAL,(X,Y):],(X,Y):] is non empty set
(X,Y) is non empty Relation-like (X,Y) -defined REAL -valued Function-like V23((X,Y)) quasi_total V105() V106() V107() Element of bool [:(X,Y),REAL:]
[:(X,Y),REAL:] is non empty Relation-like V105() V106() V107() set
bool [:(X,Y),REAL:] is non empty set
NORMSTR(# (X,Y),(Zero_ ((X,Y),(RealVectSpace (X,Y)))),(Add_ ((X,Y),(RealVectSpace (X,Y)))),(Mult_ ((X,Y),(RealVectSpace (X,Y)))),(X,Y) #) is non empty strict NORMSTR
the carrier of (X,Y) is non empty set
the carrier of Y is non empty set
[:X, the carrier of Y:] is non empty Relation-like set
bool [:X, the carrier of Y:] is non empty set
vseq is Element of the carrier of (X,Y)
f is Element of the carrier of (X,Y)
tseq is Element of the carrier of (X,Y)
vseq + f is Element of the carrier of (X,Y)
the addF of (X,Y) is non empty Relation-like [: the carrier of (X,Y), the carrier of (X,Y):] -defined the carrier of (X,Y) -valued Function-like V23([: the carrier of (X,Y), the carrier of (X,Y):]) quasi_total Element of bool [:[: the carrier of (X,Y), the carrier of (X,Y):], the carrier of (X,Y):]
[: the carrier of (X,Y), the carrier of (X,Y):] is non empty Relation-like set
[:[: the carrier of (X,Y), the carrier of (X,Y):], the carrier of (X,Y):] is non empty Relation-like set
bool [:[: the carrier of (X,Y), the carrier of (X,Y):], the carrier of (X,Y):] is non empty set
K584( the carrier of (X,Y), the addF of (X,Y),vseq,f) is Element of the carrier of (X,Y)
[vseq,f] is set
{vseq,f} is set
{vseq} is set
{{vseq,f},{vseq}} is set
the addF of (X,Y) . [vseq,f] is set
(X,Y) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() RLSStruct
RLSStruct(# (X,Y),(Zero_ ((X,Y),(RealVectSpace (X,Y)))),(Add_ ((X,Y),(RealVectSpace (X,Y)))),(Mult_ ((X,Y),(RealVectSpace (X,Y)))) #) 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 (X,Y) is non empty set
e is Element of the carrier of (X,Y)
tseq is Element of the carrier of (X,Y)
tv is Element of the carrier of (X,Y)
tseq + tv is Element of the carrier of (X,Y)
the addF of (X,Y) is non empty Relation-like [: the carrier of (X,Y), the carrier of (X,Y):] -defined the carrier of (X,Y) -valued Function-like V23([: the carrier of (X,Y), the carrier of (X,Y):]) quasi_total Element of bool [:[: the carrier of (X,Y), the carrier of (X,Y):], the carrier of (X,Y):]
[: the carrier of (X,Y), the carrier of (X,Y):] is non empty Relation-like set
[:[: the carrier of (X,Y), the carrier of (X,Y):], the carrier of (X,Y):] is non empty Relation-like set
bool [:[: the carrier of (X,Y), the carrier of (X,Y):], the carrier of (X,Y):] is non empty set
K584( the carrier of (X,Y), the addF of (X,Y),tseq,tv) is Element of the carrier of (X,Y)
[tseq,tv] is set
{tseq,tv} is set
{tseq} is set
{{tseq,tv},{tseq}} is set
the addF of (X,Y) . [tseq,tv] is set
m is non empty Relation-like X -defined the carrier of Y -valued Function-like V23(X) quasi_total (X,Y) Element of bool [:X, the carrier of Y:]
n is non empty Relation-like X -defined the carrier of Y -valued Function-like V23(X) quasi_total (X,Y) Element of bool [:X, the carrier of Y:]
n is non empty Relation-like X -defined the carrier of Y -valued Function-like V23(X) quasi_total (X,Y) Element of bool [:X, the carrier of Y:]
h1 is Element of X
n . h1 is Element of the carrier of Y
m . h1 is Element of the carrier of Y
n . h1 is Element of the carrier of Y
(m . h1) + (n . h1) is Element of the carrier of Y
the addF of Y is non empty Relation-like [: the carrier of Y, the carrier of Y:] -defined the carrier of Y -valued Function-like V23([: the carrier of Y, the carrier of Y:]) quasi_total Element of bool [:[: the carrier of Y, the carrier of Y:], the carrier of Y:]
[: the carrier of Y, the carrier of Y:] is non empty Relation-like set
[:[: the carrier of Y, the carrier of Y:], the carrier of Y:] is non empty Relation-like set
bool [:[: the carrier of Y, the carrier of Y:], the carrier of Y:] is non empty set
K584( the carrier of Y, the addF of Y,(m . h1),(n . h1)) is Element of the carrier of Y
[(m . h1),(n . h1)] is set
{(m . h1),(n . h1)} is set
{(m . h1)} is set
{{(m . h1),(n . h1)},{(m . h1)}} is set
the addF of Y . [(m . h1),(n . h1)] is set
X is non empty set
Y is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like NORMSTR
(X,Y) is non empty NORMSTR
(X,Y) is non empty Element of bool the carrier of (RealVectSpace (X,Y))
RealVectSpace (X,Y) is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() RLSStruct
the carrier of (RealVectSpace (X,Y)) is non empty set
bool the carrier of (RealVectSpace (X,Y)) is non empty set
Zero_ ((X,Y),(RealVectSpace (X,Y))) is Element of (X,Y)
Add_ ((X,Y),(RealVectSpace (X,Y))) is non empty Relation-like [:(X,Y),(X,Y):] -defined (X,Y) -valued Function-like V23([:(X,Y),(X,Y):]) quasi_total Element of bool [:[:(X,Y),(X,Y):],(X,Y):]
[:(X,Y),(X,Y):] is non empty Relation-like set
[:[:(X,Y),(X,Y):],(X,Y):] is non empty Relation-like set
bool [:[:(X,Y),(X,Y):],(X,Y):] is non empty set
Mult_ ((X,Y),(RealVectSpace (X,Y))) is non empty Relation-like [:REAL,(X,Y):] -defined (X,Y) -valued Function-like V23([:REAL,(X,Y):]) quasi_total Element of bool [:[:REAL,(X,Y):],(X,Y):]
[:REAL,(X,Y):] is non empty Relation-like set
[:[:REAL,(X,Y):],(X,Y):] is non empty Relation-like set
bool [:[:REAL,(X,Y):],(X,Y):] is non empty set
(X,Y) is non empty Relation-like (X,Y) -defined REAL -valued Function-like V23((X,Y)) quasi_total V105() V106() V107() Element of bool [:(X,Y),REAL:]
[:(X,Y),REAL:] is non empty Relation-like V105() V106() V107() set
bool [:(X,Y),REAL:] is non empty set
NORMSTR(# (X,Y),(Zero_ ((X,Y),(RealVectSpace (X,Y)))),(Add_ ((X,Y),(RealVectSpace (X,Y)))),(Mult_ ((X,Y),(RealVectSpace (X,Y)))),(X,Y) #) is non empty strict NORMSTR
the carrier of (X,Y) is non empty set
the carrier of Y is non empty set
[:X, the carrier of Y:] is non empty Relation-like set
bool [:X, the carrier of Y:] is non empty set
vseq is Element of the carrier of (X,Y)
f is Element of the carrier of (X,Y)
tseq is non empty Relation-like X -defined the carrier of Y -valued Function-like V23(X) quasi_total (X,Y) Element of bool [:X, the carrier of Y:]
tseq is non empty Relation-like X -defined the carrier of Y -valued Function-like V23(X) quasi_total (X,Y) Element of bool [:X, the carrier of Y:]
(X,Y) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() RLSStruct
RLSStruct(# (X,Y),(Zero_ ((X,Y),(RealVectSpace (X,Y)))),(Add_ ((X,Y),(RealVectSpace (X,Y)))),(Mult_ ((X,Y),(RealVectSpace (X,Y)))) #) 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 (X,Y) is non empty set
m is V11() real ext-real Element of REAL
m * vseq is Element of the carrier of (X,Y)
the Mult of (X,Y) is non empty Relation-like [:REAL, the carrier of (X,Y):] -defined the carrier of (X,Y) -valued Function-like V23([:REAL, the carrier of (X,Y):]) quasi_total Element of bool [:[:REAL, the carrier of (X,Y):], the carrier of (X,Y):]
[:REAL, the carrier of (X,Y):] is non empty Relation-like set
[:[:REAL, the carrier of (X,Y):], the carrier of (X,Y):] is non empty Relation-like set
bool [:[:REAL, the carrier of (X,Y):], the carrier of (X,Y):] is non empty set
K580( the Mult of (X,Y),m,vseq) is set
[m,vseq] is set
{m,vseq} is set
{m} is V115() V116() V117() set
{{m,vseq},{m}} is set
the Mult of (X,Y) . [m,vseq] is set
tv is Element of the carrier of (X,Y)
e is Element of the carrier of (X,Y)
m * e is Element of the carrier of (X,Y)
the Mult of (X,Y) is non empty Relation-like [:REAL, the carrier of (X,Y):] -defined the carrier of (X,Y) -valued Function-like V23([:REAL, the carrier of (X,Y):]) quasi_total Element of bool [:[:REAL, the carrier of (X,Y):], the carrier of (X,Y):]
[:REAL, the carrier of (X,Y):] is non empty Relation-like set
[:[:REAL, the carrier of (X,Y):], the carrier of (X,Y):] is non empty Relation-like set
bool [:[:REAL, the carrier of (X,Y):], the carrier of (X,Y):] is non empty set
K580( the Mult of (X,Y),m,e) is set
[m,e] is set
{m,e} is set
{{m,e},{m}} is set
the Mult of (X,Y) . [m,e] is set
n is Element of X
tseq . n is Element of the carrier of Y
tseq . n is Element of the carrier of Y
m * (tseq . n) is Element of the carrier of Y
the Mult of Y is non empty Relation-like [:REAL, the carrier of Y:] -defined the carrier of Y -valued Function-like V23([:REAL, the carrier of Y:]) quasi_total Element of bool [:[:REAL, the carrier of Y:], the carrier of Y:]
[:REAL, the carrier of Y:] is non empty Relation-like set
[:[:REAL, the carrier of Y:], the carrier of Y:] is non empty Relation-like set
bool [:[:REAL, the carrier of Y:], the carrier of Y:] is non empty set
K580( the Mult of Y,m,(tseq . n)) is set
[m,(tseq . n)] is set
{m,(tseq . n)} is set
{{m,(tseq . n)},{m}} is set
the Mult of Y . [m,(tseq . n)] is set
X is non empty set
Y is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like NORMSTR
(X,Y) is non empty NORMSTR
(X,Y) is non empty Element of bool the carrier of (RealVectSpace (X,Y))
RealVectSpace (X,Y) is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() RLSStruct
the carrier of (RealVectSpace (X,Y)) is non empty set
bool the carrier of (RealVectSpace (X,Y)) is non empty set
Zero_ ((X,Y),(RealVectSpace (X,Y))) is Element of (X,Y)
Add_ ((X,Y),(RealVectSpace (X,Y))) is non empty Relation-like [:(X,Y),(X,Y):] -defined (X,Y) -valued Function-like V23([:(X,Y),(X,Y):]) quasi_total Element of bool [:[:(X,Y),(X,Y):],(X,Y):]
[:(X,Y),(X,Y):] is non empty Relation-like set
[:[:(X,Y),(X,Y):],(X,Y):] is non empty Relation-like set
bool [:[:(X,Y),(X,Y):],(X,Y):] is non empty set
Mult_ ((X,Y),(RealVectSpace (X,Y))) is non empty Relation-like [:REAL,(X,Y):] -defined (X,Y) -valued Function-like V23([:REAL,(X,Y):]) quasi_total Element of bool [:[:REAL,(X,Y):],(X,Y):]
[:REAL,(X,Y):] is non empty Relation-like set
[:[:REAL,(X,Y):],(X,Y):] is non empty Relation-like set
bool [:[:REAL,(X,Y):],(X,Y):] is non empty set
(X,Y) is non empty Relation-like (X,Y) -defined REAL -valued Function-like V23((X,Y)) quasi_total V105() V106() V107() Element of bool [:(X,Y),REAL:]
[:(X,Y),REAL:] is non empty Relation-like V105() V106() V107() set
bool [:(X,Y),REAL:] is non empty set
NORMSTR(# (X,Y),(Zero_ ((X,Y),(RealVectSpace (X,Y)))),(Add_ ((X,Y),(RealVectSpace (X,Y)))),(Mult_ ((X,Y),(RealVectSpace (X,Y)))),(X,Y) #) is non empty strict NORMSTR
the carrier of (X,Y) is non empty set
0. (X,Y) is V49((X,Y)) Element of the carrier of (X,Y)
the ZeroF of (X,Y) is Element of the carrier of (X,Y)
vseq is Element of the carrier of (X,Y)
||.vseq.|| is V11() real ext-real Element of REAL
the normF of (X,Y) is non empty Relation-like the carrier of (X,Y) -defined REAL -valued Function-like V23( the carrier of (X,Y)) quasi_total V105() V106() V107() Element of bool [: the carrier of (X,Y),REAL:]
[: the carrier of (X,Y),REAL:] is non empty Relation-like V105() V106() V107() set
bool [: the carrier of (X,Y),REAL:] is non empty set
the normF of (X,Y) . vseq is V11() real ext-real Element of REAL
f is Element of the carrier of (X,Y)
vseq + f is Element of the carrier of (X,Y)
the addF of (X,Y) is non empty Relation-like [: the carrier of (X,Y), the carrier of (X,Y):] -defined the carrier of (X,Y) -valued Function-like V23([: the carrier of (X,Y), the carrier of (X,Y):]) quasi_total Element of bool [:[: the carrier of (X,Y), the carrier of (X,Y):], the carrier of (X,Y):]
[: the carrier of (X,Y), the carrier of (X,Y):] is non empty Relation-like set
[:[: the carrier of (X,Y), the carrier of (X,Y):], the carrier of (X,Y):] is non empty Relation-like set
bool [:[: the carrier of (X,Y), the carrier of (X,Y):], the carrier of (X,Y):] is non empty set
K584( the carrier of (X,Y), the addF of (X,Y),vseq,f) is Element of the carrier of (X,Y)
[vseq,f] is set
{vseq,f} is set
{vseq} is set
{{vseq,f},{vseq}} is set
the addF of (X,Y) . [vseq,f] is set
||.(vseq + f).|| is V11() real ext-real Element of REAL
the normF of (X,Y) . (vseq + f) is V11() real ext-real Element of REAL
||.f.|| is V11() real ext-real Element of REAL
the normF of (X,Y) . f is V11() real ext-real Element of REAL
||.vseq.|| + ||.f.|| is V11() real ext-real Element of REAL
tseq is V11() real ext-real Element of REAL
tseq * vseq is Element of the carrier of (X,Y)
the Mult of (X,Y) is non empty Relation-like [:REAL, the carrier of (X,Y):] -defined the carrier of (X,Y) -valued Function-like V23([:REAL, the carrier of (X,Y):]) quasi_total Element of bool [:[:REAL, the carrier of (X,Y):], the carrier of (X,Y):]
[:REAL, the carrier of (X,Y):] is non empty Relation-like set
[:[:REAL, the carrier of (X,Y):], the carrier of (X,Y):] is non empty Relation-like set
bool [:[:REAL, the carrier of (X,Y):], the carrier of (X,Y):] is non empty set
K580( the Mult of (X,Y),tseq,vseq) is set
[tseq,vseq] is set
{tseq,vseq} is set
{tseq} is V115() V116() V117() set
{{tseq,vseq},{tseq}} is set
the Mult of (X,Y) . [tseq,vseq] is set
||.(tseq * vseq).|| is V11() real ext-real Element of REAL
the normF of (X,Y) . (tseq * vseq) is V11() real ext-real Element of REAL
abs tseq is V11() real ext-real Element of REAL
(abs tseq) * ||.vseq.|| is V11() real ext-real Element of REAL
the carrier of Y is non empty set
[:X, the carrier of Y:] is non empty Relation-like set
bool [:X, the carrier of Y:] is non empty set
0. Y is V49(Y) Element of the carrier of Y
the ZeroF of Y is Element of the carrier of Y
X --> (0. Y) is non empty Relation-like X -defined the carrier of Y -valued Function-like constant V23(X) quasi_total Element of bool [:X, the carrier of Y:]
tseq is non empty Relation-like X -defined the carrier of Y -valued Function-like V23(X) quasi_total (X,Y) Element of bool [:X, the carrier of Y:]
(X,Y,tseq) is non empty V115() V116() V117() Element of bool REAL
{ ||.(tseq . b₁).|| where b₁ is Element of X : verum } is set
m is set
upper_bound (X,Y,tseq) is V11() real ext-real Element of REAL
e is non empty Relation-like X -defined the carrier of Y -valued Function-like V23(X) quasi_total Element of bool [:X, the carrier of Y:]
n is V11() real ext-real Element of REAL
h1 is Element of X
tseq . h1 is Element of the carrier of Y
||.(tseq . h1).|| is V11() real ext-real non negative Element of REAL
the normF of Y is non empty Relation-like the carrier of Y -defined REAL -valued Function-like V23( the carrier of Y) quasi_total V105() V106() V107() Element of bool [: the carrier of Y,REAL:]
[: the carrier of Y,REAL:] is non empty Relation-like V105() V106() V107() set
bool [: the carrier of Y,REAL:] is non empty set
the normF of Y . (tseq . h1) is V11() real ext-real Element of REAL
||.(0. Y).|| 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() Element of REAL
the normF of Y . (0. Y) is V11() real ext-real Element of REAL
n is V11() real ext-real Element of REAL
n is V11() real ext-real set
the carrier of Y is non empty set
[:X, the carrier of Y:] is non empty Relation-like set
bool [:X, the carrier of Y:] is non empty set
tseq is non empty Relation-like X -defined the carrier of Y -valued Function-like V23(X) quasi_total (X,Y) Element of bool [:X, the carrier of Y:]
m is Element of X
tseq . m is Element of the carrier of Y
||.(tseq . m).|| is V11() real ext-real non negative Element of REAL
the normF of Y is non empty Relation-like the carrier of Y -defined REAL -valued Function-like V23( the carrier of Y) quasi_total V105() V106() V107() Element of bool [: the carrier of Y,REAL:]
[: the carrier of Y,REAL:] is non empty Relation-like V105() V106() V107() set
bool [: the carrier of Y,REAL:] is non empty set
the normF of Y . (tseq . m) is V11() real ext-real Element of REAL
tv is non empty Relation-like X -defined the carrier of Y -valued Function-like V23(X) quasi_total (X,Y) Element of bool [:X, the carrier of Y:]
tv . m is Element of the carrier of Y
||.(tv . m).|| is V11() real ext-real non negative Element of REAL
the normF of Y . (tv . m) is V11() real ext-real Element of REAL
||.(tseq . m).|| + ||.(tv . m).|| is V11() real ext-real non negative Element of REAL
e is non empty Relation-like X -defined the carrier of Y -valued Function-like V23(X) quasi_total (X,Y) Element of bool [:X, the carrier of Y:]
e . m is Element of the carrier of Y
||.(e . m).|| is V11() real ext-real non negative Element of REAL
the normF of Y . (e . m) is V11() real ext-real Element of REAL
(tseq . m) + (tv . m) is Element of the carrier of Y
the addF of Y is non empty Relation-like [: the carrier of Y, the carrier of Y:] -defined the carrier of Y -valued Function-like V23([: the carrier of Y, the carrier of Y:]) quasi_total Element of bool [:[: the carrier of Y, the carrier of Y:], the carrier of Y:]
[: the carrier of Y, the carrier of Y:] is non empty Relation-like set
[:[: the carrier of Y, the carrier of Y:], the carrier of Y:] is non empty Relation-like set
bool [:[: the carrier of Y, the carrier of Y:], the carrier of Y:] is non empty set
K584( the carrier of Y, the addF of Y,(tseq . m),(tv . m)) is Element of the carrier of Y
[(tseq . m),(tv . m)] is set
{(tseq . m),(tv . m)} is set
{(tseq . m)} is set
{{(tseq . m),(tv . m)},{(tseq . m)}} is set
the addF of Y . [(tseq . m),(tv . m)] is set
||.((tseq . m) + (tv . m)).|| is V11() real ext-real non negative Element of REAL
the normF of Y . ((tseq . m) + (tv . m)) is V11() real ext-real Element of REAL
m is V11() real ext-real Element of REAL
(X,Y,e) is non empty V115() V116() V117() Element of bool REAL
{ ||.(e . b₁).|| where b₁ is Element of X : verum } is set
n is Element of X
e . n is Element of the carrier of Y
||.(e . n).|| is V11() real ext-real non negative Element of REAL
the normF of Y . (e . n) is V11() real ext-real Element of REAL
upper_bound (X,Y,e) is V11() real ext-real Element of REAL
m is V11() real ext-real set
the carrier of Y is non empty set
[:X, the carrier of Y:] is non empty Relation-like set
bool [:X, the carrier of Y:] is non empty set
tv is non empty Relation-like X -defined the carrier of Y -valued Function-like V23(X) quasi_total (X,Y) Element of bool [:X, the carrier of Y:]
(X,Y,tv) is non empty V115() V116() V117() Element of bool REAL
{ ||.(tv . b₁).|| where b₁ is Element of X : verum } is set
upper_bound (X,Y,tv) is V11() real ext-real Element of REAL
e is Element of X
tv . e is Element of the carrier of Y
||.(tv . e).|| is V11() real ext-real non negative Element of REAL
the normF of Y is non empty Relation-like the carrier of Y -defined REAL -valued Function-like V23( the carrier of Y) quasi_total V105() V106() V107() Element of bool [: the carrier of Y,REAL:]
[: the carrier of Y,REAL:] is non empty Relation-like V105() V106() V107() set
bool [: the carrier of Y,REAL:] is non empty set
the normF of Y . (tv . e) is V11() real ext-real Element of REAL
tseq is non empty Relation-like X -defined the carrier of Y -valued Function-like V23(X) quasi_total (X,Y) Element of bool [:X, the carrier of Y:]
tseq . e is Element of the carrier of Y
tseq * (tseq . e) is Element of the carrier of Y
the Mult of Y is non empty Relation-like [:REAL, the carrier of Y:] -defined the carrier of Y -valued Function-like V23([:REAL, the carrier of Y:]) quasi_total Element of bool [:[:REAL, the carrier of Y:], the carrier of Y:]
[:REAL, the carrier of Y:] is non empty Relation-like set
[:[:REAL, the carrier of Y:], the carrier of Y:] is non empty Relation-like set
bool [:[:REAL, the carrier of Y:], the carrier of Y:] is non empty set
K580( the Mult of Y,tseq,(tseq . e)) is set
[tseq,(tseq . e)] is set
{tseq,(tseq . e)} is set
{{tseq,(tseq . e)},{tseq}} is set
the Mult of Y . [tseq,(tseq . e)] is set
||.(tseq * (tseq . e)).|| is V11() real ext-real non negative Element of REAL
the normF of Y . (tseq * (tseq . e)) is V11() real ext-real Element of REAL
||.(tseq . e).|| is V11() real ext-real non negative Element of REAL
the normF of Y . (tseq . e) is V11() real ext-real Element of REAL
(abs tseq) * ||.(tseq . e).|| is V11() real ext-real Element of REAL
e is V11() real ext-real Element of REAL
m is Element of X
tv . m is Element of the carrier of Y
||.(tv . m).|| is V11() real ext-real non negative Element of REAL
the normF of Y . (tv . m) is V11() real ext-real Element of REAL
tseq " is V11() real ext-real Element of REAL
abs (tseq ") is V11() real ext-real Element of REAL
1 * (tseq ") is V11() real ext-real Element of REAL
abs (1 * (tseq ")) is V11() real ext-real Element of REAL
1 / tseq is V11() real ext-real Element of REAL
abs (1 / tseq) is V11() real ext-real Element of REAL
1 / (abs tseq) is V11() real ext-real Element of REAL
(abs tseq) " is V11() real ext-real Element of REAL
1 * ((abs tseq) ") is V11() real ext-real Element of REAL
e is Element of X
tv . e is Element of the carrier of Y
tseq . e is Element of the carrier of Y
tseq * (tseq . e) is Element of the carrier of Y
K580( the Mult of Y,tseq,(tseq . e)) is set
[tseq,(tseq . e)] is set
{tseq,(tseq . e)} is set
{{tseq,(tseq . e)},{tseq}} is set
the Mult of Y . [tseq,(tseq . e)] is set
(tseq ") * (tv . e) is Element of the carrier of Y
K580( the Mult of Y,(tseq "),(tv . e)) is set
[(tseq "),(tv . e)] is set
{(tseq "),(tv . e)} is set
{(tseq ")} is V115() V116() V117() set
{{(tseq "),(tv . e)},{(tseq ")}} is set
the Mult of Y . [(tseq "),(tv . e)] is set
(tseq ") * tseq is V11() real ext-real Element of REAL
((tseq ") * tseq) * (tseq . e) is Element of the carrier of Y
K580( the Mult of Y,((tseq ") * tseq),(tseq . e)) is set
[((tseq ") * tseq),(tseq . e)] is set
{((tseq ") * tseq),(tseq . e)} is set
{((tseq ") * tseq)} is V115() V116() V117() set
{{((tseq ") * tseq),(tseq . e)},{((tseq ") * tseq)}} is set
the Mult of Y . [((tseq ") * tseq),(tseq . e)] is set
1 * (tseq . e) is Element of the carrier of Y
K580( the Mult of Y,1,(tseq . e)) is set
[1,(tseq . e)] is set
{1,(tseq . e)} is set
{1} is V115() V116() V117() V118() V119() V120() set
{{1,(tseq . e)},{1}} is set
the Mult of Y . [1,(tseq . e)] is set
||.((tseq ") * (tv . e)).|| is V11() real ext-real non negative Element of REAL
the normF of Y . ((tseq ") * (tv . e)) is V11() real ext-real Element of REAL
||.(tv . e).|| is V11() real ext-real non negative Element of REAL
the normF of Y . (tv . e) is V11() real ext-real Element of REAL
(abs (tseq ")) * ||.(tv . e).|| is V11() real ext-real Element of REAL
||.(tseq . e).|| is V11() real ext-real non negative Element of REAL
the normF of Y . (tseq . e) is V11() real ext-real Element of REAL
((abs tseq) ") * ||.(tseq * vseq).|| is V11() real ext-real Element of REAL
e is V11() real ext-real Element of REAL
(X,Y,tseq) is non empty V115() V116() V117() Element of bool REAL
{ ||.(tseq . b₁).|| where b₁ is Element of X : verum } is set
m is Element of X
tseq . m is Element of the carrier of Y
||.(tseq . m).|| is V11() real ext-real non negative Element of REAL
the normF of Y . (tseq . m) is V11() real ext-real Element of REAL
upper_bound (X,Y,tseq) is V11() real ext-real Element of REAL
(X,Y) . vseq is V11() real ext-real Element of REAL
(abs tseq) * (((abs tseq) ") * ||.(tseq * vseq).||) is V11() real ext-real Element of REAL
e is V11() real ext-real set
(abs tseq) * ((abs tseq) ") is V11() real ext-real Element of REAL
((abs tseq) * ((abs tseq) ")) * ||.(tseq * vseq).|| is V11() real ext-real Element of REAL
1 * ||.(tseq * vseq).|| is V11() real ext-real Element of REAL
(X,Y) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() RLSStruct
RLSStruct(# (X,Y),(Zero_ ((X,Y),(RealVectSpace (X,Y)))),(Add_ ((X,Y),(RealVectSpace (X,Y)))),(Mult_ ((X,Y),(RealVectSpace (X,Y)))) #) 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 (X,Y) is non empty set
e is Element of the carrier of (X,Y)
tseq * e is Element of the carrier of (X,Y)
the Mult of (X,Y) is non empty Relation-like [:REAL, the carrier of (X,Y):] -defined the carrier of (X,Y) -valued Function-like V23([:REAL, the carrier of (X,Y):]) quasi_total Element of bool [:[:REAL, the carrier of (X,Y):], the carrier of (X,Y):]
[:REAL, the carrier of (X,Y):] is non empty Relation-like set
[:[:REAL, the carrier of (X,Y):], the carrier of (X,Y):] is non empty Relation-like set
bool [:[:REAL, the carrier of (X,Y):], the carrier of (X,Y):] is non empty set
K580( the Mult of (X,Y),tseq,e) is set
[tseq,e] is set
{tseq,e} is set
{{tseq,e},{tseq}} is set
the Mult of (X,Y) . [tseq,e] is set
0. (X,Y) is V49((X,Y)) Element of the carrier of (X,Y)
the ZeroF of (X,Y) is Element of the carrier of (X,Y)
0 * ||.vseq.|| is V11() real ext-real Element of REAL
(X,Y) . (tseq * vseq) is V11() real ext-real Element of REAL
e is V11() real ext-real set
the carrier of Y is non empty set
[:X, the carrier of Y:] is non empty Relation-like set
bool [:X, the carrier of Y:] is non empty set
0. Y is V49(Y) Element of the carrier of Y
the ZeroF of Y is Element of the carrier of Y
X --> (0. Y) is non empty Relation-like X -defined the carrier of Y -valued Function-like constant V23(X) quasi_total Element of bool [:X, the carrier of Y:]
tseq is non empty Relation-like X -defined the carrier of Y -valued Function-like V23(X) quasi_total (X,Y) Element of bool [:X, the carrier of Y:]
m is Element of X
tseq . m is Element of the carrier of Y
||.(tseq . m).|| is V11() real ext-real non negative Element of REAL
the normF of Y is non empty Relation-like the carrier of Y -defined REAL -valued Function-like V23( the carrier of Y) quasi_total V105() V106() V107() Element of bool [: the carrier of Y,REAL:]
[: the carrier of Y,REAL:] is non empty Relation-like V105() V106() V107() set
bool [: the carrier of Y,REAL:] is non empty set
the normF of Y . (tseq . m) is V11() real ext-real Element of REAL
e is non empty Relation-like X -defined the carrier of Y -valued Function-like V23(X) quasi_total Element of bool [:X, the carrier of Y:]
e . m is Element of the carrier of Y
X is non empty set
Y is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like NORMSTR
(X,Y) is non empty NORMSTR
(X,Y) is non empty Element of bool the carrier of (RealVectSpace (X,Y))
RealVectSpace (X,Y) is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() RLSStruct
the carrier of (RealVectSpace (X,Y)) is non empty set
bool the carrier of (RealVectSpace (X,Y)) is non empty set
Zero_ ((X,Y),(RealVectSpace (X,Y))) is Element of (X,Y)
Add_ ((X,Y),(RealVectSpace (X,Y))) is non empty Relation-like [:(X,Y),(X,Y):] -defined (X,Y) -valued Function-like V23([:(X,Y),(X,Y):]) quasi_total Element of bool [:[:(X,Y),(X,Y):],(X,Y):]
[:(X,Y),(X,Y):] is non empty Relation-like set
[:[:(X,Y),(X,Y):],(X,Y):] is non empty Relation-like set
bool [:[:(X,Y),(X,Y):],(X,Y):] is non empty set
Mult_ ((X,Y),(RealVectSpace (X,Y))) is non empty Relation-like [:REAL,(X,Y):] -defined (X,Y) -valued Function-like V23([:REAL,(X,Y):]) quasi_total Element of bool [:[:REAL,(X,Y):],(X,Y):]
[:REAL,(X,Y):] is non empty Relation-like set
[:[:REAL,(X,Y):],(X,Y):] is non empty Relation-like set
bool [:[:REAL,(X,Y):],(X,Y):] is non empty set
(X,Y) is non empty Relation-like (X,Y) -defined REAL -valued Function-like V23((X,Y)) quasi_total V105() V106() V107() Element of bool [:(X,Y),REAL:]
[:(X,Y),REAL:] is non empty Relation-like V105() V106() V107() set
bool [:(X,Y),REAL:] is non empty set
NORMSTR(# (X,Y),(Zero_ ((X,Y),(RealVectSpace (X,Y)))),(Add_ ((X,Y),(RealVectSpace (X,Y)))),(Mult_ ((X,Y),(RealVectSpace (X,Y)))),(X,Y) #) is non empty strict NORMSTR
0. (X,Y) is V49((X,Y)) Element of the carrier of (X,Y)
the carrier of (X,Y) is non empty set
the ZeroF of (X,Y) is Element of the carrier of (X,Y)
||.(0. (X,Y)).|| is V11() real ext-real Element of REAL
the normF of (X,Y) is non empty Relation-like the carrier of (X,Y) -defined REAL -valued Function-like V23( the carrier of (X,Y)) quasi_total V105() V106() V107() Element of bool [: the carrier of (X,Y),REAL:]
[: the carrier of (X,Y),REAL:] is non empty Relation-like V105() V106() V107() set
bool [: the carrier of (X,Y),REAL:] is non empty set
the normF of (X,Y) . (0. (X,Y)) is V11() real ext-real Element of REAL
vseq is Element of the carrier of (X,Y)
||.vseq.|| is V11() real ext-real Element of REAL
the normF of (X,Y) . vseq is V11() real ext-real Element of REAL
f is Element of the carrier of (X,Y)
||.f.|| is V11() real ext-real Element of REAL
the normF of (X,Y) . f is V11() real ext-real Element of REAL
tseq is Element of the carrier of (X,Y)
tseq is V11() real ext-real Element of REAL
tseq * tseq is Element of the carrier of (X,Y)
the Mult of (X,Y) is non empty Relation-like [:REAL, the carrier of (X,Y):] -defined the carrier of (X,Y) -valued Function-like V23([:REAL, the carrier of (X,Y):]) quasi_total Element of bool [:[:REAL, the carrier of (X,Y):], the carrier of (X,Y):]
[:REAL, the carrier of (X,Y):] is non empty Relation-like set
[:[:REAL, the carrier of (X,Y):], the carrier of (X,Y):] is non empty Relation-like set
bool [:[:REAL, the carrier of (X,Y):], the carrier of (X,Y):] is non empty set
K580( the Mult of (X,Y),tseq,tseq) is set
[tseq,tseq] is set
{tseq,tseq} is set
{tseq} is V115() V116() V117() set
{{tseq,tseq},{tseq}} is set
the Mult of (X,Y) . [tseq,tseq] is set
||.(tseq * tseq).|| is V11() real ext-real Element of REAL
the normF of (X,Y) . (tseq * tseq) is V11() real ext-real Element of REAL
abs tseq is V11() real ext-real Element of REAL
||.tseq.|| is V11() real ext-real Element of REAL
the normF of (X,Y) . tseq is V11() real ext-real Element of REAL
(abs tseq) * ||.tseq.|| is V11() real ext-real Element of REAL
tv is Element of the carrier of (X,Y)
e is Element of the carrier of (X,Y)
tv + e is Element of the carrier of (X,Y)
the addF of (X,Y) is non empty Relation-like [: the carrier of (X,Y), the carrier of (X,Y):] -defined the carrier of (X,Y) -valued Function-like V23([: the carrier of (X,Y), the carrier of (X,Y):]) quasi_total Element of bool [:[: the carrier of (X,Y), the carrier of (X,Y):], the carrier of (X,Y):]
[: the carrier of (X,Y), the carrier of (X,Y):] is non empty Relation-like set
[:[: the carrier of (X,Y), the carrier of (X,Y):], the carrier of (X,Y):] is non empty Relation-like set
bool [:[: the carrier of (X,Y), the carrier of (X,Y):], the carrier of (X,Y):] is non empty set
K584( the carrier of (X,Y), the addF of (X,Y),tv,e) is Element of the carrier of (X,Y)
[tv,e] is set
{tv,e} is set
{tv} is set
{{tv,e},{tv}} is set
the addF of (X,Y) . [tv,e] is set
||.(tv + e).|| is V11() real ext-real Element of REAL
the normF of (X,Y) . (tv + e) is V11() real ext-real Element of REAL
||.tv.|| is V11() real ext-real Element of REAL
the normF of (X,Y) . tv is V11() real ext-real Element of REAL
||.e.|| is V11() real ext-real Element of REAL
the normF of (X,Y) . e is V11() real ext-real Element of REAL
||.tv.|| + ||.e.|| is V11() real ext-real Element of REAL
X is non empty set
Y is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like NORMSTR
(X,Y) is non empty NORMSTR
(X,Y) is non empty Element of bool the carrier of (RealVectSpace (X,Y))
RealVectSpace (X,Y) is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() RLSStruct
the carrier of (RealVectSpace (X,Y)) is non empty set
bool the carrier of (RealVectSpace (X,Y)) is non empty set
Zero_ ((X,Y),(RealVectSpace (X,Y))) is Element of (X,Y)
Add_ ((X,Y),(RealVectSpace (X,Y))) is non empty Relation-like [:(X,Y),(X,Y):] -defined (X,Y) -valued Function-like V23([:(X,Y),(X,Y):]) quasi_total Element of bool [:[:(X,Y),(X,Y):],(X,Y):]
[:(X,Y),(X,Y):] is non empty Relation-like set
[:[:(X,Y),(X,Y):],(X,Y):] is non empty Relation-like set
bool [:[:(X,Y),(X,Y):],(X,Y):] is non empty set
Mult_ ((X,Y),(RealVectSpace (X,Y))) is non empty Relation-like [:REAL,(X,Y):] -defined (X,Y) -valued Function-like V23([:REAL,(X,Y):]) quasi_total Element of bool [:[:REAL,(X,Y):],(X,Y):]
[:REAL,(X,Y):] is non empty Relation-like set
[:[:REAL,(X,Y):],(X,Y):] is non empty Relation-like set
bool [:[:REAL,(X,Y):],(X,Y):] is non empty set
(X,Y) is non empty Relation-like (X,Y) -defined REAL -valued Function-like V23((X,Y)) quasi_total V105() V106() V107() Element of bool [:(X,Y),REAL:]
[:(X,Y),REAL:] is non empty Relation-like V105() V106() V107() set
bool [:(X,Y),REAL:] is non empty set
NORMSTR(# (X,Y),(Zero_ ((X,Y),(RealVectSpace (X,Y)))),(Add_ ((X,Y),(RealVectSpace (X,Y)))),(Mult_ ((X,Y),(RealVectSpace (X,Y)))),(X,Y) #) is non empty strict NORMSTR
RLSStruct(# (X,Y),(Zero_ ((X,Y),(RealVectSpace (X,Y)))),(Add_ ((X,Y),(RealVectSpace (X,Y)))),(Mult_ ((X,Y),(RealVectSpace (X,Y)))) #) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() RLSStruct
X is non empty set
Y is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like NORMSTR
(X,Y) is non empty NORMSTR
(X,Y) is non empty Element of bool the carrier of (RealVectSpace (X,Y))
RealVectSpace (X,Y) is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() RLSStruct
the carrier of (RealVectSpace (X,Y)) is non empty set
bool the carrier of (RealVectSpace (X,Y)) is non empty set
Zero_ ((X,Y),(RealVectSpace (X,Y))) is Element of (X,Y)
Add_ ((X,Y),(RealVectSpace (X,Y))) is non empty Relation-like [:(X,Y),(X,Y):] -defined (X,Y) -valued Function-like V23([:(X,Y),(X,Y):]) quasi_total Element of bool [:[:(X,Y),(X,Y):],(X,Y):]
[:(X,Y),(X,Y):] is non empty Relation-like set
[:[:(X,Y),(X,Y):],(X,Y):] is non empty Relation-like set
bool [:[:(X,Y),(X,Y):],(X,Y):] is non empty set
Mult_ ((X,Y),(RealVectSpace (X,Y))) is non empty Relation-like [:REAL,(X,Y):] -defined (X,Y) -valued Function-like V23([:REAL,(X,Y):]) quasi_total Element of bool [:[:REAL,(X,Y):],(X,Y):]
[:REAL,(X,Y):] is non empty Relation-like set
[:[:REAL,(X,Y):],(X,Y):] is non empty Relation-like set
bool [:[:REAL,(X,Y):],(X,Y):] is non empty set
(X,Y) is non empty Relation-like (X,Y) -defined REAL -valued Function-like V23((X,Y)) quasi_total V105() V106() V107() Element of bool [:(X,Y),REAL:]
[:(X,Y),REAL:] is non empty Relation-like V105() V106() V107() set
bool [:(X,Y),REAL:] is non empty set
NORMSTR(# (X,Y),(Zero_ ((X,Y),(RealVectSpace (X,Y)))),(Add_ ((X,Y),(RealVectSpace (X,Y)))),(Mult_ ((X,Y),(RealVectSpace (X,Y)))),(X,Y) #) is non empty strict NORMSTR
X is non empty set
Y is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like NORMSTR
(X,Y) is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like NORMSTR
(X,Y) is non empty Element of bool the carrier of (RealVectSpace (X,Y))
RealVectSpace (X,Y) is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() RLSStruct
the carrier of (RealVectSpace (X,Y)) is non empty set
bool the carrier of (RealVectSpace (X,Y)) is non empty set
Zero_ ((X,Y),(RealVectSpace (X,Y))) is Element of (X,Y)
Add_ ((X,Y),(RealVectSpace (X,Y))) is non empty Relation-like [:(X,Y),(X,Y):] -defined (X,Y) -valued Function-like V23([:(X,Y),(X,Y):]) quasi_total Element of bool [:[:(X,Y),(X,Y):],(X,Y):]
[:(X,Y),(X,Y):] is non empty Relation-like set
[:[:(X,Y),(X,Y):],(X,Y):] is non empty Relation-like set
bool [:[:(X,Y),(X,Y):],(X,Y):] is non empty set
Mult_ ((X,Y),(RealVectSpace (X,Y))) is non empty Relation-like [:REAL,(X,Y):] -defined (X,Y) -valued Function-like V23([:REAL,(X,Y):]) quasi_total Element of bool [:[:REAL,(X,Y):],(X,Y):]
[:REAL,(X,Y):] is non empty Relation-like set
[:[:REAL,(X,Y):],(X,Y):] is non empty Relation-like set
bool [:[:REAL,(X,Y):],(X,Y):] is non empty set
(X,Y) is non empty Relation-like (X,Y) -defined REAL -valued Function-like V23((X,Y)) quasi_total V105() V106() V107() Element of bool [:(X,Y),REAL:]
[:(X,Y),REAL:] is non empty Relation-like V105() V106() V107() set
bool [:(X,Y),REAL:] is non empty set
NORMSTR(# (X,Y),(Zero_ ((X,Y),(RealVectSpace (X,Y)))),(Add_ ((X,Y),(RealVectSpace (X,Y)))),(Mult_ ((X,Y),(RealVectSpace (X,Y)))),(X,Y) #) is non empty strict NORMSTR
the carrier of (X,Y) is non empty set
the carrier of Y is non empty set
[:X, the carrier of Y:] is non empty Relation-like set
bool [:X, the carrier of Y:] is non empty set
vseq is Element of the carrier of (X,Y)
f is Element of the carrier of (X,Y)
tseq is Element of the carrier of (X,Y)
vseq - f is Element of the carrier of (X,Y)
- f is Element of the carrier of (X,Y)
vseq + (- f) is Element of the carrier of (X,Y)
the addF of (X,Y) is non empty Relation-like [: the carrier of (X,Y), the carrier of (X,Y):] -defined the carrier of (X,Y) -valued Function-like V23([: the carrier of (X,Y), the carrier of (X,Y):]) quasi_total Element of bool [:[: the carrier of (X,Y), the carrier of (X,Y):], the carrier of (X,Y):]
[: the carrier of (X,Y), the carrier of (X,Y):] is non empty Relation-like set
[:[: the carrier of (X,Y), the carrier of (X,Y):], the carrier of (X,Y):] is non empty Relation-like set
bool [:[: the carrier of (X,Y), the carrier of (X,Y):], the carrier of (X,Y):] is non empty set
K584( the carrier of (X,Y), the addF of (X,Y),vseq,(- f)) is Element of the carrier of (X,Y)
[vseq,(- f)] is set
{vseq,(- f)} is set
{vseq} is set
{{vseq,(- f)},{vseq}} is set
the addF of (X,Y) . [vseq,(- f)] is set
tseq is non empty Relation-like X -defined the carrier of Y -valued Function-like V23(X) quasi_total (X,Y) Element of bool [:X, the carrier of Y:]
tv is non empty Relation-like X -defined the carrier of Y -valued Function-like V23(X) quasi_total (X,Y) Element of bool [:X, the carrier of Y:]
e is non empty Relation-like X -defined the carrier of Y -valued Function-like V23(X) quasi_total (X,Y) Element of bool [:X, the carrier of Y:]
m is Element of X
e . m is Element of the carrier of Y
tseq . m is Element of the carrier of Y
tv . m is Element of the carrier of Y
(tseq . m) - (tv . m) is Element of the carrier of Y
- (tv . m) is Element of the carrier of Y
(tseq . m) + (- (tv . m)) is Element of the carrier of Y
the addF of Y is non empty Relation-like [: the carrier of Y, the carrier of Y:] -defined the carrier of Y -valued Function-like V23([: the carrier of Y, the carrier of Y:]) quasi_total Element of bool [:[: the carrier of Y, the carrier of Y:], the carrier of Y:]
[: the carrier of Y, the carrier of Y:] is non empty Relation-like set
[:[: the carrier of Y, the carrier of Y:], the carrier of Y:] is non empty Relation-like set
bool [:[: the carrier of Y, the carrier of Y:], the carrier of Y:] is non empty set
K584( the carrier of Y, the addF of Y,(tseq . m),(- (tv . m))) is Element of the carrier of Y
[(tseq . m),(- (tv . m))] is set
{(tseq . m),(- (tv . m))} is set
{(tseq . m)} is set
{{(tseq . m),(- (tv . m))},{(tseq . m)}} is set
the addF of Y . [(tseq . m),(- (tv . m))] is set
(e . m) + (tv . m) is Element of the carrier of Y
K584( the carrier of Y, the addF of Y,(e . m),(tv . m)) is Element of the carrier of Y
[(e . m),(tv . m)] is set
{(e . m),(tv . m)} is set
{(e . m)} is set
{{(e . m),(tv . m)},{(e . m)}} is set
the addF of Y . [(e . m),(tv . m)] is set
(tv . m) - (tv . m) is Element of the carrier of Y
(tv . m) + (- (tv . m)) is Element of the carrier of Y
K584( the carrier of Y, the addF of Y,(tv . m),(- (tv . m))) is Element of the carrier of Y
[(tv . m),(- (tv . m))] is set
{(tv . m),(- (tv . m))} is set
{(tv . m)} is set
{{(tv . m),(- (tv . m))},{(tv . m)}} is set
the addF of Y . [(tv . m),(- (tv . m))] is set
(tseq . m) - ((tv . m) - (tv . m)) is Element of the carrier of Y
- ((tv . m) - (tv . m)) is Element of the carrier of Y
(tseq . m) + (- ((tv . m) - (tv . m))) is Element of the carrier of Y
K584( the carrier of Y, the addF of Y,(tseq . m),(- ((tv . m) - (tv . m)))) is Element of the carrier of Y
[(tseq . m),(- ((tv . m) - (tv . m)))] is set
{(tseq . m),(- ((tv . m) - (tv . m)))} is set
{{(tseq . m),(- ((tv . m) - (tv . m)))},{(tseq . m)}} is set
the addF of Y . [(tseq . m),(- ((tv . m) - (tv . m)))] is set
0. Y is V49(Y) Element of the carrier of Y
the ZeroF of Y is Element of the carrier of Y
(tseq . m) - (0. Y) is Element of the carrier of Y
- (0. Y) is Element of the carrier of Y
(tseq . m) + (- (0. Y)) is Element of the carrier of Y
K584( the carrier of Y, the addF of Y,(tseq . m),(- (0. Y))) is Element of the carrier of Y
[(tseq . m),(- (0. Y))] is set
{(tseq . m),(- (0. Y))} is set
{{(tseq . m),(- (0. Y))},{(tseq . m)}} is set
the addF of Y . [(tseq . m),(- (0. Y))] is set
tseq + f is Element of the carrier of (X,Y)
K584( the carrier of (X,Y), the addF of (X,Y),tseq,f) is Element of the carrier of (X,Y)
[tseq,f] is set
{tseq,f} is set
{tseq} is set
{{tseq,f},{tseq}} is set
the addF of (X,Y) . [tseq,f] is set
f - f is Element of the carrier of (X,Y)
f + (- f) is Element of the carrier of (X,Y)
K584( the carrier of (X,Y), the addF of (X,Y),f,(- f)) is Element of the carrier of (X,Y)
[f,(- f)] is set
{f,(- f)} is set
{f} is set
{{f,(- f)},{f}} is set
the addF of (X,Y) . [f,(- f)] is set
tseq + (f - f) is Element of the carrier of (X,Y)
K584( the carrier of (X,Y), the addF of (X,Y),tseq,(f - f)) is Element of the carrier of (X,Y)
[tseq,(f - f)] is set
{tseq,(f - f)} is set
{{tseq,(f - f)},{tseq}} is set
the addF of (X,Y) . [tseq,(f - f)] is set
0. (X,Y) is V49((X,Y)) Element of the carrier of (X,Y)
the ZeroF of (X,Y) is Element of the carrier of (X,Y)
tseq + (0. (X,Y)) is Element of the carrier of (X,Y)
K584( the carrier of (X,Y), the addF of (X,Y),tseq,(0. (X,Y))) is Element of the carrier of (X,Y)
[tseq,(0. (X,Y))] is set
{tseq,(0. (X,Y))} is set
{{tseq,(0. (X,Y))},{tseq}} is set
the addF of (X,Y) . [tseq,(0. (X,Y))] is set
vseq - (f - f) is Element of the carrier of (X,Y)
- (f - f) is Element of the carrier of (X,Y)
vseq + (- (f - f)) is Element of the carrier of (X,Y)
K584( the carrier of (X,Y), the addF of (X,Y),vseq,(- (f - f))) is Element of the carrier of (X,Y)
[vseq,(- (f - f))] is set
{vseq,(- (f - f))} is set
{{vseq,(- (f - f))},{vseq}} is set
the addF of (X,Y) . [vseq,(- (f - f))] is set
vseq - (0. (X,Y)) is Element of the carrier of (X,Y)
- (0. (X,Y)) is Element of the carrier of (X,Y)
vseq + (- (0. (X,Y))) is Element of the carrier of (X,Y)
K584( the carrier of (X,Y), the addF of (X,Y),vseq,(- (0. (X,Y)))) is Element of the carrier of (X,Y)
[vseq,(- (0. (X,Y)))] is set
{vseq,(- (0. (X,Y)))} is set
{{vseq,(- (0. (X,Y)))},{vseq}} is set
the addF of (X,Y) . [vseq,(- (0. (X,Y)))] is set
m is Element of X
tseq . m is Element of the carrier of Y
e . m is Element of the carrier of Y
tv . m is Element of the carrier of Y
(e . m) + (tv . m) is Element of the carrier of Y
K584( the carrier of Y, the addF of Y,(e . m),(tv . m)) is Element of the carrier of Y
[(e . m),(tv . m)] is set
{(e . m),(tv . m)} is set
{(e . m)} is set
{{(e . m),(tv . m)},{(e . m)}} is set
the addF of Y . [(e . m),(tv . m)] is set
(tseq . m) - (tv . m) is Element of the carrier of Y
- (tv . m) is Element of the carrier of Y
(tseq . m) + (- (tv . m)) is Element of the carrier of Y
K584( the carrier of Y, the addF of Y,(tseq . m),(- (tv . m))) is Element of the carrier of Y
[(tseq . m),(- (tv . m))] is set
{(tseq . m),(- (tv . m))} is set
{(tseq . m)} is set
{{(tseq . m),(- (tv . m))},{(tseq . m)}} is set
the addF of Y . [(tseq . m),(- (tv . m))] is set
(tv . m) - (tv . m) is Element of the carrier of Y
(tv . m) + (- (tv . m)) is Element of the carrier of Y
K584( the carrier of Y, the addF of Y,(tv . m),(- (tv . m))) is Element of the carrier of Y
[(tv . m),(- (tv . m))] is set
{(tv . m),(- (tv . m))} is set
{(tv . m)} is set
{{(tv . m),(- (tv . m))},{(tv . m)}} is set
the addF of Y . [(tv . m),(- (tv . m))] is set
(e . m) + ((tv . m) - (tv . m)) is Element of the carrier of Y
K584( the carrier of Y, the addF of Y,(e . m),((tv . m) - (tv . m))) is Element of the carrier of Y
[(e . m),((tv . m) - (tv . m))] is set
{(e . m),((tv . m) - (tv . m))} is set
{{(e . m),((tv . m) - (tv . m))},{(e . m)}} is set
the addF of Y . [(e . m),((tv . m) - (tv . m))] is set
(e . m) + (0. Y) is Element of the carrier of Y
K584( the carrier of Y, the addF of Y,(e . m),(0. Y)) is Element of the carrier of Y
[(e . m),(0. Y)] is set
{(e . m),(0. Y)} is set
{{(e . m),(0. Y)},{(e . m)}} is set
the addF of Y . [(e . m),(0. Y)] is set
m is Element of X
e . m is Element of the carrier of Y
tseq . m is Element of the carrier of Y
tv . m is Element of the carrier of Y
(tseq . m) - (tv . m) is Element of the carrier of Y
- (tv . m) is Element of the carrier of Y
(tseq . m) + (- (tv . m)) is Element of the carrier of Y
K584( the carrier of Y, the addF of Y,(tseq . m),(- (tv . m))) is Element of the carrier of Y
[(tseq . m),(- (tv . m))] is set
{(tseq . m),(- (tv . m))} is set
{(tseq . m)} is set
{{(tseq . m),(- (tv . m))},{(tseq . m)}} is set
the addF of Y . [(tseq . m),(- (tv . m))] is set
m is Element of X
e . m is Element of the carrier of Y
tseq . m is Element of the carrier of Y
tv . m is Element of the carrier of Y
(tseq . m) - (tv . m) is Element of the carrier of Y
- (tv . m) is Element of the carrier of Y
(tseq . m) + (- (tv . m)) is Element of the carrier of Y
K584( the carrier of Y, the addF of Y,(tseq . m),(- (tv . m))) is Element of the carrier of Y
[(tseq . m),(- (tv . m))] is set
{(tseq . m),(- (tv . m))} is set
{(tseq . m)} is set
{{(tseq . m),(- (tv . m))},{(tseq . m)}} is set
the addF of Y . [(tseq . m),(- (tv . m))] is set
n is Element of X
e . n is Element of the carrier of Y
tseq . n is Element of the carrier of Y
tv . n is Element of the carrier of Y
(tseq . n) - (tv . n) is Element of the carrier of Y
- (tv . n) is Element of the carrier of Y
(tseq . n) + (- (tv . n)) is Element of the carrier of Y
K584( the carrier of Y, the addF of Y,(tseq . n),(- (tv . n))) is Element of the carrier of Y
[(tseq . n),(- (tv . n))] is set
{(tseq . n),(- (tv . n))} is set
{(tseq . n)} is set
{{(tseq . n),(- (tv . n))},{(tseq . n)}} is set
the addF of Y . [(tseq . n),(- (tv . n))] is set
X 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:]
lim Y is V11() real ext-real Element of REAL
vseq is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V115() V116() V117() V118() V119() V120() V145() V168() Element of NAT
vseq is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V115() V116() V117() V118() V119() V120() V145() V168() Element of NAT
NAT --> X is non empty Relation-like NAT -defined REAL -valued Function-like constant V23( NAT ) quasi_total V105() V106() V107() bounded_above bounded_below bounded convergent Element of bool [:NAT,REAL:]
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
f . 0 is V11() real ext-real Element of REAL
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:]
tseq is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V115() V116() V117() V118() V119() V120() V145() V168() Element of NAT
(Y ^\ vseq) . tseq is V11() real ext-real Element of REAL
vseq + tseq is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V115() V116() V117() V118() V119() V120() V145() V168() Element of NAT
Y . (vseq + tseq) is V11() real ext-real Element of REAL
f . tseq is V11() real ext-real Element of REAL
lim (Y ^\ vseq) is V11() real ext-real Element of REAL
X is non empty set
Y is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like NORMSTR
(X,Y) is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like NORMSTR
(X,Y) is non empty Element of bool the carrier of (RealVectSpace (X,Y))
RealVectSpace (X,Y) is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() RLSStruct
the carrier of (RealVectSpace (X,Y)) is non empty set
bool the carrier of (RealVectSpace (X,Y)) is non empty set
Zero_ ((X,Y),(RealVectSpace (X,Y))) is Element of (X,Y)
Add_ ((X,Y),(RealVectSpace (X,Y))) is non empty Relation-like [:(X,Y),(X,Y):] -defined (X,Y) -valued Function-like V23([:(X,Y),(X,Y):]) quasi_total Element of bool [:[:(X,Y),(X,Y):],(X,Y):]
[:(X,Y),(X,Y):] is non empty Relation-like set
[:[:(X,Y),(X,Y):],(X,Y):] is non empty Relation-like set
bool [:[:(X,Y),(X,Y):],(X,Y):] is non empty set
Mult_ ((X,Y),(RealVectSpace (X,Y))) is non empty Relation-like [:REAL,(X,Y):] -defined (X,Y) -valued Function-like V23([:REAL,(X,Y):]) quasi_total Element of bool [:[:REAL,(X,Y):],(X,Y):]
[:REAL,(X,Y):] is non empty Relation-like set
[:[:REAL,(X,Y):],(X,Y):] is non empty Relation-like set
bool [:[:REAL,(X,Y):],(X,Y):] is non empty set
(X,Y) is non empty Relation-like (X,Y) -defined REAL -valued Function-like V23((X,Y)) quasi_total V105() V106() V107() Element of bool [:(X,Y),REAL:]
[:(X,Y),REAL:] is non empty Relation-like V105() V106() V107() set
bool [:(X,Y),REAL:] is non empty set
NORMSTR(# (X,Y),(Zero_ ((X,Y),(RealVectSpace (X,Y)))),(Add_ ((X,Y),(RealVectSpace (X,Y)))),(Mult_ ((X,Y),(RealVectSpace (X,Y)))),(X,Y) #) is non empty strict NORMSTR
the carrier of (X,Y) is non empty set
[:NAT, the carrier of (X,Y):] is non empty Relation-like set
bool [:NAT, the carrier of (X,Y):] is non empty set
vseq is non empty Relation-like NAT -defined the carrier of (X,Y) -valued Function-like V23( NAT ) quasi_total Element of bool [:NAT, the carrier of (X,Y):]
the carrier of Y is non empty set
[:NAT, the carrier of Y:] is non empty Relation-like set
bool [:NAT, the carrier of Y:] is non empty set
f is Element of X
tseq is non empty Relation-like NAT -defined the carrier of Y -valued Function-like V23( NAT ) quasi_total Element of bool [:NAT, the carrier of Y:]
lim tseq is Element of the carrier of Y
tseq is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V115() V116() V117() V118() V119() V120() V145() V168() Element of NAT
tseq . tseq is Element of the carrier of Y
tv is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V115() V116() V117() V118() V119() V120() V145() V168() Element of NAT
tseq . tv is Element of the carrier of Y
(tseq . tseq) - (tseq . tv) is Element of the carrier of Y
- (tseq . tv) is Element of the carrier of Y
(tseq . tseq) + (- (tseq . tv)) is Element of the carrier of Y
the addF of Y is non empty Relation-like [: the carrier of Y, the carrier of Y:] -defined the carrier of Y -valued Function-like V23([: the carrier of Y, the carrier of Y:]) quasi_total Element of bool [:[: the carrier of Y, the carrier of Y:], the carrier of Y:]
[: the carrier of Y, the carrier of Y:] is non empty Relation-like set
[:[: the carrier of Y, the carrier of Y:], the carrier of Y:] is non empty Relation-like set
bool [:[: the carrier of Y, the carrier of Y:], the carrier of Y:] is non empty set
K584( the carrier of Y, the addF of Y,(tseq . tseq),(- (tseq . tv))) is Element of the carrier of Y
[(tseq . tseq),(- (tseq . tv))] is set
{(tseq . tseq),(- (tseq . tv))} is set
{(tseq . tseq)} is set
{{(tseq . tseq),(- (tseq . tv))},{(tseq . tseq)}} is set
the addF of Y . [(tseq . tseq),(- (tseq . tv))] is set
||.((tseq . tseq) - (tseq . tv)).|| is V11() real ext-real non negative Element of REAL
the normF of Y is non empty Relation-like the carrier of Y -defined REAL -valued Function-like V23( the carrier of Y) quasi_total V105() V106() V107() Element of bool [: the carrier of Y,REAL:]
[: the carrier of Y,REAL:] is non empty Relation-like V105() V106() V107() set
bool [: the carrier of Y,REAL:] is non empty set
the normF of Y . ((tseq . tseq) - (tseq . tv)) is V11() real ext-real Element of REAL
vseq . tseq is Element of the carrier of (X,Y)
vseq . tv is Element of the carrier of (X,Y)
(vseq . tseq) - (vseq . tv) is Element of the carrier of (X,Y)
- (vseq . tv) is Element of the carrier of (X,Y)
(vseq . tseq) + (- (vseq . tv)) is Element of the carrier of (X,Y)
the addF of (X,Y) is non empty Relation-like [: the carrier of (X,Y), the carrier of (X,Y):] -defined the carrier of (X,Y) -valued Function-like V23([: the carrier of (X,Y), the carrier of (X,Y):]) quasi_total Element of bool [:[: the carrier of (X,Y), the carrier of (X,Y):], the carrier of (X,Y):]
[: the carrier of (X,Y), the carrier of (X,Y):] is non empty Relation-like set
[:[: the carrier of (X,Y), the carrier of (X,Y):], the carrier of (X,Y):] is non empty Relation-like set
bool [:[: the carrier of (X,Y), the carrier of (X,Y):], the carrier of (X,Y):] is non empty set
K584( the carrier of (X,Y), the addF of (X,Y),(vseq . tseq),(- (vseq . tv))) is Element of the carrier of (X,Y)
[(vseq . tseq),(- (vseq . tv))] is set
{(vseq . tseq),(- (vseq . tv))} is set
{(vseq . tseq)} is set
{{(vseq . tseq),(- (vseq . tv))},{(vseq . tseq)}} is set
the addF of (X,Y) . [(vseq . tseq),(- (vseq . tv))] is set
||.((vseq . tseq) - (vseq . tv)).|| is V11() real ext-real non negative Element of REAL
the normF of (X,Y) is non empty Relation-like the carrier of (X,Y) -defined REAL -valued Function-like V23( the carrier of (X,Y)) quasi_total V105() V106() V107() Element of bool [: the carrier of (X,Y),REAL:]
[: the carrier of (X,Y),REAL:] is non empty Relation-like V105() V106() V107() set
bool [: the carrier of (X,Y),REAL:] is non empty set
the normF of (X,Y) . ((vseq . tseq) - (vseq . tv)) is V11() real ext-real Element of REAL
[:X, the carrier of Y:] is non empty Relation-like set
bool [:X, the carrier of Y:] is non empty set
(X,Y,(vseq . tv)) is non empty Relation-like X -defined the carrier of Y -valued Function-like V23(X) quasi_total (X,Y) Element of bool [:X, the carrier of Y:]
(X,Y,(vseq . tseq)) is non empty Relation-like X -defined the carrier of Y -valued Function-like V23(X) quasi_total (X,Y) Element of bool [:X, the carrier of Y:]
(X,Y,(vseq . tseq)) . f is Element of the carrier of Y
(X,Y,(vseq . tv)) . f is Element of the carrier of Y
e is non empty Relation-like X -defined the carrier of Y -valued Function-like V23(X) quasi_total (X,Y) Element of bool [:X, the carrier of Y:]
e . f is Element of the carrier of Y
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
e is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V115() V116() V117() V118() V119() V120() V145() V168() Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V115() V116() V117() V118() V119() V120() V145() V168() Element of NAT
tseq . e is Element of the carrier of Y
tseq . m is Element of the carrier of Y
(tseq . e) - (tseq . m) is Element of the carrier of Y
- (tseq . m) is Element of the carrier of Y
(tseq . e) + (- (tseq . m)) is Element of the carrier of Y
the addF of Y is non empty Relation-like [: the carrier of Y, the carrier of Y:] -defined the carrier of Y -valued Function-like V23([: the carrier of Y, the carrier of Y:]) quasi_total Element of bool [:[: the carrier of Y, the carrier of Y:], the carrier of Y:]
[: the carrier of Y, the carrier of Y:] is non empty Relation-like set
[:[: the carrier of Y, the carrier of Y:], the carrier of Y:] is non empty Relation-like set
bool [:[: the carrier of Y, the carrier of Y:], the carrier of Y:] is non empty set
K584( the carrier of Y, the addF of Y,(tseq . e),(- (tseq . m))) is Element of the carrier of Y
[(tseq . e),(- (tseq . m))] is set
{(tseq . e),(- (tseq . m))} is set
{(tseq . e)} is set
{{(tseq . e),(- (tseq . m))},{(tseq . e)}} is set
the addF of Y . [(tseq . e),(- (tseq . m))] is set
||.((tseq . e) - (tseq . m)).|| is V11() real ext-real non negative Element of REAL
the normF of Y is non empty Relation-like the carrier of Y -defined REAL -valued Function-like V23( the carrier of Y) quasi_total V105() V106() V107() Element of bool [: the carrier of Y,REAL:]
[: the carrier of Y,REAL:] is non empty Relation-like V105() V106() V107() set
bool [: the carrier of Y,REAL:] is non empty set
the normF of Y . ((tseq . e) - (tseq . m)) is V11() real ext-real Element of REAL
vseq . e is Element of the carrier of (X,Y)
vseq . m is Element of the carrier of (X,Y)
(vseq . e) - (vseq . m) is Element of the carrier of (X,Y)
- (vseq . m) is Element of the carrier of (X,Y)
(vseq . e) + (- (vseq . m)) is Element of the carrier of (X,Y)
the addF of (X,Y) is non empty Relation-like [: the carrier of (X,Y), the carrier of (X,Y):] -defined the carrier of (X,Y) -valued Function-like V23([: the carrier of (X,Y), the carrier of (X,Y):]) quasi_total Element of bool [:[: the carrier of (X,Y), the carrier of (X,Y):], the carrier of (X,Y):]
[: the carrier of (X,Y), the carrier of (X,Y):] is non empty Relation-like set
[:[: the carrier of (X,Y), the carrier of (X,Y):], the carrier of (X,Y):] is non empty Relation-like set
bool [:[: the carrier of (X,Y), the carrier of (X,Y):], the carrier of (X,Y):] is non empty set
K584( the carrier of (X,Y), the addF of (X,Y),(vseq . e),(- (vseq . m))) is Element of the carrier of (X,Y)
[(vseq . e),(- (vseq . m))] is set
{(vseq . e),(- (vseq . m))} is set
{(vseq . e)} is set
{{(vseq . e),(- (vseq . m))},{(vseq . e)}} is set
the addF of (X,Y) . [(vseq . e),(- (vseq . m))] is set
||.((vseq . e) - (vseq . m)).|| is V11() real ext-real non negative Element of REAL
the normF of (X,Y) is non empty Relation-like the carrier of (X,Y) -defined REAL -valued Function-like V23( the carrier of (X,Y)) quasi_total V105() V106() V107() Element of bool [: the carrier of (X,Y),REAL:]
[: the carrier of (X,Y),REAL:] is non empty Relation-like V105() V106() V107() set
bool [: the carrier of (X,Y),REAL:] is non empty set
the normF of (X,Y) . ((vseq . e) - (vseq . m)) is V11() real ext-real Element of REAL
[:X, the carrier of Y:] is non empty Relation-like set
bool [:X, the carrier of Y:] is non empty set
f is non empty Relation-like X -defined the carrier of Y -valued Function-like V23(X) quasi_total Element of bool [:X, the carrier of Y:]
tseq is V11() real ext-real set
tv is V11() real ext-real Element of REAL
e is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V115() V116() V117() V118() V119() V120() V145() V168() Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V115() V116() V117() V118() V119() V120() V145() V168() Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V115() V116() V117() V118() V119() V120() V145() V168() Element of NAT
vseq . n is Element of the carrier of (X,Y)
||.(vseq . n).|| is V11() real ext-real non negative Element of REAL
the normF of (X,Y) is non empty Relation-like the carrier of (X,Y) -defined REAL -valued Function-like V23( the carrier of (X,Y)) quasi_total V105() V106() V107() Element of bool [: the carrier of (X,Y),REAL:]
[: the carrier of (X,Y),REAL:] is non empty Relation-like V105() V106() V107() set
bool [: the carrier of (X,Y),REAL:] is non empty set
the normF of (X,Y) . (vseq . n) 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.|| . n is V11() real ext-real Element of REAL
vseq . m is Element of the carrier of (X,Y)
(vseq . n) - (vseq . m) is Element of the carrier of (X,Y)
- (vseq . m) is Element of the carrier of (X,Y)
(vseq . n) + (- (vseq . m)) is Element of the carrier of (X,Y)
the addF of (X,Y) is non empty Relation-like [: the carrier of (X,Y), the carrier of (X,Y):] -defined the carrier of (X,Y) -valued Function-like V23([: the carrier of (X,Y), the carrier of (X,Y):]) quasi_total Element of bool [:[: the carrier of (X,Y), the carrier of (X,Y):], the carrier of (X,Y):]
[: the carrier of (X,Y), the carrier of (X,Y):] is non empty Relation-like set
[:[: the carrier of (X,Y), the carrier of (X,Y):], the carrier of (X,Y):] is non empty Relation-like set
bool [:[: the carrier of (X,Y), the carrier of (X,Y):], the carrier of (X,Y):] is non empty set
K584( the carrier of (X,Y), the addF of (X,Y),(vseq . n),(- (vseq . m))) is Element of the carrier of (X,Y)
[(vseq . n),(- (vseq . m))] is set
{(vseq . n),(- (vseq . m))} is set
{(vseq . n)} is set
{{(vseq . n),(- (vseq . m))},{(vseq . n)}} is set
the addF of (X,Y) . [(vseq . n),(- (vseq . m))] is set
||.((vseq . n) - (vseq . m)).|| is V11() real ext-real non negative Element of REAL
the normF of (X,Y) . ((vseq . n) - (vseq . m)) is V11() real ext-real Element of REAL
||.(vseq . m).|| is V11() real ext-real non negative Element of REAL
the normF of (X,Y) . (vseq . m) is V11() real ext-real Element of REAL
||.(vseq . n).|| - ||.(vseq . m).|| is V11() real ext-real Element of REAL
abs (||.(vseq . n).|| - ||.(vseq . m).||) is V11() real ext-real Element of REAL
||.vseq.|| . m is V11() real ext-real Element of REAL
(||.vseq.|| . n) - (||.vseq.|| . m) is V11() real ext-real Element of REAL
abs ((||.vseq.|| . n) - (||.vseq.|| . m)) is V11() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V115() V116() V117() V118() V119() V120() V145() V168() Element of NAT
||.vseq.|| . n is V11() real ext-real Element of REAL
(||.vseq.|| . n) - (||.vseq.|| . m) is V11() real ext-real Element of REAL
abs ((||.vseq.|| . n) - (||.vseq.|| . m)) is V11() real ext-real Element of REAL
tseq is non empty Relation-like X -defined the carrier of Y -valued Function-like V23(X) quasi_total Element of bool [:X, the carrier of Y:]
lim ||.vseq.|| is V11() real ext-real Element of REAL
tseq is Element of X
tseq . tseq is Element of the carrier of Y
tv is non empty Relation-like NAT -defined the carrier of Y -valued Function-like V23( NAT ) quasi_total Element of bool [:NAT, the carrier of Y:]
lim tv is Element of the carrier of Y
e is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V115() V116() V117() V118() V119() V120() V145() V168() Element of NAT
tv . e is Element of the carrier of Y
||.(tv . e).|| is V11() real ext-real non negative Element of REAL
the normF of Y is non empty Relation-like the carrier of Y -defined REAL -valued Function-like V23( the carrier of Y) quasi_total V105() V106() V107() Element of bool [: the carrier of Y,REAL:]
[: the carrier of Y,REAL:] is non empty Relation-like V105() V106() V107() set
bool [: the carrier of Y,REAL:] is non empty set
the normF of Y . (tv . e) is V11() real ext-real Element of REAL
vseq . e is Element of the carrier of (X,Y)
||.(vseq . e).|| is V11() real ext-real non negative Element of REAL
the normF of (X,Y) . (vseq . e) is V11() real ext-real Element of REAL
(X,Y,(vseq . e)) is non empty Relation-like X -defined the carrier of Y -valued Function-like V23(X) quasi_total (X,Y) Element of bool [:X, the carrier of Y:]
(X,Y,(vseq . e)) . tseq is Element of the carrier of Y
||.tv.|| 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 epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V115() V116() V117() V118() V119() V120() V145() V168() Element of NAT
||.tv.|| . e is V11() real ext-real Element of REAL
||.vseq.|| . e is V11() real ext-real Element of REAL
tv . e is Element of the carrier of Y
||.(tv . e).|| is V11() real ext-real non negative Element of REAL
the normF of Y is non empty Relation-like the carrier of Y -defined REAL -valued Function-like V23( the carrier of Y) quasi_total V105() V106() V107() Element of bool [: the carrier of Y,REAL:]
[: the carrier of Y,REAL:] is non empty Relation-like V105() V106() V107() set
bool [: the carrier of Y,REAL:] is non empty set
the normF of Y . (tv . e) is V11() real ext-real Element of REAL
vseq . e is Element of the carrier of (X,Y)
||.(vseq . e).|| is V11() real ext-real non negative Element of REAL
the normF of (X,Y) . (vseq . e) is V11() real ext-real Element of REAL
||.(tseq . tseq).|| is V11() real ext-real non negative Element of REAL
the normF of Y is non empty Relation-like the carrier of Y -defined REAL -valued Function-like V23( the carrier of Y) quasi_total V105() V106() V107() Element of bool [: the carrier of Y,REAL:]
[: the carrier of Y,REAL:] is non empty Relation-like V105() V106() V107() set
bool [: the carrier of Y,REAL:] is non empty set
the normF of Y . (tseq . tseq) is V11() real ext-real Element of REAL
lim ||.tv.|| 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
vseq . tseq is Element of the carrier of (X,Y)
||.(vseq . tseq).|| is V11() real ext-real non negative Element of REAL
the normF of (X,Y) . (vseq . tseq) is V11() real ext-real Element of REAL
||.vseq.|| . tseq is V11() real ext-real Element of REAL
tseq is Element of X
tseq . tseq is Element of the carrier of Y
||.(tseq . tseq).|| is V11() real ext-real non negative Element of REAL
the normF of Y . (tseq . tseq) is V11() real ext-real Element of REAL
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
e is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V115() V116() V117() V118() V119() V120() V145() V168() Element of NAT
m is Element of X
tseq . m is Element of the carrier of Y
n is non empty Relation-like NAT -defined the carrier of Y -valued Function-like V23( NAT ) quasi_total Element of bool [:NAT, the carrier of Y:]
lim n is Element of the carrier of Y
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V115() V116() V117() V118() V119() V120() V145() V168() Element of NAT
n . n is Element of the carrier of Y
h1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V115() V116() V117() V118() V119() V120() V145() V168() Element of NAT
n . h1 is Element of the carrier of Y
(n . n) - (n . h1) is Element of the carrier of Y
- (n . h1) is Element of the carrier of Y
(n . n) + (- (n . h1)) is Element of the carrier of Y
the addF of Y is non empty Relation-like [: the carrier of Y, the carrier of Y:] -defined the carrier of Y -valued Function-like V23([: the carrier of Y, the carrier of Y:]) quasi_total Element of bool [:[: the carrier of Y, the carrier of Y:], the carrier of Y:]
[: the carrier of Y, the carrier of Y:] is non empty Relation-like set
[:[: the carrier of Y, the carrier of Y:], the carrier of Y:] is non empty Relation-like set
bool [:[: the carrier of Y, the carrier of Y:], the carrier of Y:] is non empty set
K584( the carrier of Y, the addF of Y,(n . n),(- (n . h1))) is Element of the carrier of Y
[(n . n),(- (n . h1))] is set
{(n . n),(- (n . h1))} is set
{(n . n)} is set
{{(n . n),(- (n . h1))},{(n . n)}} is set
the addF of Y . [(n . n),(- (n . h1))] is set
||.((n . n) - (n . h1)).|| is V11() real ext-real non negative Element of REAL
the normF of Y is non empty Relation-like the carrier of Y -defined REAL -valued Function-like V23( the carrier of Y) quasi_total V105() V106() V107() Element of bool [: the carrier of Y,REAL:]
[: the carrier of Y,REAL:] is non empty Relation-like V105() V106() V107() set
bool [: the carrier of Y,REAL:] is non empty set
the normF of Y . ((n . n) - (n . h1)) is V11() real ext-real Element of REAL
vseq . n is Element of the carrier of (X,Y)
vseq . h1 is Element of the carrier of (X,Y)
(vseq . n) - (vseq . h1) is Element of the carrier of (X,Y)
- (vseq . h1) is Element of the carrier of (X,Y)
(vseq . n) + (- (vseq . h1)) is Element of the carrier of (X,Y)
K584( the carrier of (X,Y), the addF of (X,Y),(vseq . n),(- (vseq . h1))) is Element of the carrier of (X,Y)
[(vseq . n),(- (vseq . h1))] is set
{(vseq . n),(- (vseq . h1))} is set
{(vseq . n)} is set
{{(vseq . n),(- (vseq . h1))},{(vseq . n)}} is set
the addF of (X,Y) . [(vseq . n),(- (vseq . h1))] is set
||.((vseq . n) - (vseq . h1)).|| is V11() real ext-real non negative Element of REAL
the normF of (X,Y) . ((vseq . n) - (vseq . h1)) is V11() real ext-real Element of REAL
(X,Y,(vseq . h1)) is non empty Relation-like X -defined the carrier of Y -valued Function-like V23(X) quasi_total (X,Y) Element of bool [:X, the carrier of Y:]
(X,Y,(vseq . n)) is non empty Relation-like X -defined the carrier of Y -valued Function-like V23(X) quasi_total (X,Y) Element of bool [:X, the carrier of Y:]
(X,Y,(vseq . n)) . m is Element of the carrier of Y
(X,Y,(vseq . h1)) . m is Element of the carrier of Y
f1 is non empty Relation-like X -defined the carrier of Y -valued Function-like V23(X) quasi_total (X,Y) Element of bool [:X, the carrier of Y:]
f1 . m is Element of the carrier of Y
n . e is Element of the carrier of Y
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V115() V116() V117() V118() V119() V120() V145() V168() Element of NAT
n . n is Element of the carrier of Y
(n . e) - (n . n) is Element of the carrier of Y
- (n . n) is Element of the carrier of Y
(n . e) + (- (n . n)) is Element of the carrier of Y
the addF of Y is non empty Relation-like [: the carrier of Y, the carrier of Y:] -defined the carrier of Y -valued Function-like V23([: the carrier of Y, the carrier of Y:]) quasi_total Element of bool [:[: the carrier of Y, the carrier of Y:], the carrier of Y:]
[: the carrier of Y, the carrier of Y:] is non empty Relation-like set
[:[: the carrier of Y, the carrier of Y:], the carrier of Y:] is non empty Relation-like set
bool [:[: the carrier of Y, the carrier of Y:], the carrier of Y:] is non empty set
K584( the carrier of Y, the addF of Y,(n . e),(- (n . n))) is Element of the carrier of Y
[(n . e),(- (n . n))] is set
{(n . e),(- (n . n))} is set
{(n . e)} is set
{{(n . e),(- (n . n))},{(n . e)}} is set
the addF of Y . [(n . e),(- (n . n))] is set
||.((n . e) - (n . n)).|| is V11() real ext-real non negative Element of REAL
the normF of Y is non empty Relation-like the carrier of Y -defined REAL -valued Function-like V23( the carrier of Y) quasi_total V105() V106() V107() Element of bool [: the carrier of Y,REAL:]
[: the carrier of Y,REAL:] is non empty Relation-like V105() V106() V107() set
bool [: the carrier of Y,REAL:] is non empty set
the normF of Y . ((n . e) - (n . n)) is V11() real ext-real Element of REAL
vseq . e is Element of the carrier of (X,Y)
vseq . n is Element of the carrier of (X,Y)
(vseq . e) - (vseq . n) is Element of the carrier of (X,Y)
- (vseq . n) is Element of the carrier of (X,Y)
(vseq . e) + (- (vseq . n)) is Element of the carrier of (X,Y)
K584( the carrier of (X,Y), the addF of (X,Y),(vseq . e),(- (vseq . n))) is Element of the carrier of (X,Y)
[(vseq . e),(- (vseq . n))] is set
{(vseq . e),(- (vseq . n))} is set
{(vseq . e)} is set
{{(vseq . e),(- (vseq . n))},{(vseq . e)}} is set
the addF of (X,Y) . [(vseq . e),(- (vseq . n))] is set
||.((vseq . e) - (vseq . n)).|| is V11() real ext-real non negative Element of REAL
the normF of (X,Y) . ((vseq . e) - (vseq . n)) is V11() real ext-real Element of REAL
(n . e) - (tseq . m) is Element of the carrier of Y
- (tseq . m) is Element of the carrier of Y
(n . e) + (- (tseq . m)) is Element of the carrier of Y
the addF of Y is non empty Relation-like [: the carrier of Y, the carrier of Y:] -defined the carrier of Y -valued Function-like V23([: the carrier of Y, the carrier of Y:]) quasi_total Element of bool [:[: the carrier of Y, the carrier of Y:], the carrier of Y:]
[: the carrier of Y, the carrier of Y:] is non empty Relation-like set
[:[: the carrier of Y, the carrier of Y:], the carrier of Y:] is non empty Relation-like set
bool [:[: the carrier of Y, the carrier of Y:], the carrier of Y:] is non empty set
K584( the carrier of Y, the addF of Y,(n . e),(- (tseq . m))) is Element of the carrier of Y
[(n . e),(- (tseq . m))] is set
{(n . e),(- (tseq . m))} is set
{(n . e)} is set
{{(n . e),(- (tseq . m))},{(n . e)}} is set
the addF of Y . [(n . e),(- (tseq . m))] is set
||.((n . e) - (tseq . m)).|| is V11() real ext-real non negative Element of REAL
the normF of Y is non empty Relation-like the carrier of Y -defined REAL -valued Function-like V23( the carrier of Y) quasi_total V105() V106() V107() Element of bool [: the carrier of Y,REAL:]
[: the carrier of Y,REAL:] is non empty Relation-like V105() V106() V107() set
bool [: the carrier of Y,REAL:] is non empty set
the normF of Y . ((n . e) - (tseq . m)) is V11() real ext-real Element of REAL
n is non empty Relation-like NAT -defined REAL -valued Function-like V23( NAT ) quasi_total V105() V106() V107() Element of bool [:NAT,REAL:]
h1 is set
n . h1 is V11() real ext-real Element of REAL
f1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V115() V116() V117() V118() V119() V120() V145() V168() Element of NAT
n . f1 is Element of the carrier of Y
(n . f1) - (n . e) is Element of the carrier of Y
- (n . e) is Element of the carrier of Y
(n . f1) + (- (n . e)) is Element of the carrier of Y
K584( the carrier of Y, the addF of Y,(n . f1),(- (n . e))) is Element of the carrier of Y
[(n . f1),(- (n . e))] is set
{(n . f1),(- (n . e))} is set
{(n . f1)} is set
{{(n . f1),(- (n . e))},{(n . f1)}} is set
the addF of Y . [(n . f1),(- (n . e))] is set
||.((n . f1) - (n . e)).|| is V11() real ext-real non negative Element of REAL
the normF of Y . ((n . f1) - (n . e)) is V11() real ext-real Element of REAL
n - (n . e) is non empty Relation-like NAT -defined the carrier of Y -valued Function-like V23( NAT ) quasi_total Element of bool [:NAT, the carrier of Y:]
(n - (n . e)) . f1 is Element of the carrier of Y
||.((n - (n . e)) . f1).|| is V11() real ext-real non negative Element of REAL
the normF of Y . ((n - (n . e)) . f1) is V11() real ext-real Element of REAL
||.(n - (n . e)).|| is non empty Relation-like NAT -defined REAL -valued Function-like V23( NAT ) quasi_total V105() V106() V107() Element of bool [:NAT,REAL:]
||.(n - (n . e)).|| . h1 is V11() real ext-real Element of REAL
lim (n - (n . e)) is Element of the carrier of Y
(tseq . m) - (n . e) is Element of the carrier of Y
(tseq . m) + (- (n . e)) is Element of the carrier of Y
K584( the carrier of Y, the addF of Y,(tseq . m),(- (n . e))) is Element of the carrier of Y
[(tseq . m),(- (n . e))] is set
{(tseq . m),(- (n . e))} is set
{(tseq . m)} is set
{{(tseq . m),(- (n . e))},{(tseq . m)}} is set
the addF of Y . [(tseq . m),(- (n . e))] is set
lim n is V11() real ext-real Element of REAL
||.((tseq . m) - (n . e)).|| is V11() real ext-real non negative Element of REAL
the normF of Y . ((tseq . m) - (n . e)) is V11() real ext-real Element of REAL
h1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V115() V116() V117() V118() V119() V120() V145() V168() Element of NAT
n . h1 is V11() real ext-real Element of REAL
n . h1 is Element of the carrier of Y
(n . h1) - (n . e) is Element of the carrier of Y
(n . h1) + (- (n . e)) is Element of the carrier of Y
K584( the carrier of Y, the addF of Y,(n . h1),(- (n . e))) is Element of the carrier of Y
[(n . h1),(- (n . e))] is set
{(n . h1),(- (n . e))} is set
{(n . h1)} is set
{{(n . h1),(- (n . e))},{(n . h1)}} is set
the addF of Y . [(n . h1),(- (n . e))] is set
||.((n . h1) - (n . e)).|| is V11() real ext-real non negative Element of REAL
the normF of Y . ((n . h1) - (n . e)) is V11() real ext-real Element of REAL
(n . e) - (n . h1) is Element of the carrier of Y
- (n . h1) is Element of the carrier of Y
(n . e) + (- (n . h1)) is Element of the carrier of Y
K584( the carrier of Y, the addF of Y,(n . e),(- (n . h1))) is Element of the carrier of Y
[(n . e),(- (n . h1))] is set
{(n . e),(- (n . h1))} is set
{{(n . e),(- (n . h1))},{(n . e)}} is set
the addF of Y . [(n . e),(- (n . h1))] is set
||.((n . e) - (n . h1)).|| is V11() real ext-real non negative Element of REAL
the normF of Y . ((n . e) - (n . h1)) is V11() real ext-real Element of REAL
vseq . e is Element of the carrier of (X,Y)
(X,Y,(vseq . e)) is non empty Relation-like X -defined the carrier of Y -valued Function-like V23(X) quasi_total (X,Y) Element of bool [:X, the carrier of Y:]
(X,Y,(vseq . e)) . m is Element of the carrier of Y
((X,Y,(vseq . e)) . m) - (tseq . m) is Element of the carrier of Y
((X,Y,(vseq . e)) . m) + (- (tseq . m)) is Element of the carrier of Y
K584( the carrier of Y, the addF of Y,((X,Y,(vseq . e)) . m),(- (tseq . m))) is Element of the carrier of Y
[((X,Y,(vseq . e)) . m),(- (tseq . m))] is set
{((X,Y,(vseq . e)) . m),(- (tseq . m))} is set
{((X,Y,(vseq . e)) . m)} is set
{{((X,Y,(vseq . e)) . m),(- (tseq . m))},{((X,Y,(vseq . e)) . m)}} is set
the addF of Y . [((X,Y,(vseq . e)) . m),(- (tseq . m))] is set
||.(((X,Y,(vseq . e)) . m) - (tseq . m)).|| is V11() real ext-real non negative Element of REAL
the normF of Y . (((X,Y,(vseq . e)) . m) - (tseq . m)) is V11() real ext-real Element of REAL
m is Element of X
(X,Y,(vseq . e)) . m is Element of the carrier of Y
tseq . m is Element of the carrier of Y
((X,Y,(vseq . e)) . m) - (tseq . m) is Element of the carrier of Y
- (tseq . m) is Element of the carrier of Y
((X,Y,(vseq . e)) . m) + (- (tseq . m)) is Element of the carrier of Y
K584( the carrier of Y, the addF of Y,((X,Y,(vseq . e)) . m),(- (tseq . m))) is Element of the carrier of Y
[((X,Y,(vseq . e)) . m),(- (tseq . m))] is set
{((X,Y,(vseq . e)) . m),(- (tseq . m))} is set
{((X,Y,(vseq . e)) . m)} is set
{{((X,Y,(vseq . e)) . m),(- (tseq . m))},{((X,Y,(vseq . e)) . m)}} is set
the addF of Y . [((X,Y,(vseq . e)) . m),(- (tseq . m))] is set
||.(((X,Y,(vseq . e)) . m) - (tseq . m)).|| is V11() real ext-real non negative Element of REAL
the normF of Y . (((X,Y,(vseq . e)) . m) - (tseq . m)) is V11() real ext-real Element of REAL
e is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V115() V116() V117() V118() V119() V120() V145() V168() Element of NAT
vseq . e is Element of the carrier of (X,Y)
(X,Y,(vseq . e)) is non empty Relation-like X -defined the carrier of Y -valued Function-like V23(X) quasi_total (X,Y) Element of bool [:X, the carrier of Y:]
m is Element of X
(X,Y,(vseq . e)) . m is Element of the carrier of Y
tseq . m is Element of the carrier of Y
((X,Y,(vseq . e)) . m) - (tseq . m) is Element of the carrier of Y
- (tseq . m) is Element of the carrier of Y
((X,Y,(vseq . e)) . m) + (- (tseq . m)) is Element of the carrier of Y
K584( the carrier of Y, the addF of Y,((X,Y,(vseq . e)) . m),(- (tseq . m))) is Element of the carrier of Y
[((X,Y,(vseq . e)) . m),(- (tseq . m))] is set
{((X,Y,(vseq . e)) . m),(- (tseq . m))} is set
{((X,Y,(vseq . e)) . m)} is set
{{((X,Y,(vseq . e)) . m),(- (tseq . m))},{((X,Y,(vseq . e)) . m)}} is set
the addF of Y . [((X,Y,(vseq . e)) . m),(- (tseq . m))] is set
||.(((X,Y,(vseq . e)) . m) - (tseq . m)).|| is V11() real ext-real non negative Element of REAL
the normF of Y . (((X,Y,(vseq . e)) . m) - (tseq . m)) is V11() real ext-real Element of REAL
tseq is non empty Relation-like X -defined the carrier of Y -valued Function-like V23(X) quasi_total (X,Y) Element of bool [:X, the carrier of Y:]
tv is Element of the carrier of (X,Y)
e is V11() real ext-real Element of REAL
m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V115() V116() V117() V118() V119() V120() V145() V168() Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V115() V116() V117() V118() V119() V120() V145() V168() Element of NAT
vseq . n is Element of the carrier of (X,Y)
(vseq . n) - tv is Element of the carrier of (X,Y)
- tv is Element of the carrier of (X,Y)
(vseq . n) + (- tv) is Element of the carrier of (X,Y)
K584( the carrier of (X,Y), the addF of (X,Y),(vseq . n),(- tv)) is Element of the carrier of (X,Y)
[(vseq . n),(- tv)] is set
{(vseq . n),(- tv)} is set
{(vseq . n)} is set
{{(vseq . n),(- tv)},{(vseq . n)}} is set
the addF of (X,Y) . [(vseq . n),(- tv)] is set
(X,Y,(vseq . n)) is non empty Relation-like X -defined the carrier of Y -valued Function-like V23(X) quasi_total (X,Y) Element of bool [:X, the carrier of Y:]
h1 is non empty Relation-like X -defined the carrier of Y -valued Function-like V23(X) quasi_total (X,Y) Element of bool [:X, the carrier of Y:]
r is Element of X
h1 . r is Element of the carrier of Y
||.(h1 . r).|| is V11() real ext-real non negative Element of REAL
the normF of Y is non empty Relation-like the carrier of Y -defined REAL -valued Function-like V23( the carrier of Y) quasi_total V105() V106() V107() Element of bool [: the carrier of Y,REAL:]
[: the carrier of Y,REAL:] is non empty Relation-like V105() V106() V107() set
bool [: the carrier of Y,REAL:] is non empty set
the normF of Y . (h1 . r) is V11() real ext-real Element of REAL
(X,Y,(vseq . n)) . r is Element of the carrier of Y
tseq . r is Element of the carrier of Y
((X,Y,(vseq . n)) . r) - (tseq . r) is Element of the carrier of Y
- (tseq . r) is Element of the carrier of Y
((X,Y,(vseq . n)) . r) + (- (tseq . r)) is Element of the carrier of Y
the addF of Y is non empty Relation-like [: the carrier of Y, the carrier of Y:] -defined the carrier of Y -valued Function-like V23([: the carrier of Y, the carrier of Y:]) quasi_total Element of bool [:[: the carrier of Y, the carrier of Y:], the carrier of Y:]
[: the carrier of Y, the carrier of Y:] is non empty Relation-like set
[:[: the carrier of Y, the carrier of Y:], the carrier of Y:] is non empty Relation-like set
bool [:[: the carrier of Y, the carrier of Y:], the carrier of Y:] is non empty set
K584( the carrier of Y, the addF of Y,((X,Y,(vseq . n)) . r),(- (tseq . r))) is Element of the carrier of Y
[((X,Y,(vseq . n)) . r),(- (tseq . r))] is set
{((X,Y,(vseq . n)) . r),(- (tseq . r))} is set
{((X,Y,(vseq . n)) . r)} is set
{{((X,Y,(vseq . n)) . r),(- (tseq . r))},{((X,Y,(vseq . n)) . r)}} is set
the addF of Y . [((X,Y,(vseq . n)) . r),(- (tseq . r))] is set
||.(((X,Y,(vseq . n)) . r) - (tseq . r)).|| is V11() real ext-real non negative Element of REAL
the normF of Y . (((X,Y,(vseq . n)) . r) - (tseq . r)) is V11() real ext-real Element of REAL
r is V11() real ext-real Element of REAL
(X,Y,h1) is non empty V115() V116() V117() Element of bool REAL
{ ||.(h1 . b₁).|| where b₁ is Element of X : verum } is set
c₁₅ is Element of X
h1 . c₁₅ is Element of the carrier of Y
||.(h1 . c₁₅).|| is V11() real ext-real non negative Element of REAL
the normF of Y . (h1 . c₁₅) is V11() real ext-real Element of REAL
upper_bound (X,Y,h1) is V11() real ext-real Element of REAL
||.((vseq . n) - tv).|| is V11() real ext-real non negative Element of REAL
the normF of (X,Y) . ((vseq . n) - tv) is V11() real ext-real Element of REAL
r is V11() real ext-real set
e is V11() real ext-real Element of REAL
e / 2 is V11() real ext-real Element of REAL
m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V115() V116() V117() V118() V119() V120() V145() V168() Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V115() V116() V117() V118() V119() V120() V145() V168() Element of NAT
vseq . n is Element of the carrier of (X,Y)
(vseq . n) - tv is Element of the carrier of (X,Y)
- tv is Element of the carrier of (X,Y)
(vseq . n) + (- tv) is Element of the carrier of (X,Y)
K584( the carrier of (X,Y), the addF of (X,Y),(vseq . n),(- tv)) is Element of the carrier of (X,Y)
[(vseq . n),(- tv)] is set
{(vseq . n),(- tv)} is set
{(vseq . n)} is set
{{(vseq . n),(- tv)},{(vseq . n)}} is set
the addF of (X,Y) . [(vseq . n),(- tv)] is set
||.((vseq . n) - tv).|| is V11() real ext-real non negative Element of REAL
the normF of (X,Y) . ((vseq . n) - tv) is V11() real ext-real Element of REAL
X is non empty set
Y is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like complete NORMSTR
(X,Y) is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like NORMSTR
(X,Y) is non empty Element of bool the carrier of (RealVectSpace (X,Y))
RealVectSpace (X,Y) is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() RLSStruct
the carrier of (RealVectSpace (X,Y)) is non empty set
bool the carrier of (RealVectSpace (X,Y)) is non empty set
Zero_ ((X,Y),(RealVectSpace (X,Y))) is Element of (X,Y)
Add_ ((X,Y),(RealVectSpace (X,Y))) is non empty Relation-like [:(X,Y),(X,Y):] -defined (X,Y) -valued Function-like V23([:(X,Y),(X,Y):]) quasi_total Element of bool [:[:(X,Y),(X,Y):],(X,Y):]
[:(X,Y),(X,Y):] is non empty Relation-like set
[:[:(X,Y),(X,Y):],(X,Y):] is non empty Relation-like set
bool [:[:(X,Y),(X,Y):],(X,Y):] is non empty set
Mult_ ((X,Y),(RealVectSpace (X,Y))) is non empty Relation-like [:REAL,(X,Y):] -defined (X,Y) -valued Function-like V23([:REAL,(X,Y):]) quasi_total Element of bool [:[:REAL,(X,Y):],(X,Y):]
[:REAL,(X,Y):] is non empty Relation-like set
[:[:REAL,(X,Y):],(X,Y):] is non empty Relation-like set
bool [:[:REAL,(X,Y):],(X,Y):] is non empty set
(X,Y) is non empty Relation-like (X,Y) -defined REAL -valued Function-like V23((X,Y)) quasi_total V105() V106() V107() Element of bool [:(X,Y),REAL:]
[:(X,Y),REAL:] is non empty Relation-like V105() V106() V107() set
bool [:(X,Y),REAL:] is non empty set
NORMSTR(# (X,Y),(Zero_ ((X,Y),(RealVectSpace (X,Y)))),(Add_ ((X,Y),(RealVectSpace (X,Y)))),(Mult_ ((X,Y),(RealVectSpace (X,Y)))),(X,Y) #) is non empty strict NORMSTR
the carrier of (X,Y) is non empty set
[:NAT, the carrier of (X,Y):] is non empty Relation-like set
bool [:NAT, the carrier of (X,Y):] is non empty set
vseq is non empty Relation-like NAT -defined the carrier of (X,Y) -valued Function-like V23( NAT ) quasi_total Element of bool [:NAT, the carrier of (X,Y):]
X is non empty set
Y is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like complete NORMSTR
(X,Y) is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() discerning reflexive RealNormSpace-like NORMSTR
(X,Y) is non empty Element of bool the carrier of (RealVectSpace (X,Y))
RealVectSpace (X,Y) is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V100() RLSStruct
the carrier of (RealVectSpace (X,Y)) is non empty set
bool the carrier of (RealVectSpace (X,Y)) is non empty set
Zero_ ((X,Y),(RealVectSpace (X,Y))) is Element of (X,Y)
Add_ ((X,Y),(RealVectSpace (X,Y))) is non empty Relation-like [:(X,Y),(X,Y):] -defined (X,Y) -valued Function-like V23([:(X,Y),(X,Y):]) quasi_total Element of bool [:[:(X,Y),(X,Y):],(X,Y):]
[:(X,Y),(X,Y):] is non empty Relation-like set
[:[:(X,Y),(X,Y):],(X,Y):] is non empty Relation-like set
bool [:[:(X,Y),(X,Y):],(X,Y):] is non empty set
Mult_ ((X,Y),(RealVectSpace (X,Y))) is non empty Relation-like [:REAL,(X,Y):] -defined (X,Y) -valued Function-like V23([:REAL,(X,Y):]) quasi_total Element of bool [:[:REAL,(X,Y):],(X,Y):]
[:REAL,(X,Y):] is non empty Relation-like set
[:[:REAL,(X,Y):],(X,Y):] is non empty Relation-like set
bool [:[:REAL,(X,Y):],(X,Y):] is non empty set
(X,Y) is non empty Relation-like (X,Y) -defined REAL -valued Function-like V23((X,Y)) quasi_total V105() V106() V107() Element of bool [:(X,Y),REAL:]
[:(X,Y),REAL:] is non empty Relation-like V105() V106() V107() set
bool [:(X,Y),REAL:] is non empty set
NORMSTR(# (X,Y),(Zero_ ((X,Y),(RealVectSpace (X,Y)))),(Add_ ((X,Y),(RealVectSpace (X,Y)))),(Mult_ ((X,Y),(RealVectSpace (X,Y)))),(X,Y) #) is non empty strict NORMSTR