:: 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