REAL is non empty V49() V158() V159() V160() V164() set
NAT is non empty epsilon-transitive epsilon-connected ordinal V49() V54() V55() V158() V159() V160() V161() V162() V163() V164() Element of bool REAL
bool REAL is V49() set
COMPLEX is non empty V49() V158() V164() set
RAT is non empty V49() V158() V159() V160() V161() V164() set
INT is non empty V49() V158() V159() V160() V161() V162() V164() set
[:COMPLEX,COMPLEX:] is complex-yielding V49() set
bool [:COMPLEX,COMPLEX:] is V49() set
[:[:COMPLEX,COMPLEX:],COMPLEX:] is complex-yielding V49() set
bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is V49() set
[:REAL,REAL:] is complex-yielding V36() V37() V49() set
bool [:REAL,REAL:] is V49() set
[:[:REAL,REAL:],REAL:] is complex-yielding V36() V37() V49() set
bool [:[:REAL,REAL:],REAL:] is V49() set
[:RAT,RAT:] is RAT -valued complex-yielding V36() V37() V49() set
bool [:RAT,RAT:] is V49() set
[:[:RAT,RAT:],RAT:] is RAT -valued complex-yielding V36() V37() V49() set
bool [:[:RAT,RAT:],RAT:] is V49() set
[:INT,INT:] is RAT -valued INT -valued complex-yielding V36() V37() V49() set
bool [:INT,INT:] is V49() set
[:[:INT,INT:],INT:] is RAT -valued INT -valued complex-yielding V36() V37() V49() set
bool [:[:INT,INT:],INT:] is V49() set
[:NAT,NAT:] is RAT -valued INT -valued complex-yielding V36() V37() V38() V49() set
[:[:NAT,NAT:],NAT:] is RAT -valued INT -valued complex-yielding V36() V37() V38() V49() set
bool [:[:NAT,NAT:],NAT:] is V49() set
omega is non empty epsilon-transitive epsilon-connected ordinal V49() V54() V55() V158() V159() V160() V161() V162() V163() V164() set
bool omega is V49() set
bool NAT is V49() set
2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V33() V34() V49() V54() V158() V159() V160() V161() V162() V163() Element of NAT
[:2,2:] is RAT -valued INT -valued complex-yielding V36() V37() V38() set
[:[:2,2:],2:] is RAT -valued INT -valued complex-yielding V36() V37() V38() set
bool [:[:2,2:],2:] is set
[:NAT,REAL:] is complex-yielding V36() V37() V49() set
bool [:NAT,REAL:] is V49() set
K356() is non empty set
[:K356(),K356():] is set
[:[:K356(),K356():],K356():] is set
bool [:[:K356(),K356():],K356():] is set
[:REAL,K356():] is V49() set
[:[:REAL,K356():],K356():] is V49() set
bool [:[:REAL,K356():],K356():] is V49() set
K362() is RLSStruct
the carrier of K362() is set
bool the carrier of K362() is set
K366() is Element of bool the carrier of K362()
[:K366(),K366():] is set
[:[:K366(),K366():],REAL:] is complex-yielding V36() V37() set
bool [:[:K366(),K366():],REAL:] is set
the_set_of_l1RealSequences is non empty Element of bool the carrier of K362()
[:the_set_of_l1RealSequences,REAL:] is complex-yielding V36() V37() V49() set
bool [:the_set_of_l1RealSequences,REAL:] is V49() set
1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V33() V34() V49() V54() V158() V159() V160() V161() V162() V163() Element of NAT
[:1,1:] is RAT -valued INT -valued complex-yielding V36() V37() V38() set
bool [:1,1:] is set
[:[:1,1:],1:] is RAT -valued INT -valued complex-yielding V36() V37() V38() set
bool [:[:1,1:],1:] is set
[:[:1,1:],REAL:] is complex-yielding V36() V37() set
bool [:[:1,1:],REAL:] is set
[:[:2,2:],REAL:] is complex-yielding V36() V37() set
bool [:[:2,2:],REAL:] is set
TOP-REAL 2 is non empty non trivial right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital TopSpace-like V200() L20()
the carrier of (TOP-REAL 2) is non empty non trivial set
{} is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative Function-like functional V49() V54() V56( {} ) FinSequence-membered V158() V159() V160() V161() V162() V163() V164() set
0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative Function-like functional V33() V34() V49() V54() V56( {} ) FinSequence-membered V158() V159() V160() V161() V162() V163() V164() Element of NAT
3 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V33() V34() V49() V54() V158() V159() V160() V161() V162() V163() Element of NAT
- 1 is V11() real ext-real non positive Element of REAL
multreal is Relation-like [:REAL,REAL:] -defined REAL -valued Function-like V26([:REAL,REAL:]) V30([:REAL,REAL:], REAL ) complex-yielding V36() V37() Element of bool [:[:REAL,REAL:],REAL:]
<*> REAL is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative Relation-like NAT -defined REAL -valued Function-like one-to-one constant functional complex-yielding V36() V37() V38() V47() V48() V49() V54() V56( {} ) FinSequence-like FinSubsequence-like FinSequence-membered V158() V159() V160() V161() V162() V163() V164() FinSequence of REAL
Sum (<*> REAL) is V11() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V49() V54() set
REAL n is non empty functional FinSequence-membered FinSequenceSet of REAL
[:(REAL n),(REAL n):] is set
[:[:(REAL n),(REAL n):],(REAL n):] is set
bool [:[:(REAL n),(REAL n):],(REAL n):] is set
seq is Relation-like [:(REAL n),(REAL n):] -defined REAL n -valued Function-like V26([:(REAL n),(REAL n):]) V30([:(REAL n),(REAL n):], REAL n) V47() V48() Element of bool [:[:(REAL n),(REAL n):],(REAL n):]
n -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
seq9 is Relation-like NAT -defined REAL -valued Function-like complex-yielding V36() V37() V49() V56(n) FinSequence-like FinSubsequence-like Element of REAL n
r is Relation-like NAT -defined REAL -valued Function-like complex-yielding V36() V37() V49() V56(n) FinSequence-like FinSubsequence-like Element of REAL n
k is Relation-like NAT -defined REAL -valued Function-like complex-yielding V36() V37() V49() V56(n) FinSequence-like FinSubsequence-like Element of REAL n
seq . (r,k) is Relation-like NAT -defined Function-like V49() V56(n) FinSequence-like FinSubsequence-like Element of REAL n
[r,k] is set
seq . [r,k] is Relation-like NAT -defined Function-like V49() FinSequence-like FinSubsequence-like set
seq . (seq9,(seq . (r,k))) is Relation-like NAT -defined Function-like V49() V56(n) FinSequence-like FinSubsequence-like Element of REAL n
[seq9,(seq . (r,k))] is set
seq . [seq9,(seq . (r,k))] is Relation-like NAT -defined Function-like V49() FinSequence-like FinSubsequence-like set
seq9 + (seq . (r,k)) is Relation-like NAT -defined REAL -valued Function-like complex-yielding V36() V37() V49() V56(n) FinSequence-like FinSubsequence-like Element of REAL n
r + k is Relation-like NAT -defined REAL -valued Function-like complex-yielding V36() V37() V49() V56(n) FinSequence-like FinSubsequence-like Element of REAL n
seq9 + (r + k) is Relation-like NAT -defined REAL -valued Function-like complex-yielding V36() V37() V49() V56(n) FinSequence-like FinSubsequence-like Element of REAL n
m1 is Relation-like NAT -defined REAL -valued Function-like complex-yielding V36() V37() V49() V56(n) FinSequence-like FinSubsequence-like Element of n -tuples_on REAL
m2 is Relation-like NAT -defined REAL -valued Function-like complex-yielding V36() V37() V49() V56(n) FinSequence-like FinSubsequence-like Element of n -tuples_on REAL
m1 + m2 is Relation-like NAT -defined REAL -valued Function-like complex-yielding V36() V37() V49() V56(n) FinSequence-like FinSubsequence-like Element of n -tuples_on REAL
p is Relation-like NAT -defined REAL -valued Function-like complex-yielding V36() V37() V49() V56(n) FinSequence-like FinSubsequence-like Element of n -tuples_on REAL
(m1 + m2) + p is Relation-like NAT -defined REAL -valued Function-like complex-yielding V36() V37() V49() V56(n) FinSequence-like FinSubsequence-like Element of n -tuples_on REAL
seq . (seq9,r) is Relation-like NAT -defined Function-like V49() V56(n) FinSequence-like FinSubsequence-like Element of REAL n
[seq9,r] is set
seq . [seq9,r] is Relation-like NAT -defined Function-like V49() FinSequence-like FinSubsequence-like set
(seq . (seq9,r)) + k is Relation-like NAT -defined REAL -valued Function-like complex-yielding V36() V37() V49() V56(n) FinSequence-like FinSubsequence-like Element of REAL n
seq . ((seq . (seq9,r)),k) is Relation-like NAT -defined Function-like V49() V56(n) FinSequence-like FinSubsequence-like Element of REAL n
[(seq . (seq9,r)),k] is set
seq . [(seq . (seq9,r)),k] is Relation-like NAT -defined Function-like V49() FinSequence-like FinSubsequence-like set
seq9 is Relation-like NAT -defined REAL -valued Function-like complex-yielding V36() V37() V49() V56(n) FinSequence-like FinSubsequence-like Element of REAL n
r is Relation-like NAT -defined REAL -valued Function-like complex-yielding V36() V37() V49() V56(n) FinSequence-like FinSubsequence-like Element of REAL n
seq . (seq9,r) is Relation-like NAT -defined Function-like V49() V56(n) FinSequence-like FinSubsequence-like Element of REAL n
[seq9,r] is set
seq . [seq9,r] is Relation-like NAT -defined Function-like V49() FinSequence-like FinSubsequence-like set
seq9 + r is Relation-like NAT -defined REAL -valued Function-like complex-yielding V36() V37() V49() V56(n) FinSequence-like FinSubsequence-like Element of REAL n
seq . (r,seq9) is Relation-like NAT -defined Function-like V49() V56(n) FinSequence-like FinSubsequence-like Element of REAL n
[r,seq9] is set
seq . [r,seq9] is Relation-like NAT -defined Function-like V49() FinSequence-like FinSubsequence-like set
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V49() V54() set
REAL n is non empty functional FinSequence-membered FinSequenceSet of REAL
[:(REAL n),(REAL n):] is set
[:[:(REAL n),(REAL n):],(REAL n):] is set
bool [:[:(REAL n),(REAL n):],(REAL n):] is set
seq is Relation-like [:(REAL n),(REAL n):] -defined REAL n -valued Function-like V26([:(REAL n),(REAL n):]) V30([:(REAL n),(REAL n):], REAL n) V47() V48() Element of bool [:[:(REAL n),(REAL n):],(REAL n):]
seq9 is Relation-like NAT -defined REAL -valued Function-like complex-yielding V36() V37() V49() V56(n) FinSequence-like FinSubsequence-like Element of REAL n
r is Relation-like NAT -defined REAL -valued Function-like complex-yielding V36() V37() V49() V56(n) FinSequence-like FinSubsequence-like Element of REAL n
seq . (seq9,r) is Relation-like NAT -defined Function-like V49() V56(n) FinSequence-like FinSubsequence-like Element of REAL n
[seq9,r] is set
seq . [seq9,r] is Relation-like NAT -defined Function-like V49() FinSequence-like FinSubsequence-like set
seq9 + r is Relation-like NAT -defined REAL -valued Function-like complex-yielding V36() V37() V49() V56(n) FinSequence-like FinSubsequence-like Element of REAL n
seq is Relation-like [:(REAL n),(REAL n):] -defined REAL n -valued Function-like V26([:(REAL n),(REAL n):]) V30([:(REAL n),(REAL n):], REAL n) V47() V48() Element of bool [:[:(REAL n),(REAL n):],(REAL n):]
seq9 is Relation-like [:(REAL n),(REAL n):] -defined REAL n -valued Function-like V26([:(REAL n),(REAL n):]) V30([:(REAL n),(REAL n):], REAL n) V47() V48() Element of bool [:[:(REAL n),(REAL n):],(REAL n):]
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V49() V54() set
REAL n is non empty functional FinSequence-membered FinSequenceSet of REAL
(n) is Relation-like [:(REAL n),(REAL n):] -defined REAL n -valued Function-like V26([:(REAL n),(REAL n):]) V30([:(REAL n),(REAL n):], REAL n) V47() V48() Element of bool [:[:(REAL n),(REAL n):],(REAL n):]
[:(REAL n),(REAL n):] is set
[:[:(REAL n),(REAL n):],(REAL n):] is set
bool [:[:(REAL n),(REAL n):],(REAL n):] is set
seq is Relation-like [:(REAL n),(REAL n):] -defined REAL n -valued Function-like V26([:(REAL n),(REAL n):]) V30([:(REAL n),(REAL n):], REAL n) V47() V48() Element of bool [:[:(REAL n),(REAL n):],(REAL n):]
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V49() V54() set
REAL n is non empty functional FinSequence-membered FinSequenceSet of REAL
[:REAL,(REAL n):] is V49() set
[:[:REAL,(REAL n):],(REAL n):] is V49() set
bool [:[:REAL,(REAL n):],(REAL n):] is V49() set
seq is Relation-like [:REAL,(REAL n):] -defined REAL n -valued Function-like V26([:REAL,(REAL n):]) V30([:REAL,(REAL n):], REAL n) V47() V48() Element of bool [:[:REAL,(REAL n):],(REAL n):]
seq is Relation-like [:REAL,(REAL n):] -defined REAL n -valued Function-like V26([:REAL,(REAL n):]) V30([:REAL,(REAL n):], REAL n) V47() V48() Element of bool [:[:REAL,(REAL n):],(REAL n):]
seq9 is Relation-like [:REAL,(REAL n):] -defined REAL n -valued Function-like V26([:REAL,(REAL n):]) V30([:REAL,(REAL n):], REAL n) V47() V48() Element of bool [:[:REAL,(REAL n):],(REAL n):]
r is V11() real ext-real Element of REAL
k is Relation-like NAT -defined REAL -valued Function-like complex-yielding V36() V37() V49() V56(n) FinSequence-like FinSubsequence-like Element of REAL n
seq . (r,k) is Relation-like NAT -defined Function-like V49() V56(n) FinSequence-like FinSubsequence-like Element of REAL n
[r,k] is set
seq . [r,k] is Relation-like NAT -defined Function-like V49() FinSequence-like FinSubsequence-like set
seq9 . (r,k) is Relation-like NAT -defined Function-like V49() V56(n) FinSequence-like FinSubsequence-like Element of REAL n
seq9 . [r,k] is Relation-like NAT -defined Function-like V49() FinSequence-like FinSubsequence-like set
r * k is Relation-like NAT -defined REAL -valued Function-like complex-yielding V36() V37() V49() V56(n) FinSequence-like FinSubsequence-like Element of REAL n
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V49() V54() set
REAL n is non empty functional FinSequence-membered FinSequenceSet of REAL
[:(REAL n),REAL:] is complex-yielding V36() V37() V49() set
bool [:(REAL n),REAL:] is V49() set
seq is non empty Relation-like REAL n -defined REAL -valued Function-like V26( REAL n) V30( REAL n, REAL ) complex-yielding V36() V37() Element of bool [:(REAL n),REAL:]
seq9 is Relation-like NAT -defined REAL -valued Function-like complex-yielding V36() V37() V49() V56(n) FinSequence-like FinSubsequence-like Element of REAL n
seq . seq9 is V11() real ext-real Element of REAL
|.seq9.| is V11() real ext-real non negative Element of REAL
seq is non empty Relation-like REAL n -defined REAL -valued Function-like V26( REAL n) V30( REAL n, REAL ) complex-yielding V36() V37() Element of bool [:(REAL n),REAL:]
seq9 is non empty Relation-like REAL n -defined REAL -valued Function-like V26( REAL n) V30( REAL n, REAL ) complex-yielding V36() V37() Element of bool [:(REAL n),REAL:]
r is Relation-like NAT -defined REAL -valued Function-like complex-yielding V36() V37() V49() V56(n) FinSequence-like FinSubsequence-like Element of REAL n
seq . r is V11() real ext-real Element of REAL
|.r.| is V11() real ext-real non negative Element of REAL
seq9 . r is V11() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V49() V54() set
REAL n is non empty functional FinSequence-membered FinSequenceSet of REAL
0* n is Relation-like NAT -defined REAL -valued Function-like complex-yielding V36() V37() V49() V56(n) FinSequence-like FinSubsequence-like Element of REAL n
[:(REAL n),(REAL n):] is set
(n) is Relation-like [:(REAL n),(REAL n):] -defined REAL n -valued Function-like V26([:(REAL n),(REAL n):]) V30([:(REAL n),(REAL n):], REAL n) V47() V48() commutative associative Element of bool [:[:(REAL n),(REAL n):],(REAL n):]
[:[:(REAL n),(REAL n):],(REAL n):] is set
bool [:[:(REAL n),(REAL n):],(REAL n):] is set
[:REAL,(REAL n):] is V49() set
(n) is Relation-like [:REAL,(REAL n):] -defined REAL n -valued Function-like V26([:REAL,(REAL n):]) V30([:REAL,(REAL n):], REAL n) V47() V48() Element of bool [:[:REAL,(REAL n):],(REAL n):]
[:[:REAL,(REAL n):],(REAL n):] is V49() set
bool [:[:REAL,(REAL n):],(REAL n):] is V49() set
(n) is non empty Relation-like REAL n -defined REAL -valued Function-like V26( REAL n) V30( REAL n, REAL ) complex-yielding V36() V37() Element of bool [:(REAL n),REAL:]
[:(REAL n),REAL:] is complex-yielding V36() V37() V49() set
bool [:(REAL n),REAL:] is V49() set
NORMSTR(# (REAL n),(0* n),(n),(n),(n) #) is non empty strict NORMSTR
the carrier of NORMSTR(# (REAL n),(0* n),(n),(n),(n) #) is non empty set
0. NORMSTR(# (REAL n),(0* n),(n),(n),(n) #) is V69( NORMSTR(# (REAL n),(0* n),(n),(n),(n) #)) Element of the carrier of NORMSTR(# (REAL n),(0* n),(n),(n),(n) #)
the ZeroF of NORMSTR(# (REAL n),(0* n),(n),(n),(n) #) is Element of the carrier of NORMSTR(# (REAL n),(0* n),(n),(n),(n) #)
[: the carrier of NORMSTR(# (REAL n),(0* n),(n),(n),(n) #), the carrier of NORMSTR(# (REAL n),(0* n),(n),(n),(n) #):] is set
the addF of NORMSTR(# (REAL n),(0* n),(n),(n),(n) #) is Relation-like [: the carrier of NORMSTR(# (REAL n),(0* n),(n),(n),(n) #), the carrier of NORMSTR(# (REAL n),(0* n),(n),(n),(n) #):] -defined the carrier of NORMSTR(# (REAL n),(0* n),(n),(n),(n) #) -valued Function-like V26([: the carrier of NORMSTR(# (REAL n),(0* n),(n),(n),(n) #), the carrier of NORMSTR(# (REAL n),(0* n),(n),(n),(n) #):]) V30([: the carrier of NORMSTR(# (REAL n),(0* n),(n),(n),(n) #), the carrier of NORMSTR(# (REAL n),(0* n),(n),(n),(n) #):], the carrier of NORMSTR(# (REAL n),(0* n),(n),(n),(n) #)) Element of bool [:[: the carrier of NORMSTR(# (REAL n),(0* n),(n),(n),(n) #), the carrier of NORMSTR(# (REAL n),(0* n),(n),(n),(n) #):], the carrier of NORMSTR(# (REAL n),(0* n),(n),(n),(n) #):]
[:[: the carrier of NORMSTR(# (REAL n),(0* n),(n),(n),(n) #), the carrier of NORMSTR(# (REAL n),(0* n),(n),(n),(n) #):], the carrier of NORMSTR(# (REAL n),(0* n),(n),(n),(n) #):] is set
bool [:[: the carrier of NORMSTR(# (REAL n),(0* n),(n),(n),(n) #), the carrier of NORMSTR(# (REAL n),(0* n),(n),(n),(n) #):], the carrier of NORMSTR(# (REAL n),(0* n),(n),(n),(n) #):] is set
[:REAL, the carrier of NORMSTR(# (REAL n),(0* n),(n),(n),(n) #):] is V49() set
the Mult of NORMSTR(# (REAL n),(0* n),(n),(n),(n) #) is Relation-like [:REAL, the carrier of NORMSTR(# (REAL n),(0* n),(n),(n),(n) #):] -defined the carrier of NORMSTR(# (REAL n),(0* n),(n),(n),(n) #) -valued Function-like V26([:REAL, the carrier of NORMSTR(# (REAL n),(0* n),(n),(n),(n) #):]) V30([:REAL, the carrier of NORMSTR(# (REAL n),(0* n),(n),(n),(n) #):], the carrier of NORMSTR(# (REAL n),(0* n),(n),(n),(n) #)) Element of bool [:[:REAL, the carrier of NORMSTR(# (REAL n),(0* n),(n),(n),(n) #):], the carrier of NORMSTR(# (REAL n),(0* n),(n),(n),(n) #):]
[:[:REAL, the carrier of NORMSTR(# (REAL n),(0* n),(n),(n),(n) #):], the carrier of NORMSTR(# (REAL n),(0* n),(n),(n),(n) #):] is V49() set
bool [:[:REAL, the carrier of NORMSTR(# (REAL n),(0* n),(n),(n),(n) #):], the carrier of NORMSTR(# (REAL n),(0* n),(n),(n),(n) #):] is V49() set
the normF of NORMSTR(# (REAL n),(0* n),(n),(n),(n) #) is non empty Relation-like the carrier of NORMSTR(# (REAL n),(0* n),(n),(n),(n) #) -defined REAL -valued Function-like V26( the carrier of NORMSTR(# (REAL n),(0* n),(n),(n),(n) #)) V30( the carrier of NORMSTR(# (REAL n),(0* n),(n),(n),(n) #), REAL ) complex-yielding V36() V37() Element of bool [: the carrier of NORMSTR(# (REAL n),(0* n),(n),(n),(n) #),REAL:]
[: the carrier of NORMSTR(# (REAL n),(0* n),(n),(n),(n) #),REAL:] is complex-yielding V36() V37() V49() set
bool [: the carrier of NORMSTR(# (REAL n),(0* n),(n),(n),(n) #),REAL:] is V49() set
seq is non empty strict NORMSTR
the carrier of seq is non empty set
0. seq is V69(seq) Element of the carrier of seq
the ZeroF of seq is Element of the carrier of seq
[: the carrier of seq, the carrier of seq:] is set
the addF of seq is Relation-like [: the carrier of seq, the carrier of seq:] -defined the carrier of seq -valued Function-like V26([: the carrier of seq, the carrier of seq:]) V30([: the carrier of seq, the carrier of seq:], the carrier of seq) Element of bool [:[: the carrier of seq, the carrier of seq:], the carrier of seq:]
[:[: the carrier of seq, the carrier of seq:], the carrier of seq:] is set
bool [:[: the carrier of seq, the carrier of seq:], the carrier of seq:] is set
[:REAL, the carrier of seq:] is V49() set
the Mult of seq is Relation-like [:REAL, the carrier of seq:] -defined the carrier of seq -valued Function-like V26([:REAL, the carrier of seq:]) V30([:REAL, the carrier of seq:], the carrier of seq) Element of bool [:[:REAL, the carrier of seq:], the carrier of seq:]
[:[:REAL, the carrier of seq:], the carrier of seq:] is V49() set
bool [:[:REAL, the carrier of seq:], the carrier of seq:] is V49() set
the normF of seq is non empty Relation-like the carrier of seq -defined REAL -valued Function-like V26( the carrier of seq) V30( the carrier of seq, REAL ) complex-yielding V36() V37() Element of bool [: the carrier of seq,REAL:]
[: the carrier of seq,REAL:] is complex-yielding V36() V37() V49() set
bool [: the carrier of seq,REAL:] is V49() set
seq9 is non empty strict NORMSTR
the carrier of seq9 is non empty set
0. seq9 is V69(seq9) Element of the carrier of seq9
the ZeroF of seq9 is Element of the carrier of seq9
[: the carrier of seq9, the carrier of seq9:] is set
the addF of seq9 is Relation-like [: the carrier of seq9, the carrier of seq9:] -defined the carrier of seq9 -valued Function-like V26([: the carrier of seq9, the carrier of seq9:]) V30([: the carrier of seq9, the carrier of seq9:], the carrier of seq9) Element of bool [:[: the carrier of seq9, the carrier of seq9:], the carrier of seq9:]
[:[: the carrier of seq9, the carrier of seq9:], the carrier of seq9:] is set
bool [:[: the carrier of seq9, the carrier of seq9:], the carrier of seq9:] is set
[:REAL, the carrier of seq9:] is V49() set
the Mult of seq9 is Relation-like [:REAL, the carrier of seq9:] -defined the carrier of seq9 -valued Function-like V26([:REAL, the carrier of seq9:]) V30([:REAL, the carrier of seq9:], the carrier of seq9) Element of bool [:[:REAL, the carrier of seq9:], the carrier of seq9:]
[:[:REAL, the carrier of seq9:], the carrier of seq9:] is V49() set
bool [:[:REAL, the carrier of seq9:], the carrier of seq9:] is V49() set
the normF of seq9 is non empty Relation-like the carrier of seq9 -defined REAL -valued Function-like V26( the carrier of seq9) V30( the carrier of seq9, REAL ) complex-yielding V36() V37() Element of bool [: the carrier of seq9,REAL:]
[: the carrier of seq9,REAL:] is complex-yielding V36() V37() V49() set
bool [: the carrier of seq9,REAL:] is V49() set
n is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V49() V54() set
(n) is non empty strict NORMSTR
the carrier of (n) is non empty set
REAL n is non empty functional FinSequence-membered FinSequenceSet of REAL
TOP-REAL n is non empty non trivial right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital TopSpace-like V200() L20()
the carrier of (TOP-REAL n) is non empty non trivial set
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V49() V54() set
(n) is non empty strict NORMSTR
the carrier of (n) is non empty set
REAL n is non empty functional FinSequence-membered FinSequenceSet of REAL
seq is Element of the carrier of (n)
||.seq.|| is V11() real ext-real Element of REAL
the normF of (n) is non empty Relation-like the carrier of (n) -defined REAL -valued Function-like V26( the carrier of (n)) V30( the carrier of (n), REAL ) complex-yielding V36() V37() Element of bool [: the carrier of (n),REAL:]
[: the carrier of (n),REAL:] is complex-yielding V36() V37() V49() set
bool [: the carrier of (n),REAL:] is V49() set
the normF of (n) . seq is V11() real ext-real Element of REAL
seq9 is Relation-like NAT -defined REAL -valued Function-like complex-yielding V36() V37() V49() V56(n) FinSequence-like FinSubsequence-like Element of REAL n
|.seq9.| is V11() real ext-real non negative Element of REAL
the normF of (n) . seq is V11() real ext-real Element of REAL
(n) is non empty Relation-like REAL n -defined REAL -valued Function-like V26( REAL n) V30( REAL n, REAL ) complex-yielding V36() V37() Element of bool [:(REAL n),REAL:]
[:(REAL n),REAL:] is complex-yielding V36() V37() V49() set
bool [:(REAL n),REAL:] is V49() set
(n) . seq9 is V11() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V49() V54() set
(n) is non empty strict NORMSTR
the carrier of (n) is non empty set
REAL n is non empty functional FinSequence-membered FinSequenceSet of REAL
seq is Element of the carrier of (n)
seq9 is Element of the carrier of (n)
seq + seq9 is Element of the carrier of (n)
the addF of (n) is Relation-like [: the carrier of (n), the carrier of (n):] -defined the carrier of (n) -valued Function-like V26([: the carrier of (n), the carrier of (n):]) V30([: the carrier of (n), the carrier of (n):], the carrier of (n)) Element of bool [:[: the carrier of (n), the carrier of (n):], the carrier of (n):]
[: the carrier of (n), the carrier of (n):] is set
[:[: the carrier of (n), the carrier of (n):], the carrier of (n):] is set
bool [:[: the carrier of (n), the carrier of (n):], the carrier of (n):] is set
the addF of (n) . (seq,seq9) is Element of the carrier of (n)
[seq,seq9] is set
the addF of (n) . [seq,seq9] is set
r is Relation-like NAT -defined REAL -valued Function-like complex-yielding V36() V37() V49() V56(n) FinSequence-like FinSubsequence-like Element of REAL n
k is Relation-like NAT -defined REAL -valued Function-like complex-yielding V36() V37() V49() V56(n) FinSequence-like FinSubsequence-like Element of REAL n
r + k is Relation-like NAT -defined REAL -valued Function-like complex-yielding V36() V37() V49() V56(n) FinSequence-like FinSubsequence-like Element of REAL n
(n) is Relation-like [:(REAL n),(REAL n):] -defined REAL n -valued Function-like V26([:(REAL n),(REAL n):]) V30([:(REAL n),(REAL n):], REAL n) V47() V48() commutative associative Element of bool [:[:(REAL n),(REAL n):],(REAL n):]
[:(REAL n),(REAL n):] is set
[:[:(REAL n),(REAL n):],(REAL n):] is set
bool [:[:(REAL n),(REAL n):],(REAL n):] is set
(n) . (r,k) is Relation-like NAT -defined Function-like V49() V56(n) FinSequence-like FinSubsequence-like Element of REAL n
[r,k] is set
(n) . [r,k] is Relation-like NAT -defined Function-like V49() FinSequence-like FinSubsequence-like set
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V49() V54() set
(n) is non empty strict NORMSTR
the carrier of (n) is non empty set
REAL n is non empty functional FinSequence-membered FinSequenceSet of REAL
seq is Element of the carrier of (n)
seq9 is Relation-like NAT -defined REAL -valued Function-like complex-yielding V36() V37() V49() V56(n) FinSequence-like FinSubsequence-like Element of REAL n
r is V11() real ext-real set
r * seq is Element of the carrier of (n)
the Mult of (n) is Relation-like [:REAL, the carrier of (n):] -defined the carrier of (n) -valued Function-like V26([:REAL, the carrier of (n):]) V30([:REAL, the carrier of (n):], the carrier of (n)) Element of bool [:[:REAL, the carrier of (n):], the carrier of (n):]
[:REAL, the carrier of (n):] is V49() set
[:[:REAL, the carrier of (n):], the carrier of (n):] is V49() set
bool [:[:REAL, the carrier of (n):], the carrier of (n):] is V49() set
the Mult of (n) . (r,seq) is set
[r,seq] is set
the Mult of (n) . [r,seq] is set
r * seq9 is Relation-like NAT -defined REAL -valued Function-like complex-yielding V36() V37() V49() V56(n) FinSequence-like FinSubsequence-like Element of REAL n
k is V11() real ext-real Element of REAL
k * seq is Element of the carrier of (n)
the Mult of (n) . (k,seq) is set
[k,seq] is set
the Mult of (n) . [k,seq] is set
(n) is Relation-like [:REAL,(REAL n):] -defined REAL n -valued Function-like V26([:REAL,(REAL n):]) V30([:REAL,(REAL n):], REAL n) V47() V48() Element of bool [:[:REAL,(REAL n):],(REAL n):]
[:REAL,(REAL n):] is V49() set
[:[:REAL,(REAL n):],(REAL n):] is V49() set
bool [:[:REAL,(REAL n):],(REAL n):] is V49() set
(n) . (k,seq) is set
(n) . [k,seq] is Relation-like NAT -defined Function-like V49() FinSequence-like FinSubsequence-like set
k * seq9 is Relation-like NAT -defined REAL -valued Function-like complex-yielding V36() V37() V49() V56(n) FinSequence-like FinSubsequence-like Element of REAL n
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V49() V54() set
(n) is non empty strict NORMSTR
REAL n is non empty functional FinSequence-membered FinSequenceSet of REAL
0. (n) is V69((n)) Element of the carrier of (n)
the carrier of (n) is non empty set
the ZeroF of (n) is Element of the carrier of (n)
seq is Relation-like NAT -defined REAL -valued Function-like complex-yielding V36() V37() V49() V56(n) FinSequence-like FinSubsequence-like Element of REAL n
|.seq.| is V11() real ext-real non negative Element of REAL
0* n is Relation-like NAT -defined REAL -valued Function-like complex-yielding V36() V37() V49() V56(n) FinSequence-like FinSubsequence-like Element of REAL n
||.(0. (n)).|| is V11() real ext-real Element of REAL
the normF of (n) is non empty Relation-like the carrier of (n) -defined REAL -valued Function-like V26( the carrier of (n)) V30( the carrier of (n), REAL ) complex-yielding V36() V37() Element of bool [: the carrier of (n),REAL:]
[: the carrier of (n),REAL:] is complex-yielding V36() V37() V49() set
bool [: the carrier of (n),REAL:] is V49() set
the normF of (n) . (0. (n)) is V11() real ext-real Element of REAL
seq9 is Element of the carrier of (n)
||.seq9.|| is V11() real ext-real Element of REAL
the normF of (n) . seq9 is V11() real ext-real Element of REAL
r is Element of the carrier of (n)
seq9 + r is Element of the carrier of (n)
the addF of (n) is Relation-like [: the carrier of (n), the carrier of (n):] -defined the carrier of (n) -valued Function-like V26([: the carrier of (n), the carrier of (n):]) V30([: the carrier of (n), the carrier of (n):], the carrier of (n)) Element of bool [:[: the carrier of (n), the carrier of (n):], the carrier of (n):]
[: the carrier of (n), the carrier of (n):] is set
[:[: the carrier of (n), the carrier of (n):], the carrier of (n):] is set
bool [:[: the carrier of (n), the carrier of (n):], the carrier of (n):] is set
the addF of (n) . (seq9,r) is Element of the carrier of (n)
[seq9,r] is set
the addF of (n) . [seq9,r] is set
||.(seq9 + r).|| is V11() real ext-real Element of REAL
the normF of (n) . (seq9 + r) is V11() real ext-real Element of REAL
||.r.|| is V11() real ext-real Element of REAL
the normF of (n) . r is V11() real ext-real Element of REAL
||.seq9.|| + ||.r.|| is V11() real ext-real Element of REAL
k is V11() real ext-real Element of REAL
k * seq9 is Element of the carrier of (n)
the Mult of (n) is Relation-like [:REAL, the carrier of (n):] -defined the carrier of (n) -valued Function-like V26([:REAL, the carrier of (n):]) V30([:REAL, the carrier of (n):], the carrier of (n)) Element of bool [:[:REAL, the carrier of (n):], the carrier of (n):]
[:REAL, the carrier of (n):] is V49() set
[:[:REAL, the carrier of (n):], the carrier of (n):] is V49() set
bool [:[:REAL, the carrier of (n):], the carrier of (n):] is V49() set
the Mult of (n) . (k,seq9) is set
[k,seq9] is set
the Mult of (n) . [k,seq9] is set
||.(k * seq9).|| is V11() real ext-real Element of REAL
the normF of (n) . (k * seq9) is V11() real ext-real Element of REAL
abs k is V11() real ext-real Element of REAL
(abs k) * ||.seq9.|| is V11() real ext-real Element of REAL
m1 is Relation-like NAT -defined REAL -valued Function-like complex-yielding V36() V37() V49() V56(n) FinSequence-like FinSubsequence-like Element of REAL n
|.m1.| is V11() real ext-real non negative Element of REAL
m1 is Relation-like NAT -defined REAL -valued Function-like complex-yielding V36() V37() V49() V56(n) FinSequence-like FinSubsequence-like Element of REAL n
k * m1 is Relation-like NAT -defined REAL -valued Function-like complex-yielding V36() V37() V49() V56(n) FinSequence-like FinSubsequence-like Element of REAL n
|.(k * m1).| is V11() real ext-real non negative Element of REAL
|.m1.| is V11() real ext-real non negative Element of REAL
(abs k) * |.m1.| is V11() real ext-real Element of REAL
m1 is Relation-like NAT -defined REAL -valued Function-like complex-yielding V36() V37() V49() V56(n) FinSequence-like FinSubsequence-like Element of REAL n
m2 is Relation-like NAT -defined REAL -valued Function-like complex-yielding V36() V37() V49() V56(n) FinSequence-like FinSubsequence-like Element of REAL n
m1 + m2 is Relation-like NAT -defined REAL -valued Function-like complex-yielding V36() V37() V49() V56(n) FinSequence-like FinSubsequence-like Element of REAL n
|.(m1 + m2).| is V11() real ext-real non negative Element of REAL
|.m1.| is V11() real ext-real non negative Element of REAL
|.m2.| is V11() real ext-real non negative Element of REAL
|.m1.| + |.m2.| is V11() real ext-real non negative Element of REAL
||.seq9.|| + |.m2.| is V11() real ext-real Element of REAL
seq9 is V11() real ext-real set
r is V11() real ext-real set
seq9 + r is V11() real ext-real Element of REAL
m2 is Element of the carrier of (n)
(seq9 + r) * m2 is Element of the carrier of (n)
the Mult of (n) is Relation-like [:REAL, the carrier of (n):] -defined the carrier of (n) -valued Function-like V26([:REAL, the carrier of (n):]) V30([:REAL, the carrier of (n):], the carrier of (n)) Element of bool [:[:REAL, the carrier of (n):], the carrier of (n):]
[:REAL, the carrier of (n):] is V49() set
[:[:REAL, the carrier of (n):], the carrier of (n):] is V49() set
bool [:[:REAL, the carrier of (n):], the carrier of (n):] is V49() set
the Mult of (n) . ((seq9 + r),m2) is set
[(seq9 + r),m2] is set
the Mult of (n) . [(seq9 + r),m2] is set
seq9 * m2 is Element of the carrier of (n)
the Mult of (n) . (seq9,m2) is set
[seq9,m2] is set
the Mult of (n) . [seq9,m2] is set
r * m2 is Element of the carrier of (n)
the Mult of (n) . (r,m2) is set
[r,m2] is set
the Mult of (n) . [r,m2] is set
(seq9 * m2) + (r * m2) is Element of the carrier of (n)
the addF of (n) is Relation-like [: the carrier of (n), the carrier of (n):] -defined the carrier of (n) -valued Function-like V26([: the carrier of (n), the carrier of (n):]) V30([: the carrier of (n), the carrier of (n):], the carrier of (n)) Element of bool [:[: the carrier of (n), the carrier of (n):], the carrier of (n):]
[: the carrier of (n), the carrier of (n):] is set
[:[: the carrier of (n), the carrier of (n):], the carrier of (n):] is set
bool [:[: the carrier of (n), the carrier of (n):], the carrier of (n):] is set
the addF of (n) . ((seq9 * m2),(r * m2)) is Element of the carrier of (n)
[(seq9 * m2),(r * m2)] is set
the addF of (n) . [(seq9 * m2),(r * m2)] is set
k is V11() real ext-real Element of REAL
m1 is V11() real ext-real Element of REAL
k + m1 is V11() real ext-real Element of REAL
(k + m1) * m2 is Element of the carrier of (n)
the Mult of (n) . ((k + m1),m2) is set
[(k + m1),m2] is set
the Mult of (n) . [(k + m1),m2] is set
k * m2 is Element of the carrier of (n)
the Mult of (n) . (k,m2) is set
[k,m2] is set
the Mult of (n) . [k,m2] is set
m1 * m2 is Element of the carrier of (n)
the Mult of (n) . (m1,m2) is set
[m1,m2] is set
the Mult of (n) . [m1,m2] is set
(k * m2) + (m1 * m2) is Element of the carrier of (n)
the addF of (n) . ((k * m2),(m1 * m2)) is Element of the carrier of (n)
[(k * m2),(m1 * m2)] is set
the addF of (n) . [(k * m2),(m1 * m2)] is set
n -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
p is Relation-like NAT -defined REAL -valued Function-like complex-yielding V36() V37() V49() V56(n) FinSequence-like FinSubsequence-like Element of REAL n
k * p is Relation-like NAT -defined REAL -valued Function-like complex-yielding V36() V37() V49() V56(n) FinSequence-like FinSubsequence-like Element of REAL n
m1 * p is Relation-like NAT -defined REAL -valued Function-like complex-yielding V36() V37() V49() V56(n) FinSequence-like FinSubsequence-like Element of REAL n
(n) is Relation-like [:REAL,(REAL n):] -defined REAL n -valued Function-like V26([:REAL,(REAL n):]) V30([:REAL,(REAL n):], REAL n) V47() V48() Element of bool [:[:REAL,(REAL n):],(REAL n):]
[:REAL,(REAL n):] is V49() set
[:[:REAL,(REAL n):],(REAL n):] is V49() set
bool [:[:REAL,(REAL n):],(REAL n):] is V49() set
(n) . ((k + m1),m2) is set
(n) . [(k + m1),m2] is Relation-like NAT -defined Function-like V49() FinSequence-like FinSubsequence-like set
k is Relation-like NAT -defined REAL -valued Function-like complex-yielding V36() V37() V49() V56(n) FinSequence-like FinSubsequence-like Element of n -tuples_on REAL
(k + m1) * k is Relation-like NAT -defined REAL -valued Function-like complex-yielding V36() V37() V49() V56(n) FinSequence-like FinSubsequence-like Element of n -tuples_on REAL
k * k is Relation-like NAT -defined REAL -valued Function-like complex-yielding V36() V37() V49() V56(n) FinSequence-like FinSubsequence-like Element of n -tuples_on REAL
m1 * k is Relation-like NAT -defined REAL -valued Function-like complex-yielding V36() V37() V49() V56(n) FinSequence-like FinSubsequence-like Element of n -tuples_on REAL
(k * k) + (m1 * k) is Relation-like NAT -defined REAL -valued Function-like complex-yielding V36() V37() V49() V56(n) FinSequence-like FinSubsequence-like Element of n -tuples_on REAL
seq9 is V11() real ext-real set
k is Element of the carrier of (n)
m1 is Element of the carrier of (n)
k + m1 is Element of the carrier of (n)
the addF of (n) is Relation-like [: the carrier of (n), the carrier of (n):] -defined the carrier of (n) -valued Function-like V26([: the carrier of (n), the carrier of (n):]) V30([: the carrier of (n), the carrier of (n):], the carrier of (n)) Element of bool [:[: the carrier of (n), the carrier of (n):], the carrier of (n):]
[: the carrier of (n), the carrier of (n):] is set
[:[: the carrier of (n), the carrier of (n):], the carrier of (n):] is set
bool [:[: the carrier of (n), the carrier of (n):], the carrier of (n):] is set
the addF of (n) . (k,m1) is Element of the carrier of (n)
[k,m1] is set
the addF of (n) . [k,m1] is set
seq9 * (k + m1) is Element of the carrier of (n)
the Mult of (n) is Relation-like [:REAL, the carrier of (n):] -defined the carrier of (n) -valued Function-like V26([:REAL, the carrier of (n):]) V30([:REAL, the carrier of (n):], the carrier of (n)) Element of bool [:[:REAL, the carrier of (n):], the carrier of (n):]
[:REAL, the carrier of (n):] is V49() set
[:[:REAL, the carrier of (n):], the carrier of (n):] is V49() set
bool [:[:REAL, the carrier of (n):], the carrier of (n):] is V49() set
the Mult of (n) . (seq9,(k + m1)) is set
[seq9,(k + m1)] is set
the Mult of (n) . [seq9,(k + m1)] is set
seq9 * k is Element of the carrier of (n)
the Mult of (n) . (seq9,k) is set
[seq9,k] is set
the Mult of (n) . [seq9,k] is set
seq9 * m1 is Element of the carrier of (n)
the Mult of (n) . (seq9,m1) is set
[seq9,m1] is set
the Mult of (n) . [seq9,m1] is set
(seq9 * k) + (seq9 * m1) is Element of the carrier of (n)
the addF of (n) . ((seq9 * k),(seq9 * m1)) is Element of the carrier of (n)
[(seq9 * k),(seq9 * m1)] is set
the addF of (n) . [(seq9 * k),(seq9 * m1)] is set
r is V11() real ext-real Element of REAL
r * (k + m1) is Element of the carrier of (n)
the Mult of (n) . (r,(k + m1)) is set
[r,(k + m1)] is set
the Mult of (n) . [r,(k + m1)] is set
r * k is Element of the carrier of (n)
the Mult of (n) . (r,k) is set
[r,k] is set
the Mult of (n) . [r,k] is set
r * m1 is Element of the carrier of (n)
the Mult of (n) . (r,m1) is set
[r,m1] is set
the Mult of (n) . [r,m1] is set
(r * k) + (r * m1) is Element of the carrier of (n)
the addF of (n) . ((r * k),(r * m1)) is Element of the carrier of (n)
[(r * k),(r * m1)] is set
the addF of (n) . [(r * k),(r * m1)] is set
n -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
m2 is Relation-like NAT -defined REAL -valued Function-like complex-yielding V36() V37() V49() V56(n) FinSequence-like FinSubsequence-like Element of REAL n
p is Relation-like NAT -defined REAL -valued Function-like complex-yielding V36() V37() V49() V56(n) FinSequence-like FinSubsequence-like Element of REAL n
r * m2 is Relation-like NAT -defined REAL -valued Function-like complex-yielding V36() V37() V49() V56(n) FinSequence-like FinSubsequence-like Element of REAL n
r * p is Relation-like NAT -defined REAL -valued Function-like complex-yielding V36() V37() V49() V56(n) FinSequence-like FinSubsequence-like Element of REAL n
(n) is Relation-like [:REAL,(REAL n):] -defined REAL n -valued Function-like V26([:REAL,(REAL n):]) V30([:REAL,(REAL n):], REAL n) V47() V48() Element of bool [:[:REAL,(REAL n):],(REAL n):]
[:REAL,(REAL n):] is V49() set
[:[:REAL,(REAL n):],(REAL n):] is V49() set
bool [:[:REAL,(REAL n):],(REAL n):] is V49() set
(n) . (r,(k + m1)) is set
(n) . [r,(k + m1)] is Relation-like NAT -defined Function-like V49() FinSequence-like FinSubsequence-like set
m2 + p is Relation-like NAT -defined REAL -valued Function-like complex-yielding V36() V37() V49() V56(n) FinSequence-like FinSubsequence-like Element of REAL n
(n) . (r,(m2 + p)) is Relation-like NAT -defined Function-like V49() V56(n) FinSequence-like FinSubsequence-like Element of REAL n
[r,(m2 + p)] is set
(n) . [r,(m2 + p)] is Relation-like NAT -defined Function-like V49() FinSequence-like FinSubsequence-like set
k is Relation-like NAT -defined REAL -valued Function-like complex-yielding V36() V37() V49() V56(n) FinSequence-like FinSubsequence-like Element of n -tuples_on REAL
p is Relation-like NAT -defined REAL -valued Function-like complex-yielding V36() V37() V49() V56(n) FinSequence-like FinSubsequence-like Element of n -tuples_on REAL
k + p is Relation-like NAT -defined REAL -valued Function-like complex-yielding V36() V37() V49() V56(n) FinSequence-like FinSubsequence-like Element of n -tuples_on REAL
r * (k + p) is Relation-like NAT -defined REAL -valued Function-like complex-yielding V36() V37() V49() V56(n) FinSequence-like FinSubsequence-like Element of n -tuples_on REAL
r * k is Relation-like NAT -defined REAL -valued Function-like complex-yielding V36() V37() V49() V56(n) FinSequence-like FinSubsequence-like Element of n -tuples_on REAL
r * p is Relation-like NAT -defined REAL -valued Function-like complex-yielding V36() V37() V49() V56(n) FinSequence-like FinSubsequence-like Element of n -tuples_on REAL
(r * k) + (r * p) is Relation-like NAT -defined REAL -valued Function-like complex-yielding V36() V37() V49() V56(n) FinSequence-like FinSubsequence-like Element of n -tuples_on REAL
seq9 is V11() real ext-real set
r is V11() real ext-real set
seq9 * r is V11() real ext-real Element of REAL
m2 is Element of the carrier of (n)
(seq9 * r) * m2 is Element of the carrier of (n)
the Mult of (n) is Relation-like [:REAL, the carrier of (n):] -defined the carrier of (n) -valued Function-like V26([:REAL, the carrier of (n):]) V30([:REAL, the carrier of (n):], the carrier of (n)) Element of bool [:[:REAL, the carrier of (n):], the carrier of (n):]
[:REAL, the carrier of (n):] is V49() set
[:[:REAL, the carrier of (n):], the carrier of (n):] is V49() set
bool [:[:REAL, the carrier of (n):], the carrier of (n):] is V49() set
the Mult of (n) . ((seq9 * r),m2) is set
[(seq9 * r),m2] is set
the Mult of (n) . [(seq9 * r),m2] is set
r * m2 is Element of the carrier of (n)
the Mult of (n) . (r,m2) is set
[r,m2] is set
the Mult of (n) . [r,m2] is set
seq9 * (r * m2) is Element of the carrier of (n)
the Mult of (n) . (seq9,(r * m2)) is set
[seq9,(r * m2)] is set
the Mult of (n) . [seq9,(r * m2)] is set
k is V11() real ext-real Element of REAL
m1 is V11() real ext-real Element of REAL
k * m1 is V11() real ext-real Element of REAL
(k * m1) * m2 is Element of the carrier of (n)
the Mult of (n) . ((k * m1),m2) is set
[(k * m1),m2] is set
the Mult of (n) . [(k * m1),m2] is set
m1 * m2 is Element of the carrier of (n)
the Mult of (n) . (m1,m2) is set
[m1,m2] is set
the Mult of (n) . [m1,m2] is set
k * (m1 * m2) is Element of the carrier of (n)
the Mult of (n) . (k,(m1 * m2)) is set
[k,(m1 * m2)] is set
the Mult of (n) . [k,(m1 * m2)] is set
n -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
p is Relation-like NAT -defined REAL -valued Function-like complex-yielding V36() V37() V49() V56(n) FinSequence-like FinSubsequence-like Element of REAL n
m1 * p is Relation-like NAT -defined REAL -valued Function-like complex-yielding V36() V37() V49() V56(n) FinSequence-like FinSubsequence-like Element of REAL n
(n) is Relation-like [:REAL,(REAL n):] -defined REAL n -valued Function-like V26([:REAL,(REAL n):]) V30([:REAL,(REAL n):], REAL n) V47() V48() Element of bool [:[:REAL,(REAL n):],(REAL n):]
[:REAL,(REAL n):] is V49() set
[:[:REAL,(REAL n):],(REAL n):] is V49() set
bool [:[:REAL,(REAL n):],(REAL n):] is V49() set
(n) . ((k * m1),m2) is set
(n) . [(k * m1),m2] is Relation-like NAT -defined Function-like V49() FinSequence-like FinSubsequence-like set
(k * m1) * p is Relation-like NAT -defined REAL -valued Function-like complex-yielding V36() V37() V49() V56(n) FinSequence-like FinSubsequence-like Element of REAL n
k is Relation-like NAT -defined REAL -valued Function-like complex-yielding V36() V37() V49() V56(n) FinSequence-like FinSubsequence-like Element of n -tuples_on REAL
m1 * k is Relation-like NAT -defined REAL -valued Function-like complex-yielding V36() V37() V49() V56(n) FinSequence-like FinSubsequence-like Element of n -tuples_on REAL
k * (m1 * k) is Relation-like NAT -defined REAL -valued Function-like complex-yielding V36() V37() V49() V56(n) FinSequence-like FinSubsequence-like Element of n -tuples_on REAL
seq9 is Element of the carrier of (n)
1 * seq9 is Element of the carrier of (n)
the Mult of (n) is Relation-like [:REAL, the carrier of (n):] -defined the carrier of (n) -valued Function-like V26([:REAL, the carrier of (n):]) V30([:REAL, the carrier of (n):], the carrier of (n)) Element of bool [:[:REAL, the carrier of (n):], the carrier of (n):]
[:REAL, the carrier of (n):] is V49() set
[:[:REAL, the carrier of (n):], the carrier of (n):] is V49() set
bool [:[:REAL, the carrier of (n):], the carrier of (n):] is V49() set
the Mult of (n) . (1,seq9) is set
[1,seq9] is set
the Mult of (n) . [1,seq9] is set
n -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
r is Relation-like NAT -defined REAL -valued Function-like complex-yielding V36() V37() V49() V56(n) FinSequence-like FinSubsequence-like Element of REAL n
(n) is Relation-like [:REAL,(REAL n):] -defined REAL n -valued Function-like V26([:REAL,(REAL n):]) V30([:REAL,(REAL n):], REAL n) V47() V48() Element of bool [:[:REAL,(REAL n):],(REAL n):]
[:REAL,(REAL n):] is V49() set
[:[:REAL,(REAL n):],(REAL n):] is V49() set
bool [:[:REAL,(REAL n):],(REAL n):] is V49() set
(n) . (1,seq9) is set
(n) . [1,seq9] is Relation-like NAT -defined Function-like V49() FinSequence-like FinSubsequence-like set
k is Relation-like NAT -defined REAL -valued Function-like complex-yielding V36() V37() V49() V56(n) FinSequence-like FinSubsequence-like Element of n -tuples_on REAL
1 * k is Relation-like NAT -defined REAL -valued Function-like complex-yielding V36() V37() V49() V56(n) FinSequence-like FinSubsequence-like Element of n -tuples_on REAL
seq9 is Element of the carrier of (n)
r is Element of the carrier of (n)
seq9 + r is Element of the carrier of (n)
the addF of (n) is Relation-like [: the carrier of (n), the carrier of (n):] -defined the carrier of (n) -valued Function-like V26([: the carrier of (n), the carrier of (n):]) V30([: the carrier of (n), the carrier of (n):], the carrier of (n)) Element of bool [:[: the carrier of (n), the carrier of (n):], the carrier of (n):]
[: the carrier of (n), the carrier of (n):] is set
[:[: the carrier of (n), the carrier of (n):], the carrier of (n):] is set
bool [:[: the carrier of (n), the carrier of (n):], the carrier of (n):] is set
the addF of (n) . (seq9,r) is Element of the carrier of (n)
[seq9,r] is set
the addF of (n) . [seq9,r] is set
r + seq9 is Element of the carrier of (n)
the addF of (n) . (r,seq9) is Element of the carrier of (n)
[r,seq9] is set
the addF of (n) . [r,seq9] is set
(n) is Relation-like [:(REAL n),(REAL n):] -defined REAL n -valued Function-like V26([:(REAL n),(REAL n):]) V30([:(REAL n),(REAL n):], REAL n) V47() V48() commutative associative Element of bool [:[:(REAL n),(REAL n):],(REAL n):]
[:(REAL n),(REAL n):] is set
[:[:(REAL n),(REAL n):],(REAL n):] is set
bool [:[:(REAL n),(REAL n):],(REAL n):] is set
(n) . (seq9,r) is set
(n) . [seq9,r] is Relation-like NAT -defined Function-like V49() FinSequence-like FinSubsequence-like set
m1 is Relation-like NAT -defined REAL -valued Function-like complex-yielding V36() V37() V49() V56(n) FinSequence-like FinSubsequence-like Element of REAL n
k is Relation-like NAT -defined REAL -valued Function-like complex-yielding V36() V37() V49() V56(n) FinSequence-like FinSubsequence-like Element of REAL n
(n) . (m1,k) is Relation-like NAT -defined Function-like V49() V56(n) FinSequence-like FinSubsequence-like Element of REAL n
[m1,k] is set
(n) . [m1,k] is Relation-like NAT -defined Function-like V49() FinSequence-like FinSubsequence-like set
seq9 is Element of the carrier of (n)
r is Element of the carrier of (n)
seq9 + r is Element of the carrier of (n)
the addF of (n) is Relation-like [: the carrier of (n), the carrier of (n):] -defined the carrier of (n) -valued Function-like V26([: the carrier of (n), the carrier of (n):]) V30([: the carrier of (n), the carrier of (n):], the carrier of (n)) Element of bool [:[: the carrier of (n), the carrier of (n):], the carrier of (n):]
[: the carrier of (n), the carrier of (n):] is set
[:[: the carrier of (n), the carrier of (n):], the carrier of (n):] is set
bool [:[: the carrier of (n), the carrier of (n):], the carrier of (n):] is set
the addF of (n) . (seq9,r) is Element of the carrier of (n)
[seq9,r] is set
the addF of (n) . [seq9,r] is set
k is Element of the carrier of (n)
(seq9 + r) + k is Element of the carrier of (n)
the addF of (n) . ((seq9 + r),k) is Element of the carrier of (n)
[(seq9 + r),k] is set
the addF of (n) . [(seq9 + r),k] is set
r + k is Element of the carrier of (n)
the addF of (n) . (r,k) is Element of the carrier of (n)
[r,k] is set
the addF of (n) . [r,k] is set
seq9 + (r + k) is Element of the carrier of (n)
the addF of (n) . (seq9,(r + k)) is Element of the carrier of (n)
[seq9,(r + k)] is set
the addF of (n) . [seq9,(r + k)] is set
m2 is Relation-like NAT -defined REAL -valued Function-like complex-yielding V36() V37() V49() V56(n) FinSequence-like FinSubsequence-like Element of REAL n
p is Relation-like NAT -defined REAL -valued Function-like complex-yielding V36() V37() V49() V56(n) FinSequence-like FinSubsequence-like Element of REAL n
m2 + p is Relation-like NAT -defined REAL -valued Function-like complex-yielding V36() V37() V49() V56(n) FinSequence-like FinSubsequence-like Element of REAL n
(n) is Relation-like [:(REAL n),(REAL n):] -defined REAL n -valued Function-like V26([:(REAL n),(REAL n):]) V30([:(REAL n),(REAL n):], REAL n) V47() V48() commutative associative Element of bool [:[:(REAL n),(REAL n):],(REAL n):]
[:(REAL n),(REAL n):] is set
[:[:(REAL n),(REAL n):],(REAL n):] is set
bool [:[:(REAL n),(REAL n):],(REAL n):] is set
(n) . (( the addF of (n) . (seq9,r)),k) is set
[( the addF of (n) . (seq9,r)),k] is set
(n) . [( the addF of (n) . (seq9,r)),k] is Relation-like NAT -defined Function-like V49() FinSequence-like FinSubsequence-like set
m1 is Relation-like NAT -defined REAL -valued Function-like complex-yielding V36() V37() V49() V56(n) FinSequence-like FinSubsequence-like Element of REAL n
(n) . (m1,m2) is Relation-like NAT -defined Function-like V49() V56(n) FinSequence-like FinSubsequence-like Element of REAL n
[m1,m2] is set
(n) . [m1,m2] is Relation-like NAT -defined Function-like V49() FinSequence-like FinSubsequence-like set
(n) . (((n) . (m1,m2)),p) is Relation-like NAT -defined Function-like V49() V56(n) FinSequence-like FinSubsequence-like Element of REAL n
[((n) . (m1,m2)),p] is set
(n) . [((n) . (m1,m2)),p] is Relation-like NAT -defined Function-like V49() FinSequence-like FinSubsequence-like set
(n) . (m2,p) is Relation-like NAT -defined Function-like V49() V56(n) FinSequence-like FinSubsequence-like Element of REAL n
[m2,p] is set
(n) . [m2,p] is Relation-like NAT -defined Function-like V49() FinSequence-like FinSubsequence-like set
(n) . (m1,((n) . (m2,p))) is Relation-like NAT -defined Function-like V49() V56(n) FinSequence-like FinSubsequence-like Element of REAL n
[m1,((n) . (m2,p))] is set
(n) . [m1,((n) . (m2,p))] is Relation-like NAT -defined Function-like V49() FinSequence-like FinSubsequence-like set
(n) . (m1,(m2 + p)) is Relation-like NAT -defined Function-like V49() V56(n) FinSequence-like FinSubsequence-like Element of REAL n
[m1,(m2 + p)] is set
(n) . [m1,(m2 + p)] is Relation-like NAT -defined Function-like V49() FinSequence-like FinSubsequence-like set
m1 + (m2 + p) is Relation-like NAT -defined REAL -valued Function-like complex-yielding V36() V37() V49() V56(n) FinSequence-like FinSubsequence-like Element of REAL n
seq9 is Element of the carrier of (n)
seq9 + (0. (n)) is Element of the carrier of (n)
the addF of (n) is Relation-like [: the carrier of (n), the carrier of (n):] -defined the carrier of (n) -valued Function-like V26([: the carrier of (n), the carrier of (n):]) V30([: the carrier of (n), the carrier of (n):], the carrier of (n)) Element of bool [:[: the carrier of (n), the carrier of (n):], the carrier of (n):]
[: the carrier of (n), the carrier of (n):] is set
[:[: the carrier of (n), the carrier of (n):], the carrier of (n):] is set
bool [:[: the carrier of (n), the carrier of (n):], the carrier of (n):] is set
the addF of (n) . (seq9,(0. (n))) is Element of the carrier of (n)
[seq9,(0. (n))] is set
the addF of (n) . [seq9,(0. (n))] is set
n -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
r is Relation-like NAT -defined REAL -valued Function-like complex-yielding V36() V37() V49() V56(n) FinSequence-like FinSubsequence-like Element of REAL n
n |-> 0 is Relation-like empty-yielding NAT -defined NAT -valued Function-like complex-yielding V36() V37() V38() V49() V56(n) FinSequence-like FinSubsequence-like Element of n -tuples_on NAT
n -tuples_on NAT is non empty functional FinSequence-membered FinSequenceSet of NAT
r + (0* n) is Relation-like NAT -defined REAL -valued Function-like complex-yielding V36() V37() V49() V56(n) FinSequence-like FinSubsequence-like Element of REAL n
k is Relation-like NAT -defined REAL -valued Function-like complex-yielding V36() V37() V49() V56(n) FinSequence-like FinSubsequence-like Element of n -tuples_on REAL
m1 is Relation-like NAT -defined REAL -valued Function-like complex-yielding V36() V37() V49() V56(n) FinSequence-like FinSubsequence-like Element of n -tuples_on REAL
k + m1 is Relation-like NAT -defined REAL -valued Function-like complex-yielding V36() V37() V49() V56(n) FinSequence-like FinSubsequence-like Element of n -tuples_on REAL
seq9 is Element of the carrier of (n)
n -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
r is Relation-like NAT -defined REAL -valued Function-like complex-yielding V36() V37() V49() V56(n) FinSequence-like FinSubsequence-like Element of REAL n
n |-> 0 is Relation-like empty-yielding NAT -defined NAT -valued Function-like complex-yielding V36() V37() V38() V49() V56(n) FinSequence-like FinSubsequence-like Element of n -tuples_on NAT
n -tuples_on NAT is non empty functional FinSequence-membered FinSequenceSet of NAT
- r is Relation-like NAT -defined REAL -valued Function-like complex-yielding V36() V37() V49() V56(n) FinSequence-like FinSubsequence-like Element of REAL n
K38(1) is V11() real ext-real non positive set
K38(1) (#) r is Relation-like NAT -defined Function-like complex-yielding V36() V37() V49() FinSequence-like FinSubsequence-like set
m1 is Element of the carrier of (n)
seq9 + m1 is Element of the carrier of (n)
the addF of (n) is Relation-like [: the carrier of (n), the carrier of (n):] -defined the carrier of (n) -valued Function-like V26([: the carrier of (n), the carrier of (n):]) V30([: the carrier of (n), the carrier of (n):], the carrier of (n)) Element of bool [:[: the carrier of (n), the carrier of (n):], the carrier of (n):]
[: the carrier of (n), the carrier of (n):] is set
[:[: the carrier of (n), the carrier of (n):], the carrier of (n):] is set
bool [:[: the carrier of (n), the carrier of (n):], the carrier of (n):] is set
the addF of (n) . (seq9,m1) is Element of the carrier of (n)
[seq9,m1] is set
the addF of (n) . [seq9,m1] is set
k is Relation-like NAT -defined REAL -valued Function-like complex-yielding V36() V37() V49() V56(n) FinSequence-like FinSubsequence-like Element of n -tuples_on REAL
- k is Relation-like NAT -defined REAL -valued Function-like complex-yielding V36() V37() V49() V56(n) FinSequence-like FinSubsequence-like Element of n -tuples_on REAL
K38(1) (#) k is Relation-like NAT -defined Function-like complex-yielding V36() V37() V49() FinSequence-like FinSubsequence-like set
k + (- k) is Relation-like NAT -defined REAL -valued Function-like complex-yielding V36() V37() V49() V56(n) FinSequence-like FinSubsequence-like Element of n -tuples_on REAL
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V49() V54() set
(n) is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive strict RealNormSpace-like NORMSTR
the carrier of (n) is non empty set
REAL n is non empty functional FinSequence-membered FinSequenceSet of REAL
seq is Element of the carrier of (n)
- seq is Element of the carrier of (n)
seq9 is Relation-like NAT -defined REAL -valued Function-like complex-yielding V36() V37() V49() V56(n) FinSequence-like FinSubsequence-like Element of REAL n
- seq9 is Relation-like NAT -defined REAL -valued Function-like complex-yielding V36() V37() V49() V56(n) FinSequence-like FinSubsequence-like Element of REAL n
K38(1) is V11() real ext-real non positive set
K38(1) (#) seq9 is Relation-like NAT -defined Function-like complex-yielding V36() V37() V49() FinSequence-like FinSubsequence-like set
n -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
- 1 is V11() real ext-real non positive V33() V34() Element of INT
(- 1) * seq is Element of the carrier of (n)
the Mult of (n) is Relation-like [:REAL, the carrier of (n):] -defined the carrier of (n) -valued Function-like V26([:REAL, the carrier of (n):]) V30([:REAL, the carrier of (n):], the carrier of (n)) Element of bool [:[:REAL, the carrier of (n):], the carrier of (n):]
[:REAL, the carrier of (n):] is V49() set
[:[:REAL, the carrier of (n):], the carrier of (n):] is V49() set
bool [:[:REAL, the carrier of (n):], the carrier of (n):] is V49() set
the Mult of (n) . ((- 1),seq) is set
[(- 1),seq] is set
the Mult of (n) . [(- 1),seq] is set
r is Relation-like NAT -defined REAL -valued Function-like complex-yielding V36() V37() V49() V56(n) FinSequence-like FinSubsequence-like Element of n -tuples_on REAL
- r is Relation-like NAT -defined REAL -valued Function-like complex-yielding V36() V37() V49() V56(n) FinSequence-like FinSubsequence-like Element of n -tuples_on REAL
K38(1) (#) r is Relation-like NAT -defined Function-like complex-yielding V36() V37() V49() FinSequence-like FinSubsequence-like set
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V49() V54() set
(n) is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive strict RealNormSpace-like NORMSTR
the carrier of (n) is non empty set
REAL n is non empty functional FinSequence-membered FinSequenceSet of REAL
seq is Element of the carrier of (n)
seq9 is Element of the carrier of (n)
seq - seq9 is Element of the carrier of (n)
- seq9 is Element of the carrier of (n)
seq + (- seq9) is Element of the carrier of (n)
the addF of (n) is Relation-like [: the carrier of (n), the carrier of (n):] -defined the carrier of (n) -valued Function-like V26([: the carrier of (n), the carrier of (n):]) V30([: the carrier of (n), the carrier of (n):], the carrier of (n)) Element of bool [:[: the carrier of (n), the carrier of (n):], the carrier of (n):]
[: the carrier of (n), the carrier of (n):] is set
[:[: the carrier of (n), the carrier of (n):], the carrier of (n):] is set
bool [:[: the carrier of (n), the carrier of (n):], the carrier of (n):] is set
the addF of (n) . (seq,(- seq9)) is Element of the carrier of (n)
[seq,(- seq9)] is set
the addF of (n) . [seq,(- seq9)] is set
r is Relation-like NAT -defined REAL -valued Function-like complex-yielding V36() V37() V49() V56(n) FinSequence-like FinSubsequence-like Element of REAL n
k is Relation-like NAT -defined REAL -valued Function-like complex-yielding V36() V37() V49() V56(n) FinSequence-like FinSubsequence-like Element of REAL n
r - k is Relation-like NAT -defined REAL -valued Function-like complex-yielding V36() V37() V49() V56(n) FinSequence-like FinSubsequence-like Element of REAL n
- k is Relation-like NAT -defined Function-like complex-yielding V36() V37() V49() FinSequence-like FinSubsequence-like set
K38(1) is V11() real ext-real non positive set
K38(1) (#) k is Relation-like NAT -defined Function-like complex-yielding V36() V37() V49() FinSequence-like FinSubsequence-like set
r + (- k) is Relation-like NAT -defined Function-like complex-yielding V36() V37() V49() FinSequence-like FinSubsequence-like set
- k is Relation-like NAT -defined REAL -valued Function-like complex-yielding V36() V37() V49() V56(n) FinSequence-like FinSubsequence-like Element of REAL n
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V49() V54() set
Seg n is V49() V56(n) V158() V159() V160() V161() V162() V163() Element of bool NAT
REAL n is non empty functional FinSequence-membered FinSequenceSet of REAL
seq is Relation-like NAT -defined REAL -valued Function-like complex-yielding V36() V37() V49() FinSequence-like FinSubsequence-like FinSequence of REAL
dom seq is V158() V159() V160() V161() V162() V163() Element of bool NAT
len seq is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V33() V34() V49() V54() V158() V159() V160() V161() V162() V163() Element of NAT
n -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V49() V54() set
REAL n is non empty functional FinSequence-membered FinSequenceSet of REAL
Seg n is V49() V56(n) V158() V159() V160() V161() V162() V163() Element of bool NAT
n + 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V33() V34() V49() V54() V158() V159() V160() V161() V162() V163() Element of