:: REAL_NS1 semantic presentation

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 NAT
REAL (n + 1) is non empty functional FinSequence-membered FinSequenceSet of REAL
Seg (n + 1) is V49() V56(n + 1) V158() V159() V160() V161() V162() V163() Element of bool NAT
seq is Relation-like NAT -defined REAL -valued Function-like complex-yielding V36() V37() V49() V56(n + 1) FinSequence-like FinSubsequence-like Element of REAL (n + 1)
Sum seq is V11() real ext-real Element of REAL
seq | n is Relation-like NAT -defined REAL -valued Function-like complex-yielding V36() V37() V49() FinSequence-like FinSubsequence-like FinSequence of REAL
seq . (n + 1) is V11() real ext-real Element of REAL
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
len (seq | n) 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
Seg (len seq) is V49() V56( len seq) V158() V159() V160() V161() V162() V163() Element of bool NAT
dom seq is V56(n + 1) V158() V159() V160() V161() V162() V163() Element of bool 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
seq | (Seg n) is Relation-like NAT -defined Function-like complex-yielding V36() V37() FinSubsequence-like set
seq | (n + 1) is Relation-like NAT -defined REAL -valued Function-like complex-yielding V36() V37() V49() FinSequence-like FinSubsequence-like FinSequence of REAL
seq | (Seg (n + 1)) is Relation-like NAT -defined Function-like complex-yielding V36() V37() FinSubsequence-like set
<*(seq . (n + 1))*> is non empty trivial Relation-like NAT -defined REAL -valued Function-like one-to-one constant complex-yielding V36() V37() V39() V40() V41() V42() V49() V56(1) FinSequence-like FinSubsequence-like FinSequence of REAL
r ^ <*(seq . (n + 1))*> is non empty Relation-like NAT -defined REAL -valued Function-like complex-yielding V36() V37() V49() V56(n + 1) FinSequence-like FinSubsequence-like FinSequence of REAL
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 NAT
Sum r is V11() real ext-real Element of REAL
(Sum r) + (seq . (n + 1)) is V11() real ext-real Element of REAL
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V33() V34() V49() V54() V158() V159() V160() V161() V162() V163() Element of NAT
seq . k is V11() real ext-real Element of REAL
(seq | (Seg n)) . k is V11() real ext-real Element of REAL
r . k is V11() real ext-real Element of REAL
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V33() V34() V49() V54() V158() V159() V160() V161() V162() V163() Element of NAT
r . k is V11() real ext-real Element of REAL
seq . k is V11() real ext-real Element of REAL
seq . k is V11() real ext-real Element of REAL
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V33() V34() V49() V54() V158() V159() V160() V161() V162() V163() Element of NAT
seq . k is V11() real ext-real Element of REAL
seq is Relation-like NAT -defined REAL -valued Function-like complex-yielding V36() V37() V49() V56(n + 1) FinSequence-like FinSubsequence-like Element of REAL (n + 1)
Sum seq is V11() real ext-real Element of REAL
seq9 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V33() V34() V49() V54() V158() V159() V160() V161() V162() V163() Element of NAT
seq . seq9 is V11() real ext-real Element of REAL
REAL 0 is non empty functional FinSequence-membered FinSequenceSet of REAL
Seg 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 V49() V54() V56( 0 ) V56( {} ) FinSequence-membered V158() V159() V160() V161() V162() V163() V164() Element of bool NAT
n 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( 0 ) FinSequence-like FinSubsequence-like FinSequence-membered V158() V159() V160() V161() V162() V163() V164() Element of REAL 0
Sum n is V11() real ext-real Element of REAL
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 . seq is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real Relation-like Function-like V49() V54() 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
Seg n is V49() V56(n) V158() V159() V160() V161() V162() V163() Element of bool NAT
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
seq9 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V49() V54() set
seq . seq9 is V11() real ext-real Element of REAL
abs (seq . seq9) is V11() real ext-real Element of REAL
sqr seq 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 -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
seq (#) seq is Relation-like NAT -defined Function-like complex-yielding V36() V37() V49() FinSequence-like FinSubsequence-like set
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V33() V34() V49() V54() V158() V159() V160() V161() V162() V163() Element 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
r . k is V11() real ext-real Element of REAL
seq . k is V11() real ext-real Element of REAL
(seq . k) ^2 is V11() real ext-real Element of REAL
K37((seq . k),(seq . k)) is V11() real ext-real set
(abs (seq . seq9)) * (abs (seq . seq9)) is V11() real ext-real Element of REAL
(seq . seq9) ^2 is V11() real ext-real Element of REAL
K37((seq . seq9),(seq . seq9)) is V11() real ext-real set
- (seq . seq9) is V11() real ext-real Element of REAL
- (seq . seq9) is V11() real ext-real Element of REAL
(sqr seq) . seq9 is V11() real ext-real Element of REAL
Sum (sqr seq) is V11() real ext-real Element of REAL
sqrt ((abs (seq . seq9)) * (abs (seq . seq9))) is V11() real ext-real Element of REAL
sqrt (Sum (sqr seq)) is V11() real ext-real Element of REAL
(abs (seq . seq9)) ^2 is V11() real ext-real Element of REAL
K37((abs (seq . seq9)),(abs (seq . seq9))) is V11() real ext-real set
sqrt ((abs (seq . seq9)) ^2) 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 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
Seg n is V49() V56(n) V158() V159() V160() V161() V162() V163() Element of bool NAT
seq is Element of the carrier of (n)
||.seq.|| is V11() real ext-real non negative 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
r is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V49() V54() set
seq9 . r is V11() real ext-real Element of REAL
abs (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
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 NAT
REAL (n + 1) is non empty functional FinSequence-membered FinSequenceSet of REAL
seq is Relation-like NAT -defined REAL -valued Function-like complex-yielding V36() V37() V49() V56(n + 1) FinSequence-like FinSubsequence-like Element of REAL (n + 1)
|.seq.| is V11() real ext-real non negative Element of REAL
|.seq.| ^2 is V11() real ext-real Element of REAL
K37(|.seq.|,|.seq.|) is V11() real ext-real non negative set
seq | n is Relation-like NAT -defined REAL -valued Function-like complex-yielding V36() V37() V49() FinSequence-like FinSubsequence-like FinSequence of REAL
|.(seq | n).| is V11() real ext-real non negative Element of REAL
|.(seq | n).| ^2 is V11() real ext-real Element of REAL
K37(|.(seq | n).|,|.(seq | n).|) is V11() real ext-real non negative set
seq . (n + 1) is V11() real ext-real Element of REAL
(seq . (n + 1)) ^2 is V11() real ext-real Element of REAL
K37((seq . (n + 1)),(seq . (n + 1))) is V11() real ext-real set
(|.(seq | n).| ^2) + ((seq . (n + 1)) ^2) is V11() real ext-real Element of REAL
seq9 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V33() V34() V49() V54() V158() V159() V160() V161() V162() V163() Element of NAT
seq9 + 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V33() V34() V49() V54() V158() V159() V160() V161() V162() V163() Element of NAT
(seq9 + 1) -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(seq9 + 1) FinSequence-like FinSubsequence-like Element of (seq9 + 1) -tuples_on REAL
r | seq9 is Relation-like NAT -defined REAL -valued Function-like complex-yielding V36() V37() V49() FinSequence-like FinSubsequence-like FinSequence of REAL
Seg seq9 is V49() V56(seq9) V158() V159() V160() V161() V162() V163() Element of bool NAT
r | (Seg seq9) is Relation-like NAT -defined Function-like complex-yielding V36() V37() FinSubsequence-like set
len r is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V33() V34() V49() V54() V158() V159() V160() V161() V162() V163() Element of NAT
Seg (len r) is V49() V56( len r) V158() V159() V160() V161() V162() V163() Element of bool NAT
dom r is V56(seq9 + 1) V158() V159() V160() V161() V162() V163() Element of bool NAT
len (r | seq9) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V33() V34() V49() V54() V158() V159() V160() V161() V162() V163() Element of NAT
seq9 -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
sqr r is Relation-like NAT -defined REAL -valued Function-like complex-yielding V36() V37() V49() V56(seq9 + 1) FinSequence-like FinSubsequence-like Element of (seq9 + 1) -tuples_on REAL
r (#) r is Relation-like NAT -defined Function-like complex-yielding V36() V37() V49() FinSequence-like FinSubsequence-like set
REAL (seq9 + 1) is non empty functional FinSequence-membered FinSequenceSet of REAL
Seg (seq9 + 1) is V49() V56(seq9 + 1) V158() V159() V160() V161() V162() V163() Element of bool NAT
m1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V33() V34() V49() V54() V158() V159() V160() V161() V162() V163() Element of NAT
(sqr r) . m1 is V11() real ext-real Element of REAL
r . m1 is V11() real ext-real Element of REAL
(r . m1) ^2 is V11() real ext-real Element of REAL
K37((r . m1),(r . m1)) is V11() real ext-real set
(r . m1) * (r . m1) is V11() real ext-real Element of REAL
|.r.| is V11() real ext-real non negative Element of REAL
Sum (sqr r) is V11() real ext-real Element of REAL
sqrt (Sum (sqr r)) is V11() real ext-real Element of REAL
|.r.| ^2 is V11() real ext-real Element of REAL
K37(|.r.|,|.r.|) is V11() real ext-real non negative set
sqr (r | seq9) is Relation-like NAT -defined REAL -valued Function-like complex-yielding V36() V37() V49() FinSequence-like FinSubsequence-like FinSequence of REAL
(r | seq9) (#) (r | seq9) is Relation-like NAT -defined Function-like complex-yielding V36() V37() V49() FinSequence-like FinSubsequence-like set
REAL seq9 is non empty functional FinSequence-membered FinSequenceSet of REAL
k is Relation-like NAT -defined REAL -valued Function-like complex-yielding V36() V37() V49() V56(seq9) FinSequence-like FinSubsequence-like Element of seq9 -tuples_on REAL
sqr k is Relation-like NAT -defined REAL -valued Function-like complex-yielding V36() V37() V49() V56(seq9) FinSequence-like FinSubsequence-like Element of seq9 -tuples_on REAL
k (#) k is Relation-like NAT -defined Function-like complex-yielding V36() V37() V49() FinSequence-like FinSubsequence-like set
m1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V33() V34() V49() V54() V158() V159() V160() V161() V162() V163() Element of NAT
(sqr (r | seq9)) . m1 is V11() real ext-real Element of REAL
(sqr k) . m1 is V11() real ext-real Element of REAL
k . m1 is V11() real ext-real Element of REAL
(k . m1) ^2 is V11() real ext-real Element of REAL
K37((k . m1),(k . m1)) is V11() real ext-real set
(k . m1) * (k . m1) is V11() real ext-real Element of REAL
|.(r | seq9).| is V11() real ext-real non negative Element of REAL
Sum (sqr (r | seq9)) is V11() real ext-real Element of REAL
sqrt (Sum (sqr (r | seq9))) is V11() real ext-real Element of REAL
|.(r | seq9).| ^2 is V11() real ext-real Element of REAL
K37(|.(r | seq9).|,|.(r | seq9).|) is V11() real ext-real non negative set
r . (seq9 + 1) is V11() real ext-real Element of REAL
(r . (seq9 + 1)) ^2 is V11() real ext-real Element of REAL
K37((r . (seq9 + 1)),(r . (seq9 + 1))) is V11() real ext-real set
(|.(r | seq9).| ^2) + ((r . (seq9 + 1)) ^2) is V11() real ext-real Element of REAL
(Sum (sqr (r | seq9))) + ((r . (seq9 + 1)) ^2) is V11() real ext-real Element of REAL
r | (seq9 + 1) is Relation-like NAT -defined REAL -valued Function-like complex-yielding V36() V37() V49() FinSequence-like FinSubsequence-like FinSequence of REAL
r | (Seg (seq9 + 1)) is Relation-like NAT -defined Function-like complex-yielding V36() V37() FinSubsequence-like set
<*(r . (seq9 + 1))*> is non empty trivial Relation-like NAT -defined REAL -valued Function-like one-to-one constant complex-yielding V36() V37() V39() V40() V41() V42() V49() V56(1) FinSequence-like FinSubsequence-like FinSequence of REAL
(r | seq9) ^ <*(r . (seq9 + 1))*> is non empty Relation-like NAT -defined REAL -valued Function-like complex-yielding V36() V37() V49() FinSequence-like FinSubsequence-like FinSequence of REAL
<*((r . (seq9 + 1)) ^2)*> is non empty trivial Relation-like NAT -defined REAL -valued Function-like one-to-one constant complex-yielding V36() V37() V39() V40() V41() V42() V49() V56(1) FinSequence-like FinSubsequence-like FinSequence of REAL
(sqr (r | seq9)) ^ <*((r . (seq9 + 1)) ^2)*> is non empty Relation-like NAT -defined REAL -valued Function-like complex-yielding V36() V37() V49() FinSequence-like FinSubsequence-like FinSequence of REAL
k is Relation-like NAT -defined REAL -valued Function-like complex-yielding V36() V37() V49() V56(seq9) FinSequence-like FinSubsequence-like Element of seq9 -tuples_on REAL
mlt (k,k) is Relation-like NAT -defined REAL -valued Function-like complex-yielding V36() V37() V49() V56(seq9) FinSequence-like FinSubsequence-like Element of seq9 -tuples_on REAL
(r . (seq9 + 1)) * (r . (seq9 + 1)) is V11() real ext-real Element of REAL
<*((r . (seq9 + 1)) * (r . (seq9 + 1)))*> is non empty trivial Relation-like NAT -defined REAL -valued Function-like one-to-one constant complex-yielding V36() V37() V39() V40() V41() V42() V49() V56(1) FinSequence-like FinSubsequence-like FinSequence of REAL
(mlt (k,k)) ^ <*((r . (seq9 + 1)) * (r . (seq9 + 1)))*> is non empty Relation-like NAT -defined REAL -valued Function-like complex-yielding V36() V37() V49() V56(seq9 + 1) FinSequence-like FinSubsequence-like FinSequence of REAL
seq9 + 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V33() V34() V49() V54() V158() V159() V160() V161() V162() V163() Element of NAT
k ^ <*(r . (seq9 + 1))*> is non empty Relation-like NAT -defined REAL -valued Function-like complex-yielding V36() V37() V49() V56(seq9 + 1) FinSequence-like FinSubsequence-like FinSequence of REAL
mlt ((k ^ <*(r . (seq9 + 1))*>),((r | seq9) ^ <*(r . (seq9 + 1))*>)) is Relation-like NAT -defined REAL -valued Function-like complex-yielding V36() V37() V49() FinSequence-like FinSubsequence-like FinSequence 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
[:NAT,(REAL n):] is V49() set
bool [:NAT,(REAL n):] is V49() set
seq is non empty Relation-like NAT -defined REAL n -valued Function-like V26( NAT ) V30( NAT , REAL n) V47() V48() Element of bool [:NAT,(REAL n):]
seq9 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V49() V54() set
seq . seq9 is Relation-like NAT -defined Function-like V49() FinSequence-like FinSubsequence-like set
seq . seq9 is Relation-like NAT -defined Function-like 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 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
[:NAT, the carrier of (n):] is V49() set
bool [:NAT, the carrier of (n):] is V49() set
[:NAT,(REAL n):] is V49() set
bool [:NAT,(REAL n):] is V49() set
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 NAT
((n + 1)) 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 + 1)) is non empty set
REAL (n + 1) is non empty functional FinSequence-membered FinSequenceSet of REAL
[:NAT, the carrier of ((n + 1)):] is V49() set
bool [:NAT, the carrier of ((n + 1)):] is V49() set
[:NAT,(REAL (n + 1)):] is V49() set
bool [:NAT,(REAL (n + 1)):] is V49() set
seq9 is Relation-like NAT -defined REAL -valued Function-like complex-yielding V36() V37() V49() V56(n + 1) FinSequence-like FinSubsequence-like Element of REAL (n + 1)
seq is Element of the carrier of ((n + 1))
k is non empty Relation-like NAT -defined REAL (n + 1) -valued Function-like V26( NAT ) V30( NAT , REAL (n + 1)) V47() V48() Element of bool [:NAT,(REAL (n + 1)):]
r is non empty Relation-like NAT -defined the carrier of ((n + 1)) -valued Function-like V26( NAT ) V30( NAT , the carrier of ((n + 1))) Element of bool [:NAT, the carrier of ((n + 1)):]
Seg (n + 1) is V49() V56(n + 1) V158() V159() V160() V161() V162() V163() Element of bool NAT
lim r is Element of the carrier of ((n + 1))
len seq9 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V33() V34() V49() V54() V158() V159() V160() V161() V162() V163() Element of NAT
seq9 | n is Relation-like NAT -defined REAL -valued Function-like complex-yielding V36() V37() V49() FinSequence-like FinSubsequence-like FinSequence of REAL
len (seq9 | n) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V33() V34() V49() V54() V158() V159() V160() V161() V162() V163() Element of NAT
dom (seq9 | n) is V158() V159() V160() V161() V162() V163() Element of bool NAT
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
r - seq is non empty Relation-like NAT -defined the carrier of ((n + 1)) -valued Function-like V26( NAT ) V30( NAT , the carrier of ((n + 1))) Element of bool [:NAT, the carrier of ((n + 1)):]
||.(r - seq).|| is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-yielding V36() V37() Element of bool [:NAT,REAL:]
||.(r - seq).|| (#) ||.(r - seq).|| is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-yielding V36() V37() Element of bool [:NAT,REAL:]
seq9 . (n + 1) is V11() real ext-real Element of REAL
k is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-yielding V36() V37() Element of bool [:NAT,REAL:]
lim k is V11() real ext-real Element of REAL
p 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 + 1),k,p) is Relation-like NAT -defined REAL -valued Function-like complex-yielding V36() V37() V49() V56(n + 1) FinSequence-like FinSubsequence-like Element of REAL (n + 1)
((n + 1),k,p) | n is Relation-like NAT -defined REAL -valued Function-like complex-yielding V36() V37() V49() FinSequence-like FinSubsequence-like FinSequence of REAL
b is Relation-like NAT -defined REAL -valued Function-like complex-yielding V36() V37() V49() FinSequence-like FinSubsequence-like FinSequence of REAL
len ((n + 1),k,p) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V33() V34() V49() V54() V158() V159() V160() V161() V162() V163() Element of NAT
len (((n + 1),k,p) | n) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V33() V34() V49() V54() V158() V159() V160() V161() V162() V163() Element of NAT
dom (((n + 1),k,p) | n) is V158() V159() V160() V161() V162() V163() Element of bool NAT
p is non empty Relation-like NAT -defined REAL n -valued Function-like V26( NAT ) V30( NAT , REAL n) V47() V48() Element of bool [:NAT,(REAL n):]
b is non empty Relation-like NAT -defined the carrier of (n) -valued Function-like V26( NAT ) V30( NAT , the carrier of (n)) Element of bool [:NAT, the carrier of (n):]
m2 is Element of the carrier of (n)
b - m2 is non empty Relation-like NAT -defined the carrier of (n) -valued Function-like V26( NAT ) V30( NAT , the carrier of (n)) Element of bool [:NAT, the carrier of (n):]
||.(b - m2).|| is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-yielding V36() V37() Element of bool [:NAT,REAL:]
||.(b - m2).|| (#) ||.(b - m2).|| is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-yielding V36() V37() Element of bool [:NAT,REAL:]
k is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-yielding V36() V37() Element of bool [:NAT,REAL:]
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V33() V34() V49() V54() V158() V159() V160() V161() V162() V163() Element of NAT
m1 . k is V11() real ext-real Element of REAL
seq9 . k is V11() real ext-real Element of REAL
e is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-yielding V36() V37() Element of bool [:NAT,REAL:]
lim e is V11() real ext-real Element of REAL
m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V33() V34() V49() V54() V158() V159() V160() V161() V162() V163() Element of NAT
e . m is V11() real ext-real Element of REAL
((n + 1),k,m) is Relation-like NAT -defined REAL -valued Function-like complex-yielding V36() V37() V49() V56(n + 1) FinSequence-like FinSubsequence-like Element of REAL (n + 1)
((n + 1),k,m) . k is V11() real ext-real Element of REAL
((n + 1),k,m) | (Seg n) is Relation-like NAT -defined Function-like complex-yielding V36() V37() FinSubsequence-like set
(((n + 1),k,m) | (Seg n)) . k is V11() real ext-real Element of REAL
((n + 1),k,m) | n is Relation-like NAT -defined REAL -valued Function-like complex-yielding V36() V37() V49() FinSequence-like FinSubsequence-like FinSequence of REAL
(((n + 1),k,m) | n) . k is V11() real ext-real Element of REAL
(n,p,m) 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,p,m) . k is V11() real ext-real Element of REAL
seq9 | (Seg n) is Relation-like NAT -defined Function-like complex-yielding V36() V37() FinSubsequence-like set
(seq9 | (Seg n)) . k is V11() real ext-real Element of REAL
lim b is Element of the carrier of (n)
k (#) k is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-yielding V36() V37() Element of bool [:NAT,REAL:]
(n + 1) -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V33() V34() V49() V54() V158() V159() V160() V161() V162() V163() Element of NAT
||.(r - seq).|| . m is V11() real ext-real Element of REAL
(r - seq) . m is Element of the carrier of ((n + 1))
||.((r - seq) . m).|| is V11() real ext-real non negative Element of REAL
the normF of ((n + 1)) is non empty Relation-like the carrier of ((n + 1)) -defined REAL -valued Function-like V26( the carrier of ((n + 1))) V30( the carrier of ((n + 1)), REAL ) complex-yielding V36() V37() Element of bool [: the carrier of ((n + 1)),REAL:]
[: the carrier of ((n + 1)),REAL:] is complex-yielding V36() V37() V49() set
bool [: the carrier of ((n + 1)),REAL:] is V49() set
the normF of ((n + 1)) . ((r - seq) . m) is V11() real ext-real Element of REAL
r . m is Element of the carrier of ((n + 1))
(r . m) - seq is Element of the carrier of ((n + 1))
- seq is Element of the carrier of ((n + 1))
(r . m) + (- seq) is Element of the carrier of ((n + 1))
the addF of ((n + 1)) is Relation-like [: the carrier of ((n + 1)), the carrier of ((n + 1)):] -defined the carrier of ((n + 1)) -valued Function-like V26([: the carrier of ((n + 1)), the carrier of ((n + 1)):]) V30([: the carrier of ((n + 1)), the carrier of ((n + 1)):], the carrier of ((n + 1))) Element of bool [:[: the carrier of ((n + 1)), the carrier of ((n + 1)):], the carrier of ((n + 1)):]
[: the carrier of ((n + 1)), the carrier of ((n + 1)):] is set
[:[: the carrier of ((n + 1)), the carrier of ((n + 1)):], the carrier of ((n + 1)):] is set
bool [:[: the carrier of ((n + 1)), the carrier of ((n + 1)):], the carrier of ((n + 1)):] is set
the addF of ((n + 1)) . ((r . m),(- seq)) is Element of the carrier of ((n + 1))
[(r . m),(- seq)] is set
the addF of ((n + 1)) . [(r . m),(- seq)] is set
||.((r . m) - seq).|| is V11() real ext-real non negative Element of REAL
the normF of ((n + 1)) . ((r . m) - seq) is V11() real ext-real Element of REAL
((n + 1),k,m) is Relation-like NAT -defined REAL -valued Function-like complex-yielding V36() V37() V49() V56(n + 1) FinSequence-like FinSubsequence-like Element of REAL (n + 1)
||.(b - m2).|| . m is V11() real ext-real Element of REAL
(b - m2) . m is Element of the carrier of (n)
||.((b - m2) . m).|| is V11() real ext-real non negative 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) . ((b - m2) . m) is V11() real ext-real Element of REAL
b . m is Element of the carrier of (n)
(b . m) - m2 is Element of the carrier of (n)
- m2 is Element of the carrier of (n)
(b . m) + (- 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) . ((b . m),(- m2)) is Element of the carrier of (n)
[(b . m),(- m2)] is set
the addF of (n) . [(b . m),(- m2)] is set
||.((b . m) - m2).|| is V11() real ext-real non negative Element of REAL
the normF of (n) . ((b . m) - m2) is V11() real ext-real Element of REAL
(n,p,m) 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,p,m) - 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 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) (#) m1 is Relation-like NAT -defined Function-like complex-yielding V36() V37() V49() FinSequence-like FinSubsequence-like set
(n,p,m) + (- m1) is Relation-like NAT -defined Function-like complex-yielding V36() V37() V49() FinSequence-like FinSubsequence-like set
len ((n,p,m) - m1) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V33() V34() V49() V54() V158() V159() V160() V161() V162() V163() Element of NAT
dom ((n,p,m) - m1) is V56(n) V158() V159() V160() V161() V162() V163() Element of bool NAT
((n + 1),k,m) - seq9 is Relation-like NAT -defined REAL -valued Function-like complex-yielding V36() V37() V49() V56(n + 1) FinSequence-like FinSubsequence-like Element of REAL (n + 1)
- seq9 is Relation-like NAT -defined Function-like complex-yielding V36() V37() V49() FinSequence-like FinSubsequence-like set
K38(1) (#) seq9 is Relation-like NAT -defined Function-like complex-yielding V36() V37() V49() FinSequence-like FinSubsequence-like set
((n + 1),k,m) + (- seq9) is Relation-like NAT -defined Function-like complex-yielding V36() V37() V49() FinSequence-like FinSubsequence-like set
(((n + 1),k,m) - seq9) . (n + 1) 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 + 1) FinSequence-like FinSubsequence-like Element of (n + 1) -tuples_on REAL
k . (n + 1) is V11() real ext-real Element of REAL
e is Relation-like NAT -defined REAL -valued Function-like complex-yielding V36() V37() V49() V56(n + 1) FinSequence-like FinSubsequence-like Element of (n + 1) -tuples_on REAL
e . (n + 1) is V11() real ext-real Element of REAL
(k . (n + 1)) - (e . (n + 1)) is V11() real ext-real Element of REAL
k . m is V11() real ext-real Element of REAL
(k . m) - (seq9 . (n + 1)) is V11() real ext-real Element of REAL
len (((n + 1),k,m) - seq9) 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 + 1),k,m) - seq9) | n is Relation-like NAT -defined REAL -valued Function-like complex-yielding V36() V37() V49() FinSequence-like FinSubsequence-like FinSequence of REAL
len ((((n + 1),k,m) - seq9) | n) 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
i is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V49() V54() set
dom ((((n + 1),k,m) - seq9) | n) is V158() V159() V160() V161() V162() V163() Element of bool NAT
((n,p,m) - m1) . i is V11() real ext-real Element of REAL
xseq2 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
xseq2 . i is V11() real ext-real Element of REAL
xs2 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
xs2 . i is V11() real ext-real Element of REAL
(xseq2 . i) - (xs2 . i) is V11() real ext-real Element of REAL
(((n + 1),k,m) - seq9) . i is V11() real ext-real Element of REAL
xseq1 is Relation-like NAT -defined REAL -valued Function-like complex-yielding V36() V37() V49() V56(n + 1) FinSequence-like FinSubsequence-like Element of (n + 1) -tuples_on REAL
xseq1 . i is V11() real ext-real Element of REAL
xs1 is Relation-like NAT -defined REAL -valued Function-like complex-yielding V36() V37() V49() V56(n + 1) FinSequence-like FinSubsequence-like Element of (n + 1) -tuples_on REAL
xs1 . i is V11() real ext-real Element of REAL
(xseq1 . i) - (xs1 . i) is V11() real ext-real Element of REAL
((((n + 1),k,m) - seq9) | n) . i is V11() real ext-real Element of REAL
(((n + 1),k,m) - seq9) | (Seg n) is Relation-like NAT -defined Function-like complex-yielding V36() V37() FinSubsequence-like set
((((n + 1),k,m) - seq9) | (Seg n)) . i is V11() real ext-real Element of REAL
((n + 1),k,m) | (Seg n) is Relation-like NAT -defined Function-like complex-yielding V36() V37() FinSubsequence-like set
(((n + 1),k,m) | (Seg n)) . i is V11() real ext-real Element of REAL
seq9 . i is V11() real ext-real Element of REAL
((((n + 1),k,m) | (Seg n)) . i) - (seq9 . i) is V11() real ext-real Element of REAL
seq9 | (Seg n) is Relation-like NAT -defined Function-like complex-yielding V36() V37() FinSubsequence-like set
(seq9 | (Seg n)) . i is V11() real ext-real Element of REAL
((((n + 1),k,m) | (Seg n)) . i) - ((seq9 | (Seg n)) . i) is V11() real ext-real Element of REAL
((n + 1),k,m) | n is Relation-like NAT -defined REAL -valued Function-like complex-yielding V36() V37() V49() FinSequence-like FinSubsequence-like FinSequence of REAL
(((n + 1),k,m) | n) . i is V11() real ext-real Element of REAL
((((n + 1),k,m) | n) . i) - ((seq9 | (Seg n)) . i) is V11() real ext-real Element of REAL
(seq9 | n) . i is V11() real ext-real Element of REAL
((((n + 1),k,m) | n) . i) - ((seq9 | n) . i) is V11() real ext-real Element of REAL
((k . m) - (seq9 . (n + 1))) ^2 is V11() real ext-real Element of REAL
K37(((k . m) - (seq9 . (n + 1))),((k . m) - (seq9 . (n + 1)))) is V11() real ext-real set
k . m is V11() real ext-real Element of REAL
abs ((k . m) - (seq9 . (n + 1))) is V11() real ext-real Element of REAL
|.(((n + 1),k,m) - seq9).| is V11() real ext-real non negative Element of REAL
(||.(r - seq).|| (#) ||.(r - seq).||) . m is V11() real ext-real Element of REAL
|.(((n + 1),k,m) - seq9).| ^2 is V11() real ext-real Element of REAL
K37(|.(((n + 1),k,m) - seq9).|,|.(((n + 1),k,m) - seq9).|) is V11() real ext-real non negative set
|.((n,p,m) - m1).| is V11() real ext-real non negative Element of REAL
|.((n,p,m) - m1).| ^2 is V11() real ext-real Element of REAL
K37(|.((n,p,m) - m1).|,|.((n,p,m) - m1).|) is V11() real ext-real non negative set
(|.((n,p,m) - m1).| ^2) + (((k . m) - (seq9 . (n + 1))) ^2) is V11() real ext-real Element of REAL
||.((b . m) - m2).|| ^2 is V11() real ext-real Element of REAL
K37(||.((b . m) - m2).||,||.((b . m) - m2).||) is V11() real ext-real non negative set
(||.((b . m) - m2).|| ^2) + (((k . m) - (seq9 . (n + 1))) ^2) is V11() real ext-real Element of REAL
(||.(b - m2).|| (#) ||.(b - m2).||) . m is V11() real ext-real Element of REAL
((||.(b - m2).|| (#) ||.(b - m2).||) . m) + (((k . m) - (seq9 . (n + 1))) ^2) is V11() real ext-real Element of REAL
((k . m) - (seq9 . (n + 1))) * ((k . m) - (seq9 . (n + 1))) is V11() real ext-real Element of REAL
abs (((k . m) - (seq9 . (n + 1))) * ((k . m) - (seq9 . (n + 1)))) is V11() real ext-real Element of REAL
((||.(b - m2).|| (#) ||.(b - m2).||) . m) + (abs (((k . m) - (seq9 . (n + 1))) * ((k . m) - (seq9 . (n + 1))))) is V11() real ext-real Element of REAL
(abs ((k . m) - (seq9 . (n + 1)))) * (abs ((k . m) - (seq9 . (n + 1)))) is V11() real ext-real Element of REAL
((||.(b - m2).|| (#) ||.(b - m2).||) . m) + ((abs ((k . m) - (seq9 . (n + 1)))) * (abs ((k . m) - (seq9 . (n + 1))))) is V11() real ext-real Element of REAL
(k (#) k) . m is V11() real ext-real Element of REAL
((||.(b - m2).|| (#) ||.(b - m2).||) . m) + ((k (#) k) . m) is V11() real ext-real Element of REAL
(||.(b - m2).|| (#) ||.(b - m2).||) + (k (#) k) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-yielding V36() V37() Element of bool [:NAT,REAL:]
e is V11() real ext-real set
m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V33() V34() V49() V54() V158() V159() V160() V161() V162() V163() Element of NAT
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V33() V34() V49() V54() V158() V159() V160() V161() V162() V163() Element of NAT
k . k is V11() real ext-real Element of REAL
(k . k) - (seq9 . (n + 1)) is V11() real ext-real Element of REAL
abs ((k . k) - (seq9 . (n + 1))) is V11() real ext-real Element of REAL
(abs ((k . k) - (seq9 . (n + 1)))) - 0 is V11() real ext-real Element of REAL
abs ((abs ((k . k) - (seq9 . (n + 1)))) - 0) is V11() real ext-real Element of REAL
k . k is V11() real ext-real Element of REAL
(k . k) - 0 is V11() real ext-real Element of REAL
abs ((k . k) - 0) is V11() real ext-real Element of REAL
lim k is V11() real ext-real Element of REAL
lim (k (#) k) is V11() real ext-real Element of REAL
0 * 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
lim ||.(b - m2).|| is V11() real ext-real Element of REAL
lim (||.(b - m2).|| (#) ||.(b - m2).||) is V11() real ext-real Element of REAL
lim (||.(r - seq).|| (#) ||.(r - seq).||) is V11() real ext-real Element of REAL
0 + 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
e is V11() real ext-real Element of REAL
e * e is V11() real ext-real Element of REAL
e * 0 is V11() real ext-real Element of REAL
m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V33() V34() V49() V54() V158() V159() V160() V161() V162() V163() Element of NAT
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V33() V34() V49() V54() V158() V159() V160() V161() V162() V163() Element of NAT
||.(r - seq).|| . k is V11() real ext-real Element of REAL
(r - seq) . k is Element of the carrier of ((n + 1))
||.((r - seq) . k).|| is V11() real ext-real non negative Element of REAL
the normF of ((n + 1)) . ((r - seq) . k) is V11() real ext-real Element of REAL
r . k is Element of the carrier of ((n + 1))
(r . k) - seq is Element of the carrier of ((n + 1))
(r . k) + (- seq) is Element of the carrier of ((n + 1))
the addF of ((n + 1)) . ((r . k),(- seq)) is Element of the carrier of ((n + 1))
[(r . k),(- seq)] is set
the addF of ((n + 1)) . [(r . k),(- seq)] is set
||.((r . k) - seq).|| is V11() real ext-real non negative Element of REAL
the normF of ((n + 1)) . ((r . k) - seq) is V11() real ext-real Element of REAL
(||.(r - seq).|| (#) ||.(r - seq).||) . k is V11() real ext-real Element of REAL
||.((r . k) - seq).|| * ||.((r . k) - seq).|| is V11() real ext-real non negative Element of REAL
((||.(r - seq).|| (#) ||.(r - seq).||) . k) - 0 is V11() real ext-real Element of REAL
abs (((||.(r - seq).|| (#) ||.(r - seq).||) . k) - 0) is V11() real ext-real Element of REAL
sqrt (||.((r . k) - seq).|| * ||.((r . k) - seq).||) is V11() real ext-real Element of REAL
||.((r . k) - seq).|| ^2 is V11() real ext-real Element of REAL
K37(||.((r . k) - seq).||,||.((r . k) - seq).||) is V11() real ext-real non negative set
sqrt (||.((r . k) - seq).|| ^2) is V11() real ext-real Element of REAL
sqrt (e * e) is V11() real ext-real Element of REAL
e ^2 is V11() real ext-real Element of REAL
K37(e,e) is V11() real ext-real set
sqrt (e ^2) is V11() real ext-real Element of REAL
m1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V33() V34() V49() V54() V158() V159() V160() V161() V162() V163() Element of NAT
m2 is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-yielding V36() V37() Element of bool [:NAT,REAL:]
p is V11() real ext-real set
seq9 . m1 is V11() real ext-real Element of REAL
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V33() V34() V49() V54() V158() V159() V160() V161() V162() V163() Element of NAT
p is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V33() V34() V49() V54() V158() V159() V160() V161() V162() V163() Element of NAT
m2 . p is V11() real ext-real Element of REAL
(m2 . p) - (seq9 . m1) is V11() real ext-real Element of REAL
abs ((m2 . p) - (seq9 . m1)) is V11() real ext-real Element of REAL
r . p is Element of the carrier of ((n + 1))
(r . p) - seq is Element of the carrier of ((n + 1))
- seq is Element of the carrier of ((n + 1))
(r . p) + (- seq) is Element of the carrier of ((n + 1))
the addF of ((n + 1)) is Relation-like [: the carrier of ((n + 1)), the carrier of ((n + 1)):] -defined the carrier of ((n + 1)) -valued Function-like V26([: the carrier of ((n + 1)), the carrier of ((n + 1)):]) V30([: the carrier of ((n + 1)), the carrier of ((n + 1)):], the carrier of ((n + 1))) Element of bool [:[: the carrier of ((n + 1)), the carrier of ((n + 1)):], the carrier of ((n + 1)):]
[: the carrier of ((n + 1)), the carrier of ((n + 1)):] is set
[:[: the carrier of ((n + 1)), the carrier of ((n + 1)):], the carrier of ((n + 1)):] is set
bool [:[: the carrier of ((n + 1)), the carrier of ((n + 1)):], the carrier of ((n + 1)):] is set
the addF of ((n + 1)) . ((r . p),(- seq)) is Element of the carrier of ((n + 1))
[(r . p),(- seq)] is set
the addF of ((n + 1)) . [(r . p),(- seq)] is set
||.((r . p) - seq).|| is V11() real ext-real non negative Element of REAL
the normF of ((n + 1)) is non empty Relation-like the carrier of ((n + 1)) -defined REAL -valued Function-like V26( the carrier of ((n + 1))) V30( the carrier of ((n + 1)), REAL ) complex-yielding V36() V37() Element of bool [: the carrier of ((n + 1)),REAL:]
[: the carrier of ((n + 1)),REAL:] is complex-yielding V36() V37() V49() set
bool [: the carrier of ((n + 1)),REAL:] is V49() set
the normF of ((n + 1)) . ((r . p) - seq) is V11() real ext-real Element of REAL
((n + 1),k,p) is Relation-like NAT -defined REAL -valued Function-like complex-yielding V36() V37() V49() V56(n + 1) FinSequence-like FinSubsequence-like Element of REAL (n + 1)
((n + 1),k,p) - seq9 is Relation-like NAT -defined REAL -valued Function-like complex-yielding V36() V37() V49() V56(n + 1) FinSequence-like FinSubsequence-like Element of REAL (n + 1)
- seq9 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) (#) seq9 is Relation-like NAT -defined Function-like complex-yielding V36() V37() V49() FinSequence-like FinSubsequence-like set
((n + 1),k,p) + (- seq9) is Relation-like NAT -defined Function-like complex-yielding V36() V37() V49() FinSequence-like FinSubsequence-like set
len (((n + 1),k,p) - seq9) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V33() V34() V49() V54() V158() V159() V160() V161() V162() V163() Element of NAT
dom (((n + 1),k,p) - seq9) is V56(n + 1) V158() V159() V160() V161() V162() V163() Element of bool NAT
((n + 1),k,p) . m1 is V11() real ext-real Element of REAL
(((n + 1),k,p) . m1) - (seq9 . m1) is V11() real ext-real Element of REAL
(((n + 1),k,p) - seq9) . m1 is V11() real ext-real Element of REAL
abs ((((n + 1),k,p) . m1) - (seq9 . m1)) is V11() real ext-real Element of REAL
lim m2 is V11() real ext-real Element of REAL
m1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V33() V34() V49() V54() V158() V159() V160() V161() V162() V163() Element of NAT
seq9 . m1 is V11() real ext-real Element of REAL
m1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V33() V34() V49() V54() V158() V159() V160() V161() V162() V163() Element of NAT
seq9 . m1 is V11() real ext-real Element of REAL
m2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V33() V34() V49() V54() V158() V159() V160() V161() V162() V163() Element of NAT
seq9 . m2 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 + 1) FinSequence-like FinSubsequence-like Element of REAL (n + 1)
seq is Element of the carrier of ((n + 1))
k is non empty Relation-like NAT -defined REAL (n + 1) -valued Function-like V26( NAT ) V30( NAT , REAL (n + 1)) V47() V48() Element of bool [:NAT,(REAL (n + 1)):]
r is non empty Relation-like NAT -defined the carrier of ((n + 1)) -valued Function-like V26( NAT ) V30( NAT , the carrier of ((n + 1))) Element of bool [:NAT, the carrier of ((n + 1)):]
lim r is Element of the carrier of ((n + 1))
m1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V33() V34() V49() V54() V158() V159() V160() V161() V162() V163() Element of NAT
seq9 . m1 is V11() real ext-real Element of REAL
(0) 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 (0) is non empty set
REAL 0 is non empty functional FinSequence-membered FinSequenceSet of REAL
[:NAT, the carrier of (0):] is V49() set
bool [:NAT, the carrier of (0):] is V49() set
[:NAT,(REAL 0):] is V49() set
bool [:NAT,(REAL 0):] is V49() set
Seg 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 V49() V54() V56( 0 ) V56( {} ) FinSequence-membered V158() V159() V160() V161() V162() V163() V164() Element of bool NAT
n is Element of the carrier of (0)
seq 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( 0 ) FinSequence-like FinSubsequence-like FinSequence-membered V158() V159() V160() V161() V162() V163() V164() Element of REAL 0
seq9 is non empty Relation-like NAT -defined the carrier of (0) -valued Function-like V26( NAT ) V30( NAT , the carrier of (0)) Element of bool [:NAT, the carrier of (0):]
lim seq9 is Element of the carrier of (0)
r is non empty Relation-like NAT -defined REAL 0 -valued Function-like V26( NAT ) V30( NAT , REAL 0) V47() V48() Element of bool [:NAT,(REAL 0):]
0. (0) is V69((0)) Element of the carrier of (0)
the ZeroF of (0) is Element of the carrier of (0)
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V33() V34() V49() V54() V158() V159() V160() V161() V162() V163() Element of NAT
seq9 . k is Element of the carrier of (0)
(0,r,k) 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( 0 ) FinSequence-like FinSubsequence-like FinSequence-membered V158() V159() V160() V161() V162() V163() V164() Element of REAL 0
0.REAL 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 V37() V49() V54() V56( 0 ) FinSequence-like FinSequence-membered V158() V159() V160() V161() V162() V163() V164() Element of the carrier of (TOP-REAL 0)
TOP-REAL 0 is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital TopSpace-like V200() L20()
the carrier of (TOP-REAL 0) is non empty set
0* 0 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( 0 ) FinSequence-like FinSubsequence-like FinSequence-membered V158() V159() V160() V161() V162() V163() V164() Element of REAL 0
k is V11() real ext-real Element of REAL
m1 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
m2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V33() V34() V49() V54() V158() V159() V160() V161() V162() V163() Element of NAT
seq9 . m2 is Element of the carrier of (0)
(seq9 . m2) - n is Element of the carrier of (0)
- n is Element of the carrier of (0)
(seq9 . m2) + (- n) is Element of the carrier of (0)
the addF of (0) is Relation-like [: the carrier of (0), the carrier of (0):] -defined the carrier of (0) -valued Function-like V26([: the carrier of (0), the carrier of (0):]) V30([: the carrier of (0), the carrier of (0):], the carrier of (0)) Element of bool [:[: the carrier of (0), the carrier of (0):], the carrier of (0):]
[: the carrier of (0), the carrier of (0):] is set
[:[: the carrier of (0), the carrier of (0):], the carrier of (0):] is set
bool [:[: the carrier of (0), the carrier of (0):], the carrier of (0):] is set
the addF of (0) . ((seq9 . m2),(- n)) is Element of the carrier of (0)
[(seq9 . m2),(- n)] is set
the addF of (0) . [(seq9 . m2),(- n)] is set
||.((seq9 . m2) - n).|| is V11() real ext-real non negative Element of REAL
the normF of (0) is non empty Relation-like the carrier of (0) -defined REAL -valued Function-like V26( the carrier of (0)) V30( the carrier of (0), REAL ) complex-yielding V36() V37() Element of bool [: the carrier of (0),REAL:]
[: the carrier of (0),REAL:] is complex-yielding V36() V37() V49() set
bool [: the carrier of (0),REAL:] is V49() set
the normF of (0) . ((seq9 . m2) - n) is V11() real ext-real Element of REAL
(0. (0)) - (0. (0)) is Element of the carrier of (0)
- (0. (0)) is Element of the carrier of (0)
(0. (0)) + (- (0. (0))) is Element of the carrier of (0)
the addF of (0) . ((0. (0)),(- (0. (0)))) is Element of the carrier of (0)
[(0. (0)),(- (0. (0)))] is set
the addF of (0) . [(0. (0)),(- (0. (0)))] is set
||.((0. (0)) - (0. (0))).|| is V11() real ext-real non negative Element of REAL
the normF of (0) . ((0. (0)) - (0. (0))) is V11() real ext-real Element of REAL
||.(0. (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 V49() V54() V56( {} ) FinSequence-membered V158() V159() V160() V161() V162() V163() V164() Element of REAL
the normF of (0) . (0. (0)) is V11() real ext-real Element of REAL
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V33() V34() V49() V54() V158() V159() V160() V161() V162() V163() Element of NAT
seq . k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real Relation-like Function-like V49() V54() Element of REAL
m1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V33() V34() V49() V54() V158() V159() V160() V161() V162() V163() Element of NAT
seq . m1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real Relation-like Function-like V49() V54() Element of 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
[:NAT, the carrier of (n):] is V49() set
bool [:NAT, the carrier of (n):] is V49() set
seq is non empty Relation-like NAT -defined the carrier of (n) -valued Function-like V26( NAT ) V30( NAT , the carrier of (n)) Element of bool [:NAT, the carrier of (n):]
REAL n is non empty functional FinSequence-membered FinSequenceSet of REAL
[:NAT,(REAL n):] is V49() set
bool [:NAT,(REAL n):] is V49() set
seq9 is non empty Relation-like NAT -defined REAL n -valued Function-like V26( NAT ) V30( NAT , REAL n) V47() V48() Element of bool [:NAT,(REAL n):]
Seg n is V49() V56(n) V158() V159() V160() V161() V162() V163() Element of bool NAT
r is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V49() V54() set
k is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-yielding V36() V37() Element of bool [:NAT,REAL:]
lim k is V11() real ext-real Element of REAL
m1 is V11() real ext-real set
m2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V33() V34() V49() V54() V158() V159() V160() V161() V162() V163() Element of NAT
k . m2 is V11() real ext-real Element of REAL
p is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V33() V34() V49() V54() V158() V159() V160() V161() V162() V163() Element of NAT
k . p is V11() real ext-real Element of REAL
(k . p) - (k . m2) is V11() real ext-real Element of REAL
abs ((k . p) - (k . m2)) is V11() real ext-real Element of REAL
seq . p is Element of the carrier of (n)
seq . m2 is Element of the carrier of (n)
(seq . p) - (seq . m2) is Element of the carrier of (n)
- (seq . m2) is Element of the carrier of (n)
(seq . p) + (- (seq . 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) . ((seq . p),(- (seq . m2))) is Element of the carrier of (n)
[(seq . p),(- (seq . m2))] is set
the addF of (n) . [(seq . p),(- (seq . m2))] is set
||.((seq . p) - (seq . m2)).|| is V11() real ext-real non negative 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 . p) - (seq . m2)) is V11() real ext-real Element of REAL
(n,seq9,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,seq9,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
(n,seq9,p) - (n,seq9,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
- (n,seq9,m2) 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) (#) (n,seq9,m2) is Relation-like NAT -defined Function-like complex-yielding V36() V37() V49() FinSequence-like FinSubsequence-like set
(n,seq9,p) + (- (n,seq9,m2)) is Relation-like NAT -defined Function-like complex-yielding V36() V37() V49() FinSequence-like FinSubsequence-like set
len ((n,seq9,p) - (n,seq9,m2)) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V33() V34() V49() V54() V158() V159() V160() V161() V162() V163() Element of NAT
dom ((n,seq9,p) - (n,seq9,m2)) is V56(n) V158() V159() V160() V161() V162() V163() Element of bool NAT
(n,seq9,p) . r is V11() real ext-real Element of REAL
(n,seq9,m2) . r is V11() real ext-real Element of REAL
((n,seq9,p) . r) - ((n,seq9,m2) . r) is V11() real ext-real Element of REAL
((n,seq9,p) - (n,seq9,m2)) . r is V11() real ext-real Element of REAL
abs (((n,seq9,p) . r) - ((n,seq9,m2) . r)) is V11() real ext-real Element of REAL
r is Relation-like NAT -defined REAL -valued Function-like complex-yielding V36() V37() V49() FinSequence-like FinSubsequence-like FinSequence of REAL
dom r is V158() V159() V160() V161() V162() V163() Element of bool NAT
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 Element of the carrier of (n)
m2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V33() V34() V49() V54() V158() V159() V160() V161() V162() V163() Element of NAT
r . m2 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 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
[:NAT, the carrier of (n):] is V49() set
bool [:NAT, the carrier of (n):] is V49() set
seq is non empty Relation-like NAT -defined the carrier of (n) -valued Function-like V26( NAT ) V30( NAT , the carrier of (n)) Element of bool [:NAT, the carrier of (n):]
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
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:] is complex-yielding V36() V37() set
bool [:[:(REAL n),(REAL n):],REAL:] is set
seq is Relation-like [:(REAL n),(REAL n):] -defined REAL -valued Function-like V26([:(REAL n),(REAL n):]) V30([:(REAL n),(REAL n):], REAL ) complex-yielding V36() V37() Element of bool [:[:(REAL n),(REAL n):],REAL:]
seq is Relation-like [:(REAL n),(REAL n):] -defined REAL -valued Function-like V26([:(REAL n),(REAL n):]) V30([:(REAL n),(REAL n):], REAL ) complex-yielding V36() V37() Element of bool [:[:(REAL n),(REAL n):],REAL:]
seq9 is Relation-like [:(REAL n),(REAL n):] -defined REAL -valued Function-like V26([:(REAL n),(REAL n):]) V30([:(REAL n),(REAL n):], REAL ) complex-yielding V36() V37() Element of bool [:[:(REAL n),(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
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 V11() real ext-real Element of REAL
[r,k] is set
seq . [r,k] is V11() real ext-real set
seq9 . (r,k) is V11() real ext-real Element of REAL
seq9 . [r,k] is V11() real ext-real set
mlt (r,k) is Relation-like NAT -defined REAL -valued Function-like complex-yielding V36() V37() V49() FinSequence-like FinSubsequence-like FinSequence of REAL
Sum (mlt (r,k)) 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 Relation-like [:(REAL n),(REAL n):] -defined REAL -valued Function-like V26([:(REAL n),(REAL n):]) V30([:(REAL n),(REAL n):], REAL ) complex-yielding V36() V37() Element of bool [:[:(REAL n),(REAL n):],REAL:]
[:[:(REAL n),(REAL n):],REAL:] is complex-yielding V36() V37() set
bool [:[:(REAL n),(REAL n):],REAL:] is set
UNITSTR(# (REAL n),(0* n),(n),(n),(n) #) is non empty strict UNITSTR
the carrier of UNITSTR(# (REAL n),(0* n),(n),(n),(n) #) is non empty set
0. UNITSTR(# (REAL n),(0* n),(n),(n),(n) #) is V69( UNITSTR(# (REAL n),(0* n),(n),(n),(n) #)) Element of the carrier of UNITSTR(# (REAL n),(0* n),(n),(n),(n) #)
the ZeroF of UNITSTR(# (REAL n),(0* n),(n),(n),(n) #) is Element of the carrier of UNITSTR(# (REAL n),(0* n),(n),(n),(n) #)
[: the carrier of UNITSTR(# (REAL n),(0* n),(n),(n),(n) #), the carrier of UNITSTR(# (REAL n),(0* n),(n),(n),(n) #):] is set
the addF of UNITSTR(# (REAL n),(0* n),(n),(n),(n) #) is Relation-like [: the carrier of UNITSTR(# (REAL n),(0* n),(n),(n),(n) #), the carrier of UNITSTR(# (REAL n),(0* n),(n),(n),(n) #):] -defined the carrier of UNITSTR(# (REAL n),(0* n),(n),(n),(n) #) -valued Function-like V26([: the carrier of UNITSTR(# (REAL n),(0* n),(n),(n),(n) #), the carrier of UNITSTR(# (REAL n),(0* n),(n),(n),(n) #):]) V30([: the carrier of UNITSTR(# (REAL n),(0* n),(n),(n),(n) #), the carrier of UNITSTR(# (REAL n),(0* n),(n),(n),(n) #):], the carrier of UNITSTR(# (REAL n),(0* n),(n),(n),(n) #)) Element of bool [:[: the carrier of UNITSTR(# (REAL n),(0* n),(n),(n),(n) #), the carrier of UNITSTR(# (REAL n),(0* n),(n),(n),(n) #):], the carrier of UNITSTR(# (REAL n),(0* n),(n),(n),(n) #):]
[:[: the carrier of UNITSTR(# (REAL n),(0* n),(n),(n),(n) #), the carrier of UNITSTR(# (REAL n),(0* n),(n),(n),(n) #):], the carrier of UNITSTR(# (REAL n),(0* n),(n),(n),(n) #):] is set
bool [:[: the carrier of UNITSTR(# (REAL n),(0* n),(n),(n),(n) #), the carrier of UNITSTR(# (REAL n),(0* n),(n),(n),(n) #):], the carrier of UNITSTR(# (REAL n),(0* n),(n),(n),(n) #):] is set
[:REAL, the carrier of UNITSTR(# (REAL n),(0* n),(n),(n),(n) #):] is V49() set
the Mult of UNITSTR(# (REAL n),(0* n),(n),(n),(n) #) is Relation-like [:REAL, the carrier of UNITSTR(# (REAL n),(0* n),(n),(n),(n) #):] -defined the carrier of UNITSTR(# (REAL n),(0* n),(n),(n),(n) #) -valued Function-like V26([:REAL, the carrier of UNITSTR(# (REAL n),(0* n),(n),(n),(n) #):]) V30([:REAL, the carrier of UNITSTR(# (REAL n),(0* n),(n),(n),(n) #):], the carrier of UNITSTR(# (REAL n),(0* n),(n),(n),(n) #)) Element of bool [:[:REAL, the carrier of UNITSTR(# (REAL n),(0* n),(n),(n),(n) #):], the carrier of UNITSTR(# (REAL n),(0* n),(n),(n),(n) #):]
[:[:REAL, the carrier of UNITSTR(# (REAL n),(0* n),(n),(n),(n) #):], the carrier of UNITSTR(# (REAL n),(0* n),(n),(n),(n) #):] is V49() set
bool [:[:REAL, the carrier of UNITSTR(# (REAL n),(0* n),(n),(n),(n) #):], the carrier of UNITSTR(# (REAL n),(0* n),(n),(n),(n) #):] is V49() set
the scalar of UNITSTR(# (REAL n),(0* n),(n),(n),(n) #) is Relation-like [: the carrier of UNITSTR(# (REAL n),(0* n),(n),(n),(n) #), the carrier of UNITSTR(# (REAL n),(0* n),(n),(n),(n) #):] -defined REAL -valued Function-like V26([: the carrier of UNITSTR(# (REAL n),(0* n),(n),(n),(n) #), the carrier of UNITSTR(# (REAL n),(0* n),(n),(n),(n) #):]) V30([: the carrier of UNITSTR(# (REAL n),(0* n),(n),(n),(n) #), the carrier of UNITSTR(# (REAL n),(0* n),(n),(n),(n) #):], REAL ) complex-yielding V36() V37() Element of bool [:[: the carrier of UNITSTR(# (REAL n),(0* n),(n),(n),(n) #), the carrier of UNITSTR(# (REAL n),(0* n),(n),(n),(n) #):],REAL:]
[:[: the carrier of UNITSTR(# (REAL n),(0* n),(n),(n),(n) #), the carrier of UNITSTR(# (REAL n),(0* n),(n),(n),(n) #):],REAL:] is complex-yielding V36() V37() set
bool [:[: the carrier of UNITSTR(# (REAL n),(0* n),(n),(n),(n) #), the carrier of UNITSTR(# (REAL n),(0* n),(n),(n),(n) #):],REAL:] is set
seq is non empty strict UNITSTR
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 scalar of seq is Relation-like [: the carrier of seq, the carrier of seq:] -defined REAL -valued Function-like V26([: the carrier of seq, the carrier of seq:]) V30([: the carrier of seq, the carrier of seq:], REAL ) complex-yielding V36() V37() Element of bool [:[: the carrier of seq, the carrier of seq:],REAL:]
[:[: the carrier of seq, the carrier of seq:],REAL:] is complex-yielding V36() V37() set
bool [:[: the carrier of seq, the carrier of seq:],REAL:] is set
seq9 is non empty strict UNITSTR
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 scalar of seq9 is Relation-like [: the carrier of seq9, the carrier of seq9:] -defined REAL -valued Function-like V26([: the carrier of seq9, the carrier of seq9:]) V30([: the carrier of seq9, the carrier of seq9:], REAL ) complex-yielding V36() V37() Element of bool [:[: the carrier of seq9, the carrier of seq9:],REAL:]
[:[: the carrier of seq9, the carrier of seq9:],REAL:] is complex-yielding V36() V37() set
bool [:[: the carrier of seq9, the carrier of seq9:],REAL:] is set
n is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V49() V54() set
(n) is non empty strict UNITSTR
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 UNITSTR
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)
r is Element of the carrier of (n)
n -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet 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
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
len k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V33() V34() V49() V54() V158() V159() V160() V161() V162() V163() Element of NAT
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
len p is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V33() V34() V49() V54() V158() V159() V160() V161() V162() V163() Element of NAT
mlt (m1,m1) is Relation-like NAT -defined REAL -valued Function-like complex-yielding V36() V37() V49() FinSequence-like FinSubsequence-like FinSequence of REAL
dom (mlt (m1,m1)) is V158() V159() V160() V161() V162() V163() Element of bool NAT
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V49() V54() set
(mlt (m1,m1)) . k is V11() real ext-real Element of REAL
m1 . k is V11() real ext-real Element of REAL
(m1 . k) * (m1 . k) is V11() real ext-real Element of REAL
seq .|. seq is V11() real ext-real Element of REAL
[: the carrier of (n), the carrier of (n):] is set
the scalar of (n) is Relation-like [: the carrier of (n), the carrier of (n):] -defined REAL -valued Function-like V26([: the carrier of (n), the carrier of (n):]) V30([: the carrier of (n), the carrier of (n):], REAL ) complex-yielding V36() V37() Element of bool [:[: the carrier of (n), the carrier of (n):],REAL:]
[:[: the carrier of (n), the carrier of (n):],REAL:] is complex-yielding V36() V37() set
bool [:[: the carrier of (n), the carrier of (n):],REAL:] is set
K295( the carrier of (n), the carrier of (n),seq,seq) is Element of [: the carrier of (n), the carrier of (n):]
the scalar of (n) . K295( the carrier of (n), the carrier of (n),seq,seq) is V11() real ext-real Element of REAL
(n) is Relation-like [:(REAL n),(REAL n):] -defined REAL -valued Function-like V26([:(REAL n),(REAL n):]) V30([:(REAL n),(REAL n):], REAL ) complex-yielding V36() V37() Element of bool [:[:(REAL n),(REAL n):],REAL:]
[:(REAL n),(REAL n):] is set
[:[:(REAL n),(REAL n):],REAL:] is complex-yielding V36() V37() set
bool [:[:(REAL n),(REAL n):],REAL:] is set
(n) . (seq,seq) is set
[seq,seq] is set
(n) . [seq,seq] is V11() real ext-real set
Sum (mlt (m1,m1)) is V11() real ext-real Element of REAL
0. (n) is V69((n)) Element of the carrier of (n)
the ZeroF of (n) is Element of the carrier of (n)
dom k is V56(n) V158() V159() V160() V161() V162() V163() Element of bool NAT
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V33() V34() V49() V54() V158() V159() V160() V161() V162() V163() Element of NAT
k . k is V11() real ext-real Element of REAL
dom multreal is Relation-like set
rng m1 is V158() V159() V160() Element of bool REAL
[:(rng m1),(rng m1):] is complex-yielding V36() V37() set
multreal .: (m1,m1) is Relation-like Function-like set
dom (multreal .: (m1,m1)) is set
dom m1 is V56(n) V158() V159() V160() V161() V162() V163() Element of bool NAT
(dom m1) /\ (dom m1) is V158() V159() V160() V161() V162() V163() Element of bool NAT
(mlt (m1,m1)) . k is V11() real ext-real Element of REAL
m1 . k is V11() real ext-real Element of REAL
(m1 . k) ^2 is V11() real ext-real Element of REAL
K37((m1 . k),(m1 . k)) is V11() real ext-real set
n |-> 0 is Relation-like empty-yielding NAT -defined REAL -valued Function-like complex-yielding V36() V37() V49() V56(n) FinSequence-like FinSubsequence-like Element of n -tuples_on 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
mlt (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
0 * 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 |-> 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
b 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
len b is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V33() V34() V49() V54() V158() V159() V160() V161() V162() V163() Element of NAT
seq .|. seq9 is V11() real ext-real Element of REAL
K295( the carrier of (n), the carrier of (n),seq,seq9) is Element of [: the carrier of (n), the carrier of (n):]
the scalar of (n) . K295( the carrier of (n), the carrier of (n),seq,seq9) is V11() real ext-real Element of REAL
(n) . (seq,seq9) is set
[seq,seq9] is set
(n) . [seq,seq9] is V11() real ext-real set
mlt (m2,m1) is Relation-like NAT -defined REAL -valued Function-like complex-yielding V36() V37() V49() FinSequence-like FinSubsequence-like FinSequence of REAL
Sum (mlt (m2,m1)) is V11() real ext-real Element of REAL
(n) . (seq9,seq) is set
[seq9,seq] is set
(n) . [seq9,seq] is V11() real ext-real set
seq9 .|. seq is V11() real ext-real Element of REAL
K295( the carrier of (n), the carrier of (n),seq9,seq) is Element of [: the carrier of (n), the carrier of (n):]
the scalar of (n) . K295( the carrier of (n), the carrier of (n),seq9,seq) is V11() real ext-real Element of REAL
seq .|. r is V11() real ext-real Element of REAL
K295( the carrier of (n), the carrier of (n),seq,r) is Element of [: the carrier of (n), the carrier of (n):]
the scalar of (n) . K295( the carrier of (n), the carrier of (n),seq,r) is V11() real ext-real Element of REAL
(n) . (seq,r) is set
[seq,r] is set
(n) . [seq,r] is V11() real ext-real set
mlt (m1,p) is Relation-like NAT -defined REAL -valued Function-like complex-yielding V36() V37() V49() FinSequence-like FinSubsequence-like FinSequence of REAL
Sum (mlt (m1,p)) is V11() real ext-real Element of REAL
k is V11() real ext-real Element of REAL
k * 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) . (k,seq) is set
[k,seq] is set
the Mult of (n) . [k,seq] is set
Seg n is V49() V56(n) V158() V159() V160() V161() V162() V163() Element of bool NAT
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 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 epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V49() V54() set
k . k is V11() real ext-real Element of REAL
(k * m1) . k is V11() real ext-real Element of REAL
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,m1) is Relation-like NAT -defined Function-like V49() V56(n) FinSequence-like FinSubsequence-like Element of REAL n
[k,m1] is set
(n) . [k,m1] is Relation-like NAT -defined Function-like V49() FinSequence-like FinSubsequence-like set
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
seq9 .|. r is V11() real ext-real Element of REAL
K295( the carrier of (n), the carrier of (n),seq9,r) is Element of [: the carrier of (n), the carrier of (n):]
the scalar of (n) . K295( the carrier of (n), the carrier of (n),seq9,r) is V11() real ext-real Element of REAL
(n) . (seq9,r) is set
[seq9,r] is set
(n) . [seq9,r] is V11() real ext-real set
mlt (m2,p) is Relation-like NAT -defined REAL -valued Function-like complex-yielding V36() V37() V49() FinSequence-like FinSubsequence-like FinSequence of REAL
Sum (mlt (m2,p)) is V11() real ext-real Element of REAL
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):], 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)
the addF of (n) . [seq,seq9] is set
(seq + seq9) .|. r is V11() real ext-real Element of REAL
K295( the carrier of (n), the carrier of (n),(seq + seq9),r) is Element of [: the carrier of (n), the carrier of (n):]
the scalar of (n) . K295( the carrier of (n), the carrier of (n),(seq + seq9),r) is V11() real ext-real Element of REAL
(n) . ((seq + seq9),r) is set
[(seq + seq9),r] is set
(n) . [(seq + seq9),r] is V11() real ext-real 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
(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 V11() real ext-real Element of REAL
[((n) . (m1,m2)),p] is set
(n) . [((n) . (m1,m2)),p] is V11() real ext-real set
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
(n) . ((m1 + m2),p) is V11() real ext-real Element of REAL
[(m1 + m2),p] is set
(n) . [(m1 + m2),p] is V11() real ext-real set
mlt ((m1 + m2),p) is Relation-like NAT -defined REAL -valued Function-like complex-yielding V36() V37() V49() FinSequence-like FinSubsequence-like FinSequence of REAL
Sum (mlt ((m1 + m2),p)) is V11() real ext-real Element of REAL
(mlt (m1,p)) + (mlt (m2,p)) is Relation-like NAT -defined REAL -valued Function-like complex-yielding V36() V37() V49() FinSequence-like FinSubsequence-like FinSequence of REAL
Sum ((mlt (m1,p)) + (mlt (m2,p))) is V11() real ext-real Element of REAL
mlt (k,b) 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
Sum (mlt (k,b)) is V11() real ext-real Element of REAL
mlt (p,b) 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
Sum (mlt (p,b)) is V11() real ext-real Element of REAL
(Sum (mlt (k,b))) + (Sum (mlt (p,b))) is V11() real ext-real Element of REAL
(seq .|. r) + (seq9 .|. r) is V11() real ext-real Element of REAL
(k * seq) .|. seq9 is V11() real ext-real Element of REAL
K295( the carrier of (n), the carrier of (n),(k * seq),seq9) is Element of [: the carrier of (n), the carrier of (n):]
the scalar of (n) . K295( the carrier of (n), the carrier of (n),(k * seq),seq9) is V11() real ext-real Element of REAL
(n) . ((k * seq),seq9) is set
[(k * seq),seq9] is set
(n) . [(k * seq),seq9] is V11() real ext-real set
(n) . ((k * m1),m2) is V11() real ext-real Element of REAL
[(k * m1),m2] is set
(n) . [(k * m1),m2] is V11() real ext-real set
mlt ((k * m1),m2) is Relation-like NAT -defined REAL -valued Function-like complex-yielding V36() V37() V49() FinSequence-like FinSubsequence-like FinSequence of REAL
Sum (mlt ((k * m1),m2)) is V11() real ext-real Element of REAL
mlt (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
k * (mlt (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
Sum (k * (mlt (k,p))) is V11() real ext-real Element of REAL
Sum (mlt (k,p)) is V11() real ext-real Element of REAL
k * (Sum (mlt (k,p))) is V11() real ext-real Element of REAL
(n) . (m1,m2) is V11() real ext-real Element of REAL
(n) . [m1,m2] is V11() real ext-real set
k * ((n) . (m1,m2)) is V11() real ext-real Element of REAL
k * (seq .|. seq9) is V11() real ext-real Element of REAL
seq is V11() real ext-real set
seq9 is V11() real ext-real set
seq * seq9 is V11() real ext-real Element of REAL
r is Element of the carrier of (n)
(seq * seq9) * r is Element of the carrier of (n)
the Mult of (n) . ((seq * seq9),r) is set
[(seq * seq9),r] is set
the Mult of (n) . [(seq * seq9),r] is set
seq9 * r is Element of the carrier of (n)
the Mult of (n) . (seq9,r) is set
[seq9,r] is set
the Mult of (n) . [seq9,r] is set
seq * (seq9 * r) is Element of the carrier of (n)
the Mult of (n) . (seq,(seq9 * r)) is set
[seq,(seq9 * r)] is set
the Mult of (n) . [seq,(seq9 * r)] 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 REAL n
m2 is V11() real ext-real Element of REAL
m2 * r is Element of the carrier of (n)
the Mult of (n) . (m2,r) is set
[m2,r] is set
the Mult of (n) . [m2,r] 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
m2 * 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
b is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V49() V54() set
k . b is V11() real ext-real Element of REAL
(m2 * k) . b is V11() real ext-real Element of REAL
p is V11() real ext-real Element of REAL
p * r is Element of the carrier of (n)
the Mult of (n) . (p,r) is set
[p,r] is set
the Mult of (n) . [p,r] 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) . (p,k) is Relation-like NAT -defined Function-like V49() V56(n) FinSequence-like FinSubsequence-like Element of REAL n
[p,k] is set
(n) . [p,k] is Relation-like NAT -defined Function-like V49() FinSequence-like FinSubsequence-like set
p * 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 V11() real ext-real Element of REAL
m1 * (m2 * r) is Element of the carrier of (n)
the Mult of (n) . (m1,(m2 * r)) is set
[m1,(m2 * r)] is set
the Mult of (n) . [m1,(m2 * r)] 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) . (m1,(m2 * k)) is Relation-like NAT -defined Function-like V49() V56(n) FinSequence-like FinSubsequence-like Element of REAL n
[m1,(m2 * k)] is set
(n) . [m1,(m2 * k)] is Relation-like NAT -defined Function-like V49() FinSequence-like FinSubsequence-like set
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
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
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
m1 * m2 is V11() real ext-real Element of REAL
(m1 * m2) * r is Element of the carrier of (n)
the Mult of (n) . ((m1 * m2),r) is set
[(m1 * m2),r] is set
the Mult of (n) . [(m1 * m2),r] is set
(n) . ((m1 * m2),k) is Relation-like NAT -defined Function-like V49() V56(n) FinSequence-like FinSubsequence-like Element of REAL n
[(m1 * m2),k] is set
(n) . [(m1 * m2),k] 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 n -tuples_on REAL
seq is V11() real ext-real 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) . (seq9,r) is Element of the carrier of (n)
[seq9,r] is set
the addF of (n) . [seq9,r] is set
seq * (seq9 + r) is Element of the carrier of (n)
the Mult of (n) . (seq,(seq9 + r)) is set
[seq,(seq9 + r)] is set
the Mult of (n) . [seq,(seq9 + r)] is set
seq * seq9 is Element of the carrier of (n)
the Mult of (n) . (seq,seq9) is set
[seq,seq9] is set
the Mult of (n) . [seq,seq9] is set
seq * r is Element of the carrier of (n)
the Mult of (n) . (seq,r) is set
[seq,r] is set
the Mult of (n) . [seq,r] is set
(seq * seq9) + (seq * r) is Element of the carrier of (n)
the addF of (n) . ((seq * seq9),(seq * r)) is Element of the carrier of (n)
[(seq * seq9),(seq * r)] is set
the addF of (n) . [(seq * seq9),(seq * r)] 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 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 REAL n
m2 is V11() real ext-real Element of REAL
m2 * seq9 is Element of the carrier of (n)
the Mult of (n) . (m2,seq9) is set
[m2,seq9] is set
the Mult of (n) . [m2,seq9] is set
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
m2 * 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
b is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V49() V54() set
p . b is V11() real ext-real Element of REAL
(m2 * k) . b is V11() real ext-real Element of REAL
(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) . (m2,k) is Relation-like NAT -defined Function-like V49() V56(n) FinSequence-like FinSubsequence-like Element of REAL n
[m2,k] is set
(n) . [m2,k] is Relation-like NAT -defined Function-like V49() FinSequence-like FinSubsequence-like set
m2 * r is Element of the carrier of (n)
the Mult of (n) . (m2,r) is set
[m2,r] is set
the Mult of (n) . [m2,r] is set
b 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 * 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 epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V49() V54() set
b . k is V11() real ext-real Element of REAL
(m2 * m1) . k is V11() real ext-real Element of REAL
k is V11() real ext-real Element of REAL
k * r is Element of the carrier of (n)
the Mult of (n) . (k,r) is set
[k,r] is set
the Mult of (n) . [k,r] 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,m1) is Relation-like NAT -defined Function-like V49() V56(n) FinSequence-like FinSubsequence-like Element of REAL n
[k,m1] is set
(n) . [k,m1] is Relation-like NAT -defined Function-like V49() FinSequence-like FinSubsequence-like set
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
(m2 * seq9) + (m2 * r) is Element of the carrier of (n)
the addF of (n) . ((m2 * seq9),(m2 * r)) is Element of the carrier of (n)
[(m2 * seq9),(m2 * r)] is set
the addF of (n) . [(m2 * seq9),(m2 * r)] is set
(n) . ((m2 * seq9),(m2 * r)) is set
(n) . [(m2 * seq9),(m2 * r)] is Relation-like NAT -defined Function-like V49() FinSequence-like FinSubsequence-like set
(n) . ((m2 * k),(m2 * m1)) is Relation-like NAT -defined Function-like V49() V56(n) FinSequence-like FinSubsequence-like Element of REAL n
[(m2 * k),(m2 * m1)] is set
(n) . [(m2 * k),(m2 * m1)] is Relation-like NAT -defined Function-like V49() FinSequence-like FinSubsequence-like set
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
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
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
m2 * 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
(m2 * p) + (m2 * 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
m2 * (seq9 + r) is Element of the carrier of (n)
the Mult of (n) . (m2,(seq9 + r)) is set
[m2,(seq9 + r)] is set
the Mult of (n) . [m2,(seq9 + r)] 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) . (m2,(seq9 + r)) is set
(n) . [m2,(seq9 + r)] is Relation-like NAT -defined Function-like V49() FinSequence-like FinSubsequence-like set
(n) . (k,m1) is Relation-like NAT -defined Function-like V49() V56(n) FinSequence-like FinSubsequence-like Element of REAL n
[k,m1] is set
(n) . [k,m1] is Relation-like NAT -defined Function-like V49() FinSequence-like FinSubsequence-like set
(n) . (m2,((n) . (k,m1))) is Relation-like NAT -defined Function-like V49() V56(n) FinSequence-like FinSubsequence-like Element of REAL n
[m2,((n) . (k,m1))] is set
(n) . [m2,((n) . (k,m1))] is Relation-like NAT -defined Function-like V49() FinSequence-like FinSubsequence-like set
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
(n) . (m2,(k + m1)) is Relation-like NAT -defined Function-like V49() V56(n) FinSequence-like FinSubsequence-like Element of REAL n
[m2,(k + m1)] is set
(n) . [m2,(k + m1)] is Relation-like NAT -defined Function-like V49() FinSequence-like FinSubsequence-like set
m2 * (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
seq is V11() real ext-real set
seq9 is V11() real ext-real set
seq + seq9 is V11() real ext-real Element of REAL
r is Element of the carrier of (n)
(seq + seq9) * r is Element of the carrier of (n)
the Mult of (n) . ((seq + seq9),r) is set
[(seq + seq9),r] is set
the Mult of (n) . [(seq + seq9),r] is set
seq * r is Element of the carrier of (n)
the Mult of (n) . (seq,r) is set
[seq,r] is set
the Mult of (n) . [seq,r] is set
seq9 * r is Element of the carrier of (n)
the Mult of (n) . (seq9,r) is set
[seq9,r] is set
the Mult of (n) . [seq9,r] is set
(seq * r) + (seq9 * r) is Element of the carrier of (n)
the addF of (n) . ((seq * r),(seq9 * r)) is Element of the carrier of (n)
[(seq * r),(seq9 * r)] is set
the addF of (n) . [(seq * r),(seq9 * r)] 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 REAL n
m1 is V11() real ext-real Element of REAL
m2 is V11() real ext-real Element of REAL
m1 + m2 is V11() real ext-real Element of REAL
(m1 + m2) * r is Element of the carrier of (n)
the Mult of (n) . ((m1 + m2),r) is set
[(m1 + m2),r] is set
the Mult of (n) . [(m1 + m2),r] 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) . ((m1 + m2),k) is Relation-like NAT -defined Function-like V49() V56(n) FinSequence-like FinSubsequence-like Element of REAL n
[(m1 + m2),k] is set
(n) . [(m1 + m2),k] is Relation-like NAT -defined Function-like V49() FinSequence-like FinSubsequence-like set
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
m1 * 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
m2 * 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 * k) + (m2 * 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 * r is Element of the carrier of (n)
the Mult of (n) . (m1,r) is set
[m1,r] is set
the Mult of (n) . [m1,r] 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
b is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V49() V54() set
k . b is V11() real ext-real Element of REAL
(m1 * k) . b is V11() real ext-real Element of REAL
p is V11() real ext-real Element of REAL
p * r is Element of the carrier of (n)
the Mult of (n) . (p,r) is set
[p,r] is set
the Mult of (n) . [p,r] is set
(n) . (p,k) is Relation-like NAT -defined Function-like V49() V56(n) FinSequence-like FinSubsequence-like Element of REAL n
[p,k] is set
(n) . [p,k] is Relation-like NAT -defined Function-like V49() FinSequence-like FinSubsequence-like set
p * 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
m2 * r is Element of the carrier of (n)
the Mult of (n) . (m2,r) is set
[m2,r] is set
the Mult of (n) . [m2,r] is set
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 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V49() V54() set
p . k is V11() real ext-real Element of REAL
(m2 * k) . k is V11() real ext-real Element of REAL
b is V11() real ext-real Element of REAL
b * r is Element of the carrier of (n)
the Mult of (n) . (b,r) is set
[b,r] is set
the Mult of (n) . [b,r] is set
(n) . (b,k) is Relation-like NAT -defined Function-like V49() V56(n) FinSequence-like FinSubsequence-like Element of REAL n
[b,k] is set
(n) . [b,k] is Relation-like NAT -defined Function-like V49() FinSequence-like FinSubsequence-like set
b * 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 * r) + (m2 * r) is Element of the carrier of (n)
the addF of (n) . ((m1 * r),(m2 * r)) is Element of the carrier of (n)
[(m1 * r),(m2 * r)] is set
the addF of (n) . [(m1 * r),(m2 * r)] is set
(n) . ((m1 * r),(m2 * r)) is set
(n) . [(m1 * r),(m2 * r)] is Relation-like NAT -defined Function-like V49() FinSequence-like FinSubsequence-like set
(n) . ((m1 * k),(m2 * k)) is Relation-like NAT -defined Function-like V49() V56(n) FinSequence-like FinSubsequence-like Element of REAL n
[(m1 * k),(m2 * k)] is set
(n) . [(m1 * k),(m2 * k)] is Relation-like NAT -defined Function-like V49() FinSequence-like FinSubsequence-like set
m1 * 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
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
(m1 * p) + (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 is Element of the carrier of (n)
1 * seq is Element of the carrier of (n)
the Mult of (n) . (1,seq) is set
[1,seq] is set
the Mult of (n) . [1,seq] is 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
(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 Relation-like NAT -defined Function-like V49() V56(n) FinSequence-like FinSubsequence-like Element of REAL n
[1,seq9] is set
(n) . [1,seq9] is Relation-like NAT -defined Function-like V49() FinSequence-like FinSubsequence-like 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
1 * 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
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) . (seq,seq9) is Element of the carrier of (n)
[seq,seq9] is set
the addF of (n) . [seq,seq9] is set
seq9 + seq is Element of the carrier of (n)
the addF of (n) . (seq9,seq) is Element of the carrier of (n)
[seq9,seq] is set
the addF of (n) . [seq9,seq] is set
(n) . (seq,seq9) is set
(n) . [seq,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 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
(n) . (k,r) is Relation-like NAT -defined Function-like V49() V56(n) FinSequence-like FinSubsequence-like Element of REAL n
[k,r] is set
(n) . [k,r] is Relation-like NAT -defined Function-like V49() FinSequence-like FinSubsequence-like set
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) . (seq,seq9) is Element of the carrier of (n)
[seq,seq9] is set
the addF of (n) . [seq,seq9] is set
r is Element of the carrier of (n)
(seq + seq9) + r is Element of the carrier of (n)
the addF of (n) . ((seq + seq9),r) is Element of the carrier of (n)
[(seq + seq9),r] is set
the addF of (n) . [(seq + seq9),r] is set
seq9 + r is Element of the carrier of (n)
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
seq + (seq9 + r) is Element of the carrier of (n)
the addF of (n) . (seq,(seq9 + r)) is Element of the carrier of (n)
[seq,(seq9 + r)] is set
the addF of (n) . [seq,(seq9 + r)] 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 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 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
(n) . (k,(seq9 + r)) is set
[k,(seq9 + r)] is set
(n) . [k,(seq9 + r)] is Relation-like NAT -defined Function-like V49() FinSequence-like FinSubsequence-like set
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 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
(n) . (k,p) is set
[k,p] is set
(n) . [k,p] is Relation-like NAT -defined Function-like V49() FinSequence-like FinSubsequence-like set
(n) . (p,((n) . (k,p))) is set
[p,((n) . (k,p))] is set
(n) . [p,((n) . (k,p))] is Relation-like NAT -defined Function-like V49() FinSequence-like FinSubsequence-like set
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
(n) . (p,(m1 + m2)) is set
[p,(m1 + m2)] is set
(n) . [p,(m1 + m2)] is Relation-like NAT -defined Function-like V49() FinSequence-like FinSubsequence-like set
(n) . ((seq + seq9),m2) is set
[(seq + seq9),m2] is set
(n) . [(seq + seq9),m2] is Relation-like NAT -defined Function-like V49() FinSequence-like FinSubsequence-like set
(n) . (k,m1) is Relation-like NAT -defined Function-like V49() V56(n) FinSequence-like FinSubsequence-like Element of REAL n
[k,m1] is set
(n) . [k,m1] is Relation-like NAT -defined Function-like V49() FinSequence-like FinSubsequence-like set
(n) . (((n) . (k,m1)),m2) is Relation-like NAT -defined Function-like V49() V56(n) FinSequence-like FinSubsequence-like Element of REAL n
[((n) . (k,m1)),m2] is set
(n) . [((n) . (k,m1)),m2] is Relation-like NAT -defined Function-like V49() FinSequence-like FinSubsequence-like set
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
(n) . ((k + m1),m2) is Relation-like NAT -defined Function-like V49() V56(n) FinSequence-like FinSubsequence-like Element of REAL 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() FinSequence-like FinSubsequence-like FinSequence of 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
p + (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
seq is Element of the carrier of (n)
seq + (0. (n)) is Element of the carrier of (n)
the addF of (n) . (seq,(0. (n))) is Element of the carrier of (n)
[seq,(0. (n))] is set
the addF of (n) . [seq,(0. (n))] is set
(n) . (seq,(0. (n))) is set
(n) . [seq,(0. (n))] 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
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
(n) . (seq9,(0* n)) is Relation-like NAT -defined Function-like V49() V56(n) FinSequence-like FinSubsequence-like Element of REAL n
[seq9,(0* n)] is set
(n) . [seq9,(0* n)] is Relation-like NAT -defined Function-like V49() FinSequence-like FinSubsequence-like set
seq9 + (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
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
r is Element of the carrier of (n)
seq + r is Element of the carrier of (n)
the addF of (n) . (seq,r) is Element of the carrier of (n)
[seq,r] is set
the addF of (n) . [seq,r] is set
(n) . (seq9,(- seq9)) is Relation-like NAT -defined Function-like V49() V56(n) FinSequence-like FinSubsequence-like Element of REAL n
[seq9,(- seq9)] is set
(n) . [seq9,(- seq9)] is Relation-like NAT -defined Function-like V49() FinSequence-like FinSubsequence-like set
seq9 + (- 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
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
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 complete NORMSTR
the carrier of (n) is non empty set
(n) is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like UNITSTR
the carrier of (n) is non empty set
seq is V11() real ext-real Element of 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
- seq9 is Element of the carrier of (n)
seq * 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) . (seq,seq9) is set
[seq,seq9] is set
the Mult of (n) . [seq,seq9] is set
REAL n is non empty functional FinSequence-membered FinSequenceSet of REAL
m2 is Element of the carrier of (n)
p is Element of the carrier of (n)
m2 + p 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) . (m2,p) is Element of the carrier of (n)
[m2,p] is set
the addF of (n) . [m2,p] is set
- m2 is Element of the carrier of (n)
seq * 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) . (seq,m2) is set
[seq,m2] is set
the Mult of (n) . [seq,m2] 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
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 REAL n
(n) . (k,m1) is Relation-like NAT -defined Function-like V49() V56(n) FinSequence-like FinSubsequence-like Element of REAL n
[k,m1] is set
(n) . [k,m1] is Relation-like NAT -defined Function-like V49() FinSequence-like FinSubsequence-like set
- 1 is V11() real ext-real non positive V33() V34() Element of INT
(- 1) * seq9 is Element of the carrier of (n)
the Mult of (n) . ((- 1),seq9) is set
[(- 1),seq9] is set
the Mult of (n) . [(- 1),seq9] 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) . ((- 1),k) is set
[(- 1),k] is set
(n) . [(- 1),k] is Relation-like NAT -defined Function-like V49() FinSequence-like FinSubsequence-like set
(- 1) * m2 is Element of the carrier of (n)
the Mult of (n) . ((- 1),m2) is set
[(- 1),m2] is set
the Mult of (n) . [(- 1),m2] is set
(n) . (seq,k) is Relation-like NAT -defined Function-like V49() V56(n) FinSequence-like FinSubsequence-like Element of REAL n
[seq,k] is set
(n) . [seq,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 right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive strict RealNormSpace-like complete NORMSTR
the carrier of (n) is non empty set
(n) is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like UNITSTR
the carrier of (n) is non empty set
seq is Element of the carrier of (n)
||.seq.|| is V11() real ext-real non negative 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
||.seq.|| ^2 is V11() real ext-real Element of REAL
K37(||.seq.||,||.seq.||) is V11() real ext-real non negative set
seq9 is Element of the carrier of (n)
seq9 .|. seq9 is V11() real ext-real Element of REAL
[: the carrier of (n), the carrier of (n):] is set
the scalar of (n) is Relation-like [: the carrier of (n), the carrier of (n):] -defined REAL -valued Function-like V26([: the carrier of (n), the carrier of (n):]) V30([: the carrier of (n), the carrier of (n):], REAL ) complex-yielding V36() V37() Element of bool [:[: the carrier of (n), the carrier of (n):],REAL:]
[:[: the carrier of (n), the carrier of (n):],REAL:] is complex-yielding V36() V37() set
bool [:[: the carrier of (n), the carrier of (n):],REAL:] is set
K295( the carrier of (n), the carrier of (n),seq9,seq9) is Element of [: the carrier of (n), the carrier of (n):]
the scalar of (n) . K295( the carrier of (n), the carrier of (n),seq9,seq9) is V11() real ext-real Element of REAL
REAL n 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
|.r.| is V11() real ext-real non negative Element of REAL
|.r.| ^2 is V11() real ext-real Element of REAL
K37(|.r.|,|.r.|) is V11() real ext-real non negative set
|(r,r)| is V11() real ext-real Element of REAL
mlt (r,r) is Relation-like NAT -defined REAL -valued Function-like complex-yielding V36() V37() V49() FinSequence-like FinSubsequence-like FinSequence of REAL
Sum (mlt (r,r)) is V11() real ext-real Element of REAL
(n) is Relation-like [:(REAL n),(REAL n):] -defined REAL -valued Function-like V26([:(REAL n),(REAL n):]) V30([:(REAL n),(REAL n):], REAL ) complex-yielding V36() V37() Element of bool [:[:(REAL n),(REAL n):],REAL:]
[:(REAL n),(REAL n):] is set
[:[:(REAL n),(REAL n):],REAL:] is complex-yielding V36() V37() set
bool [:[:(REAL n),(REAL n):],REAL:] is set
(n) . (r,r) is V11() real ext-real Element of REAL
[r,r] is set
(n) . [r,r] is V11() real ext-real 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 complete NORMSTR
the carrier of (n) is non empty set
[:NAT, the carrier of (n):] is V49() set
bool [:NAT, the carrier of (n):] is V49() set
(n) is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like UNITSTR
the carrier of (n) is non empty set
[:NAT, the carrier of (n):] is V49() set
bool [:NAT, the carrier of (n):] is V49() set
seq is set
REAL n is non empty functional FinSequence-membered FinSequenceSet of 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 complete NORMSTR
the carrier of (n) is non empty set
[:NAT, the carrier of (n):] is V49() set
bool [:NAT, the carrier of (n):] is V49() set
(n) is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like UNITSTR
the carrier of (n) is non empty set
[:NAT, the carrier of (n):] is V49() set
bool [:NAT, the carrier of (n):] is V49() set
seq is non empty Relation-like NAT -defined the carrier of (n) -valued Function-like V26( NAT ) V30( NAT , the carrier of (n)) Element of bool [:NAT, the carrier of (n):]
lim seq is Element of the carrier of (n)
seq9 is non empty Relation-like NAT -defined the carrier of (n) -valued Function-like V26( NAT ) V30( NAT , the carrier of (n)) Element of bool [:NAT, the carrier of (n):]
lim seq9 is Element of the carrier of (n)
REAL n is non empty functional FinSequence-membered FinSequenceSet of REAL
k is Element of the carrier of (n)
m1 is Element of the carrier of (n)
m2 is V11() real ext-real Element of REAL
p is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V33() V34() V49() V54() V158() V159() V160() V161() V162() V163() Element of NAT
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V33() V34() V49() V54() V158() V159() V160() V161() V162() V163() Element of NAT
seq9 . k is Element of the carrier of (n)
dist ((seq9 . k),m1) is V11() real ext-real Element of REAL
(seq9 . k) - m1 is Element of the carrier of (n)
- m1 is Element of the carrier of (n)
(seq9 . 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) . ((seq9 . k),(- m1)) is Element of the carrier of (n)
[(seq9 . k),(- m1)] is set
the addF of (n) . [(seq9 . k),(- m1)] is set
||.((seq9 . k) - m1).|| is V11() real ext-real Element of REAL
((seq9 . k) - m1) .|. ((seq9 . k) - m1) is V11() real ext-real Element of REAL
the scalar of (n) is Relation-like [: the carrier of (n), the carrier of (n):] -defined REAL -valued Function-like V26([: the carrier of (n), the carrier of (n):]) V30([: the carrier of (n), the carrier of (n):], REAL ) complex-yielding V36() V37() Element of bool [:[: the carrier of (n), the carrier of (n):],REAL:]
[:[: the carrier of (n), the carrier of (n):],REAL:] is complex-yielding V36() V37() set
bool [:[: the carrier of (n), the carrier of (n):],REAL:] is set
K295( the carrier of (n), the carrier of (n),((seq9 . k) - m1),((seq9 . k) - m1)) is Element of [: the carrier of (n), the carrier of (n):]
the scalar of (n) . K295( the carrier of (n), the carrier of (n),((seq9 . k) - m1),((seq9 . k) - m1)) is V11() real ext-real Element of REAL
sqrt (((seq9 . k) - m1) .|. ((seq9 . k) - m1)) is V11() real ext-real Element of REAL
seq . k is Element of the carrier of (n)
(seq . k) - k is Element of the carrier of (n)
- k is Element of the carrier of (n)
(seq . k) + (- k) 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 . k),(- k)) is Element of the carrier of (n)
[(seq . k),(- k)] is set
the addF of (n) . [(seq . k),(- k)] is set
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
||.((seq . k) - k).|| is V11() real ext-real non negative 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 . k) - k) is V11() real ext-real Element of REAL
|.p.| is V11() real ext-real non negative Element of REAL
|(p,p)| is V11() real ext-real Element of REAL
sqrt |(p,p)| is V11() real ext-real Element of REAL
mlt (p,p) is Relation-like NAT -defined REAL -valued Function-like complex-yielding V36() V37() V49() FinSequence-like FinSubsequence-like FinSequence of REAL
Sum (mlt (p,p)) is V11() real ext-real Element of REAL
sqrt (Sum (mlt (p,p))) is V11() real ext-real Element of REAL
(n) is Relation-like [:(REAL n),(REAL n):] -defined REAL -valued Function-like V26([:(REAL n),(REAL n):]) V30([:(REAL n),(REAL n):], REAL ) complex-yielding V36() V37() Element of bool [:[:(REAL n),(REAL n):],REAL:]
[:(REAL n),(REAL n):] is set
[:[:(REAL n),(REAL n):],REAL:] is complex-yielding V36() V37() set
bool [:[:(REAL n),(REAL n):],REAL:] is set
(n) . (p,p) is V11() real ext-real Element of REAL
[p,p] is set
(n) . [p,p] is V11() real ext-real set
sqrt ((n) . (p,p)) is V11() real ext-real Element of REAL
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V33() V34() V49() V54() V158() V159() V160() V161() V162() V163() Element of NAT
seq9 . k is Element of the carrier of (n)
dist ((seq9 . k),m1) is V11() real ext-real Element of REAL
(seq9 . k) - m1 is Element of the carrier of (n)
- m1 is Element of the carrier of (n)
(seq9 . 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) . ((seq9 . k),(- m1)) is Element of the carrier of (n)
[(seq9 . k),(- m1)] is set
the addF of (n) . [(seq9 . k),(- m1)] is set
||.((seq9 . k) - m1).|| is V11() real ext-real Element of REAL
((seq9 . k) - m1) .|. ((seq9 . k) - m1) is V11() real ext-real Element of REAL
the scalar of (n) is Relation-like [: the carrier of (n), the carrier of (n):] -defined REAL -valued Function-like V26([: the carrier of (n), the carrier of (n):]) V30([: the carrier of (n), the carrier of (n):], REAL ) complex-yielding V36() V37() Element of bool [:[: the carrier of (n), the carrier of (n):],REAL:]
[:[: the carrier of (n), the carrier of (n):],REAL:] is complex-yielding V36() V37() set
bool [:[: the carrier of (n), the carrier of (n):],REAL:] is set
K295( the carrier of (n), the carrier of (n),((seq9 . k) - m1),((seq9 . k) - m1)) is Element of [: the carrier of (n), the carrier of (n):]
the scalar of (n) . K295( the carrier of (n), the carrier of (n),((seq9 . k) - m1),((seq9 . k) - m1)) is V11() real ext-real Element of REAL
sqrt (((seq9 . k) - m1) .|. ((seq9 . k) - m1)) is V11() real ext-real Element of REAL
r is Element of the carrier of (n)
m2 is V11() real ext-real Element of REAL
p is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V33() V34() V49() V54() V158() V159() V160() V161() V162() V163() Element of NAT
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V33() V34() V49() V54() V158() V159() V160() V161() V162() V163() Element of NAT
seq9 . k is Element of the carrier of (n)
dist ((seq9 . k),r) is V11() real ext-real Element of REAL
(seq9 . k) - r is Element of the carrier of (n)
- r is Element of the carrier of (n)
(seq9 . k) + (- 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 . k),(- r)) is Element of the carrier of (n)
[(seq9 . k),(- r)] is set
the addF of (n) . [(seq9 . k),(- r)] is set
||.((seq9 . k) - r).|| is V11() real ext-real Element of REAL
((seq9 . k) - r) .|. ((seq9 . k) - r) is V11() real ext-real Element of REAL
the scalar of (n) is Relation-like [: the carrier of (n), the carrier of (n):] -defined REAL -valued Function-like V26([: the carrier of (n), the carrier of (n):]) V30([: the carrier of (n), the carrier of (n):], REAL ) complex-yielding V36() V37() Element of bool [:[: the carrier of (n), the carrier of (n):],REAL:]
[:[: the carrier of (n), the carrier of (n):],REAL:] is complex-yielding V36() V37() set
bool [:[: the carrier of (n), the carrier of (n):],REAL:] is set
K295( the carrier of (n), the carrier of (n),((seq9 . k) - r),((seq9 . k) - r)) is Element of [: the carrier of (n), the carrier of (n):]
the scalar of (n) . K295( the carrier of (n), the carrier of (n),((seq9 . k) - r),((seq9 . k) - r)) is V11() real ext-real Element of REAL
sqrt (((seq9 . k) - r) .|. ((seq9 . k) - r)) is V11() real ext-real Element of REAL
seq . k is Element of the carrier of (n)
(seq . k) - (lim seq) is Element of the carrier of (n)
- (lim seq) is Element of the carrier of (n)
(seq . k) + (- (lim seq)) 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 . k),(- (lim seq))) is Element of the carrier of (n)
[(seq . k),(- (lim seq))] is set
the addF of (n) . [(seq . k),(- (lim seq))] is set
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
||.((seq . k) - (lim seq)).|| is V11() real ext-real non negative 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 . k) - (lim seq)) is V11() real ext-real Element of REAL
|.p.| is V11() real ext-real non negative Element of REAL
|(p,p)| is V11() real ext-real Element of REAL
sqrt |(p,p)| is V11() real ext-real Element of REAL
mlt (p,p) is Relation-like NAT -defined REAL -valued Function-like complex-yielding V36() V37() V49() FinSequence-like FinSubsequence-like FinSequence of REAL
Sum (mlt (p,p)) is V11() real ext-real Element of REAL
sqrt (Sum (mlt (p,p))) is V11() real ext-real Element of REAL
(n) is Relation-like [:(REAL n),(REAL n):] -defined REAL -valued Function-like V26([:(REAL n),(REAL n):]) V30([:(REAL n),(REAL n):], REAL ) complex-yielding V36() V37() Element of bool [:[:(REAL n),(REAL n):],REAL:]
[:(REAL n),(REAL n):] is set
[:[:(REAL n),(REAL n):],REAL:] is complex-yielding V36() V37() set
bool [:[:(REAL n),(REAL n):],REAL:] is set
(n) . (p,p) is V11() real ext-real Element of REAL
[p,p] is set
(n) . [p,p] is V11() real ext-real set
sqrt ((n) . (p,p)) is V11() real ext-real Element of REAL
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V33() V34() V49() V54() V158() V159() V160() V161() V162() V163() Element of NAT
seq9 . k is Element of the carrier of (n)
dist ((seq9 . k),r) is V11() real ext-real Element of REAL
(seq9 . k) - r is Element of the carrier of (n)
- r is Element of the carrier of (n)
(seq9 . k) + (- 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 . k),(- r)) is Element of the carrier of (n)
[(seq9 . k),(- r)] is set
the addF of (n) . [(seq9 . k),(- r)] is set
||.((seq9 . k) - r).|| is V11() real ext-real Element of REAL
((seq9 . k) - r) .|. ((seq9 . k) - r) is V11() real ext-real Element of REAL
the scalar of (n) is Relation-like [: the carrier of (n), the carrier of (n):] -defined REAL -valued Function-like V26([: the carrier of (n), the carrier of (n):]) V30([: the carrier of (n), the carrier of (n):], REAL ) complex-yielding V36() V37() Element of bool [:[: the carrier of (n), the carrier of (n):],REAL:]
[:[: the carrier of (n), the carrier of (n):],REAL:] is complex-yielding V36() V37() set
bool [:[: the carrier of (n), the carrier of (n):],REAL:] is set
K295( the carrier of (n), the carrier of (n),((seq9 . k) - r),((seq9 . k) - r)) is Element of [: the carrier of (n), the carrier of (n):]
the scalar of (n) . K295( the carrier of (n), the carrier of (n),((seq9 . k) - r),((seq9 . k) - r)) is V11() real ext-real Element of REAL
sqrt (((seq9 . k) - r) .|. ((seq9 . k) - r)) is V11() real ext-real Element of REAL
k is Element of the carrier of (n)
m1 is Element of the carrier of (n)
m2 is V11() real ext-real Element of REAL
p is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V33() V34() V49() V54() V158() V159() V160() V161() V162() V163() Element of NAT
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V33() V34() V49() V54() V158() V159() V160() V161() V162() V163() Element of NAT
seq . k is Element of the carrier of (n)
(seq . k) - m1 is Element of the carrier of (n)
- m1 is Element of the carrier of (n)
(seq . 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) . ((seq . k),(- m1)) is Element of the carrier of (n)
[(seq . k),(- m1)] is set
the addF of (n) . [(seq . k),(- m1)] is set
||.((seq . k) - m1).|| is V11() real ext-real non negative 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 . k) - m1) is V11() real ext-real Element of REAL
seq9 . k is Element of the carrier of (n)
(seq9 . k) - k is Element of the carrier of (n)
- k is Element of the carrier of (n)
(seq9 . k) + (- k) 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 . k),(- k)) is Element of the carrier of (n)
[(seq9 . k),(- k)] is set
the addF of (n) . [(seq9 . k),(- k)] is set
dist ((seq9 . k),k) is V11() real ext-real Element of REAL
||.((seq9 . k) - k).|| is V11() real ext-real Element of REAL
((seq9 . k) - k) .|. ((seq9 . k) - k) is V11() real ext-real Element of REAL
the scalar of (n) is Relation-like [: the carrier of (n), the carrier of (n):] -defined REAL -valued Function-like V26([: the carrier of (n), the carrier of (n):]) V30([: the carrier of (n), the carrier of (n):], REAL ) complex-yielding V36() V37() Element of bool [:[: the carrier of (n), the carrier of (n):],REAL:]
[:[: the carrier of (n), the carrier of (n):],REAL:] is complex-yielding V36() V37() set
bool [:[: the carrier of (n), the carrier of (n):],REAL:] is set
K295( the carrier of (n), the carrier of (n),((seq9 . k) - k),((seq9 . k) - k)) is Element of [: the carrier of (n), the carrier of (n):]
the scalar of (n) . K295( the carrier of (n), the carrier of (n),((seq9 . k) - k),((seq9 . k) - k)) is V11() real ext-real Element of REAL
sqrt (((seq9 . k) - k) .|. ((seq9 . k) - k)) is V11() real ext-real Element 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
(n) is Relation-like [:(REAL n),(REAL n):] -defined REAL -valued Function-like V26([:(REAL n),(REAL n):]) V30([:(REAL n),(REAL n):], REAL ) complex-yielding V36() V37() Element of bool [:[:(REAL n),(REAL n):],REAL:]
[:(REAL n),(REAL n):] is set
[:[:(REAL n),(REAL n):],REAL:] is complex-yielding V36() V37() set
bool [:[:(REAL n),(REAL n):],REAL:] is set
(n) . (p,p) is V11() real ext-real Element of REAL
[p,p] is set
(n) . [p,p] is V11() real ext-real set
sqrt ((n) . (p,p)) is V11() real ext-real Element of REAL
mlt (p,p) is Relation-like NAT -defined REAL -valued Function-like complex-yielding V36() V37() V49() FinSequence-like FinSubsequence-like FinSequence of REAL
Sum (mlt (p,p)) is V11() real ext-real Element of REAL
sqrt (Sum (mlt (p,p))) is V11() real ext-real Element of REAL
|(p,p)| is V11() real ext-real Element of REAL
sqrt |(p,p)| is V11() real ext-real Element of REAL
|.p.| is V11() real ext-real non negative Element of REAL
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V33() V34() V49() V54() V158() V159() V160() V161() V162() V163() Element of NAT
seq . k is Element of the carrier of (n)
(seq . k) - m1 is Element of the carrier of (n)
- m1 is Element of the carrier of (n)
(seq . 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) . ((seq . k),(- m1)) is Element of the carrier of (n)
[(seq . k),(- m1)] is set
the addF of (n) . [(seq . k),(- m1)] is set
||.((seq . k) - m1).|| is V11() real ext-real non negative 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 . k) - m1) is V11() real ext-real Element of REAL
r is Element of the carrier of (n)
m2 is V11() real ext-real Element of REAL
p is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V33() V34() V49() V54() V158() V159() V160() V161() V162() V163() Element of NAT
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V33() V34() V49() V54() V158() V159() V160() V161() V162() V163() Element of NAT
seq . k is Element of the carrier of (n)
(seq . k) - r is Element of the carrier of (n)
- r is Element of the carrier of (n)
(seq . k) + (- 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) . ((seq . k),(- r)) is Element of the carrier of (n)
[(seq . k),(- r)] is set
the addF of (n) . [(seq . k),(- r)] is set
||.((seq . k) - r).|| is V11() real ext-real non negative 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 . k) - r) is V11() real ext-real Element of REAL
seq9 . k is Element of the carrier of (n)
dist ((seq9 . k),(lim seq9)) is V11() real ext-real Element of REAL
(seq9 . k) - (lim seq9) is Element of the carrier of (n)
- (lim seq9) is Element of the carrier of (n)
(seq9 . k) + (- (lim 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) . ((seq9 . k),(- (lim seq9))) is Element of the carrier of (n)
[(seq9 . k),(- (lim seq9))] is set
the addF of (n) . [(seq9 . k),(- (lim seq9))] is set
||.((seq9 . k) - (lim seq9)).|| is V11() real ext-real Element of REAL
((seq9 . k) - (lim seq9)) .|. ((seq9 . k) - (lim seq9)) is V11() real ext-real Element of REAL
the scalar of (n) is Relation-like [: the carrier of (n), the carrier of (n):] -defined REAL -valued Function-like V26([: the carrier of (n), the carrier of (n):]) V30([: the carrier of (n), the carrier of (n):], REAL ) complex-yielding V36() V37() Element of bool [:[: the carrier of (n), the carrier of (n):],REAL:]
[:[: the carrier of (n), the carrier of (n):],REAL:] is complex-yielding V36() V37() set
bool [:[: the carrier of (n), the carrier of (n):],REAL:] is set
K295( the carrier of (n), the carrier of (n),((seq9 . k) - (lim seq9)),((seq9 . k) - (lim seq9))) is Element of [: the carrier of (n), the carrier of (n):]
the scalar of (n) . K295( the carrier of (n), the carrier of (n),((seq9 . k) - (lim seq9)),((seq9 . k) - (lim seq9))) is V11() real ext-real Element of REAL
sqrt (((seq9 . k) - (lim seq9)) .|. ((seq9 . k) - (lim seq9))) is V11() real ext-real Element 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
(n) is Relation-like [:(REAL n),(REAL n):] -defined REAL -valued Function-like V26([:(REAL n),(REAL n):]) V30([:(REAL n),(REAL n):], REAL ) complex-yielding V36() V37() Element of bool [:[:(REAL n),(REAL n):],REAL:]
[:(REAL n),(REAL n):] is set
[:[:(REAL n),(REAL n):],REAL:] is complex-yielding V36() V37() set
bool [:[:(REAL n),(REAL n):],REAL:] is set
(n) . (p,p) is V11() real ext-real Element of REAL
[p,p] is set
(n) . [p,p] is V11() real ext-real set
sqrt ((n) . (p,p)) is V11() real ext-real Element of REAL
mlt (p,p) is Relation-like NAT -defined REAL -valued Function-like complex-yielding V36() V37() V49() FinSequence-like FinSubsequence-like FinSequence of REAL
Sum (mlt (p,p)) is V11() real ext-real Element of REAL
sqrt (Sum (mlt (p,p))) is V11() real ext-real Element of REAL
|(p,p)| is V11() real ext-real Element of REAL
sqrt |(p,p)| is V11() real ext-real Element of REAL
|.p.| is V11() real ext-real non negative Element of 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 complete NORMSTR
the carrier of (n) is non empty set
[:NAT, the carrier of (n):] is V49() set
bool [:NAT, the carrier of (n):] is V49() set
(n) is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like UNITSTR
the carrier of (n) is non empty set
[:NAT, the carrier of (n):] is V49() set
bool [:NAT, the carrier of (n):] is V49() set
seq is non empty Relation-like NAT -defined the carrier of (n) -valued Function-like V26( NAT ) V30( NAT , the carrier of (n)) Element of bool [:NAT, the carrier of (n):]
seq9 is non empty Relation-like NAT -defined the carrier of (n) -valued Function-like V26( NAT ) V30( NAT , the carrier of (n)) Element of bool [:NAT, the carrier of (n):]
r is V11() real ext-real Element of REAL
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V33() V34() V49() V54() V158() V159() V160() V161() V162() V163() Element of NAT
m1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V33() V34() V49() V54() V158() V159() V160() V161() V162() V163() Element of NAT
m2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V33() V34() V49() V54() V158() V159() V160() V161() V162() V163() Element of NAT
seq9 . m1 is Element of the carrier of (n)
seq9 . m2 is Element of the carrier of (n)
dist ((seq9 . m1),(seq9 . m2)) is V11() real ext-real Element of REAL
(seq9 . m1) - (seq9 . m2) is Element of the carrier of (n)
- (seq9 . m2) is Element of the carrier of (n)
(seq9 . m1) + (- (seq9 . 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 . m1),(- (seq9 . m2))) is Element of the carrier of (n)
[(seq9 . m1),(- (seq9 . m2))] is set
the addF of (n) . [(seq9 . m1),(- (seq9 . m2))] is set
||.((seq9 . m1) - (seq9 . m2)).|| is V11() real ext-real Element of REAL
((seq9 . m1) - (seq9 . m2)) .|. ((seq9 . m1) - (seq9 . m2)) is V11() real ext-real Element of REAL
the scalar of (n) is Relation-like [: the carrier of (n), the carrier of (n):] -defined REAL -valued Function-like V26([: the carrier of (n), the carrier of (n):]) V30([: the carrier of (n), the carrier of (n):], REAL ) complex-yielding V36() V37() Element of bool [:[: the carrier of (n), the carrier of (n):],REAL:]
[:[: the carrier of (n), the carrier of (n):],REAL:] is complex-yielding V36() V37() set
bool [:[: the carrier of (n), the carrier of (n):],REAL:] is set
K295( the carrier of (n), the carrier of (n),((seq9 . m1) - (seq9 . m2)),((seq9 . m1) - (seq9 . m2))) is Element of [: the carrier of (n), the carrier of (n):]
the scalar of (n) . K295( the carrier of (n), the carrier of (n),((seq9 . m1) - (seq9 . m2)),((seq9 . m1) - (seq9 . m2))) is V11() real ext-real Element of REAL
sqrt (((seq9 . m1) - (seq9 . m2)) .|. ((seq9 . m1) - (seq9 . m2))) is V11() real ext-real Element of REAL
REAL n is non empty functional FinSequence-membered FinSequenceSet of REAL
seq . m2 is Element of the carrier of (n)
- (seq . m2) is Element of the carrier of (n)
seq . m1 is Element of the carrier of (n)
(seq . m1) + (- (seq . 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) . ((seq . m1),(- (seq . m2))) is Element of the carrier of (n)
[(seq . m1),(- (seq . m2))] is set
the addF of (n) . [(seq . m1),(- (seq . m2))] is set
(seq9 . m1) + (- (seq9 . m2)) is Element of the carrier of (n)
(seq . m1) - (seq . m2) is Element of the carrier of (n)
(seq . m1) + (- (seq . m2)) is Element of the carrier of (n)
||.((seq . m1) - (seq . m2)).|| is V11() real ext-real non negative 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 . m1) - (seq . m2)) is V11() real ext-real Element 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
|.p.| is V11() real ext-real non negative Element of REAL
|(p,p)| is V11() real ext-real Element of REAL
sqrt |(p,p)| is V11() real ext-real Element of REAL
mlt (p,p) is Relation-like NAT -defined REAL -valued Function-like complex-yielding V36() V37() V49() FinSequence-like FinSubsequence-like FinSequence of REAL
Sum (mlt (p,p)) is V11() real ext-real Element of REAL
sqrt (Sum (mlt (p,p))) is V11() real ext-real Element of REAL
(n) is Relation-like [:(REAL n),(REAL n):] -defined REAL -valued Function-like V26([:(REAL n),(REAL n):]) V30([:(REAL n),(REAL n):], REAL ) complex-yielding V36() V37() Element of bool [:[:(REAL n),(REAL n):],REAL:]
[:(REAL n),(REAL n):] is set
[:[:(REAL n),(REAL n):],REAL:] is complex-yielding V36() V37() set
bool [:[:(REAL n),(REAL n):],REAL:] is set
(n) . (p,p) is V11() real ext-real Element of REAL
[p,p] is set
(n) . [p,p] is V11() real ext-real set
sqrt ((n) . (p,p)) is V11() real ext-real Element of REAL
dist ((seq . m1),(seq . m2)) 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 right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive strict RealNormSpace-like complete NORMSTR
the carrier of (n) is non empty set
[:NAT, the carrier of (n):] is V49() set
bool [:NAT, the carrier of (n):] is V49() set
(n) is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like UNITSTR
the carrier of (n) is non empty set
[:NAT, the carrier of (n):] is V49() set
bool [:NAT, the carrier of (n):] is V49() set
seq is non empty Relation-like NAT -defined the carrier of (n) -valued Function-like V26( NAT ) V30( NAT , the carrier of (n)) Element of bool [:NAT, the carrier of (n):]
seq9 is non empty Relation-like NAT -defined the carrier of (n) -valued Function-like V26( NAT ) V30( NAT , the carrier of (n)) Element of bool [:NAT, the carrier of (n):]
r is V11() real ext-real Element of REAL
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V33() V34() V49() V54() V158() V159() V160() V161() V162() V163() Element of NAT
m1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V33() V34() V49() V54() V158() V159() V160() V161() V162() V163() Element of NAT
m2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V33() V34() V49() V54() V158() V159() V160() V161() V162() V163() Element of NAT
seq . m1 is Element of the carrier of (n)
seq . m2 is Element of the carrier of (n)
dist ((seq . m1),(seq . m2)) is V11() real ext-real Element of REAL
(seq . m1) - (seq . m2) is Element of the carrier of (n)
- (seq . m2) is Element of the carrier of (n)
(seq . m1) + (- (seq . 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) . ((seq . m1),(- (seq . m2))) is Element of the carrier of (n)
[(seq . m1),(- (seq . m2))] is set
the addF of (n) . [(seq . m1),(- (seq . m2))] is set
||.((seq . m1) - (seq . m2)).|| is V11() real ext-real non negative 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 . m1) - (seq . m2)) is V11() real ext-real Element of REAL
REAL n is non empty functional FinSequence-membered FinSequenceSet of REAL
seq9 . m1 is Element of the carrier of (n)
seq9 . m2 is Element of the carrier of (n)
(seq9 . m1) - (seq9 . m2) is Element of the carrier of (n)
- (seq9 . m2) is Element of the carrier of (n)
(seq9 . m1) + (- (seq9 . 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 . m1),(- (seq9 . m2))) is Element of the carrier of (n)
[(seq9 . m1),(- (seq9 . m2))] is set
the addF of (n) . [(seq9 . m1),(- (seq9 . m2))] is set
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
dist ((seq9 . m1),(seq9 . m2)) is V11() real ext-real Element of REAL
||.((seq9 . m1) - (seq9 . m2)).|| is V11() real ext-real Element of REAL
((seq9 . m1) - (seq9 . m2)) .|. ((seq9 . m1) - (seq9 . m2)) is V11() real ext-real Element of REAL
the scalar of (n) is Relation-like [: the carrier of (n), the carrier of (n):] -defined REAL -valued Function-like V26([: the carrier of (n), the carrier of (n):]) V30([: the carrier of (n), the carrier of (n):], REAL ) complex-yielding V36() V37() Element of bool [:[: the carrier of (n), the carrier of (n):],REAL:]
[:[: the carrier of (n), the carrier of (n):],REAL:] is complex-yielding V36() V37() set
bool [:[: the carrier of (n), the carrier of (n):],REAL:] is set
K295( the carrier of (n), the carrier of (n),((seq9 . m1) - (seq9 . m2)),((seq9 . m1) - (seq9 . m2))) is Element of [: the carrier of (n), the carrier of (n):]
the scalar of (n) . K295( the carrier of (n), the carrier of (n),((seq9 . m1) - (seq9 . m2)),((seq9 . m1) - (seq9 . m2))) is V11() real ext-real Element of REAL
sqrt (((seq9 . m1) - (seq9 . m2)) .|. ((seq9 . m1) - (seq9 . m2))) is V11() real ext-real Element of REAL
(n) is Relation-like [:(REAL n),(REAL n):] -defined REAL -valued Function-like V26([:(REAL n),(REAL n):]) V30([:(REAL n),(REAL n):], REAL ) complex-yielding V36() V37() Element of bool [:[:(REAL n),(REAL n):],REAL:]
[:(REAL n),(REAL n):] is set
[:[:(REAL n),(REAL n):],REAL:] is complex-yielding V36() V37() set
bool [:[:(REAL n),(REAL n):],REAL:] is set
(n) . (p,p) is V11() real ext-real Element of REAL
[p,p] is set
(n) . [p,p] is V11() real ext-real set
sqrt ((n) . (p,p)) is V11() real ext-real Element of REAL
mlt (p,p) is Relation-like NAT -defined REAL -valued Function-like complex-yielding V36() V37() V49() FinSequence-like FinSubsequence-like FinSequence of REAL
Sum (mlt (p,p)) is V11() real ext-real Element of REAL
sqrt (Sum (mlt (p,p))) is V11() real ext-real Element of REAL
|(p,p)| is V11() real ext-real Element of REAL
sqrt |(p,p)| is V11() real ext-real Element of REAL
|.p.| is V11() real ext-real non negative Element of 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 strict RealUnitarySpace-like UNITSTR
the carrier of (n) is non empty set
[:NAT, the carrier of (n):] is V49() set
bool [:NAT, the carrier of (n):] is V49() set
seq is non empty Relation-like NAT -defined the carrier of (n) -valued Function-like V26( NAT ) V30( NAT , the carrier of (n)) Element of bool [:NAT, the carrier of (n):]
(n) is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive strict RealNormSpace-like complete NORMSTR
the carrier of (n) is non empty set
[:NAT, the carrier of (n):] is V49() set
bool [:NAT, the carrier of (n):] is V49() set
seq9 is non empty Relation-like NAT -defined the carrier of (n) -valued Function-like V26( NAT ) V30( NAT , the carrier of (n)) Element of bool [:NAT, the carrier of (n):]