:: TOPRNS_1 semantic presentation

REAL is non empty V32() V126() V127() V128() V132() set
NAT is non empty V4() V5() V6() V126() V127() V128() V129() V130() V131() V132() Element of K6(REAL)
K6(REAL) is set
COMPLEX is non empty V32() V126() V132() set
NAT is non empty V4() V5() V6() V126() V127() V128() V129() V130() V131() V132() set
K6(NAT) is set
K6(NAT) is set
RAT is non empty V32() V126() V127() V128() V129() V132() set
INT is non empty V32() V126() V127() V128() V129() V130() V132() set
K7(REAL,REAL) is V116() V117() V118() set
K6(K7(REAL,REAL)) is set
K309() is non empty V72() L8()
the carrier of K309() is non empty set
K314() is non empty V72() V94() V95() V96() V98() V148() V149() V150() V151() V152() V153() L8()
K315() is non empty V72() V96() V98() V151() V152() V153() M13(K314())
K316() is non empty V72() V94() V96() V98() V151() V152() V153() V154() M16(K314(),K315())
K318() is non empty V72() V94() V96() V98() L8()
K319() is non empty V72() V94() V96() V98() V154() M13(K318())
1 is non empty V4() V5() V6() V10() V11() V12() V30() V31() ext-real positive non negative V126() V127() V128() V129() V130() V131() Element of NAT
K7(1,1) is RAT -valued INT -valued V116() V117() V118() V119() set
K6(K7(1,1)) is set
K7(K7(1,1),1) is RAT -valued INT -valued V116() V117() V118() V119() set
K6(K7(K7(1,1),1)) is set
K7(K7(1,1),REAL) is V116() V117() V118() set
K6(K7(K7(1,1),REAL)) is set
K7(K7(REAL,REAL),REAL) is V116() V117() V118() set
K6(K7(K7(REAL,REAL),REAL)) is set
2 is non empty V4() V5() V6() V10() V11() V12() V30() V31() ext-real positive non negative V126() V127() V128() V129() V130() V131() Element of NAT
K7(2,2) is RAT -valued INT -valued V116() V117() V118() V119() set
K7(K7(2,2),REAL) is V116() V117() V118() set
K6(K7(K7(2,2),REAL)) is set
TOP-REAL 2 is non empty V70() V138() V139() TopSpace-like V183() V184() V185() V186() V187() V188() V189() V195() L16()
the carrier of (TOP-REAL 2) is non empty set
K7(COMPLEX,COMPLEX) is V116() set
K6(K7(COMPLEX,COMPLEX)) is set
K7(K7(COMPLEX,COMPLEX),COMPLEX) is V116() set
K6(K7(K7(COMPLEX,COMPLEX),COMPLEX)) is set
K7(RAT,RAT) is RAT -valued V116() V117() V118() set
K6(K7(RAT,RAT)) is set
K7(K7(RAT,RAT),RAT) is RAT -valued V116() V117() V118() set
K6(K7(K7(RAT,RAT),RAT)) is set
K7(INT,INT) is RAT -valued INT -valued V116() V117() V118() set
K6(K7(INT,INT)) is set
K7(K7(INT,INT),INT) is RAT -valued INT -valued V116() V117() V118() set
K6(K7(K7(INT,INT),INT)) is set
K7(NAT,NAT) is RAT -valued INT -valued V116() V117() V118() V119() set
K7(K7(NAT,NAT),NAT) is RAT -valued INT -valued V116() V117() V118() V119() set
K6(K7(K7(NAT,NAT),NAT)) is set
K7(NAT,REAL) is V116() V117() V118() set
K6(K7(NAT,REAL)) is set
{} is empty V4() V5() V6() V8() V9() V10() V11() V12() ext-real non positive non negative V126() V127() V128() V129() V130() V131() V132() set
0 is empty V4() V5() V6() V8() V9() V10() V11() V12() V30() V31() ext-real non positive non negative V126() V127() V128() V129() V130() V131() V132() Element of NAT
- 1 is V11() V12() ext-real non positive Element of REAL
4 is non empty V4() V5() V6() V10() V11() V12() V30() V31() ext-real positive non negative V126() V127() V128() V129() V130() V131() Element of NAT
N is V4() V5() V6() V10() V11() V12() V30() V31() ext-real non negative V126() V127() V128() V129() V130() V131() Element of NAT
TOP-REAL N is non empty V70() V138() V139() TopSpace-like V183() V184() V185() V186() V187() V188() V189() V195() L16()
the carrier of (TOP-REAL N) is non empty set
K7(NAT, the carrier of (TOP-REAL N)) is set
K6(K7(NAT, the carrier of (TOP-REAL N))) is set
seq is Relation-like Function-like set
dom seq is set
n1 is V4() V5() V6() V10() V11() V12() V30() V31() ext-real non negative V126() V127() V128() V129() V130() V131() Element of NAT
seq . n1 is set
n1 is set
seq . n1 is set
N is V4() V5() V6() V10() V11() V12() V30() V31() ext-real non negative V126() V127() V128() V129() V130() V131() Element of NAT
TOP-REAL N is non empty V70() V138() V139() TopSpace-like V183() V184() V185() V186() V187() V188() V189() V195() L16()
the carrier of (TOP-REAL N) is non empty set
K7(NAT, the carrier of (TOP-REAL N)) is set
K6(K7(NAT, the carrier of (TOP-REAL N))) is set
N is V4() V5() V6() V10() V11() V12() V30() V31() ext-real non negative V126() V127() V128() V129() V130() V131() Element of NAT
TOP-REAL N is non empty V70() V138() V139() TopSpace-like V183() V184() V185() V186() V187() V188() V189() V195() L16()
the carrier of (TOP-REAL N) is non empty set
K7(NAT, the carrier of (TOP-REAL N)) is set
K6(K7(NAT, the carrier of (TOP-REAL N))) is set
0. (TOP-REAL N) is Relation-like Function-like V39(N) V40() V51( TOP-REAL N) V116() V117() V118() Element of the carrier of (TOP-REAL N)
the ZeroF of (TOP-REAL N) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
seq is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
rng seq is set
NonZero (TOP-REAL N) is Element of K6( the carrier of (TOP-REAL N))
K6( the carrier of (TOP-REAL N)) is set
[#] (TOP-REAL N) is non empty non proper Element of K6( the carrier of (TOP-REAL N))
{(0. (TOP-REAL N))} is non empty set
([#] (TOP-REAL N)) \ {(0. (TOP-REAL N))} is Element of K6( the carrier of (TOP-REAL N))
n1 is set
seq . n1 is set
dom seq is V126() V127() V128() V129() V130() V131() set
n1 is set
rng seq is set
dom seq is V126() V127() V128() V129() V130() V131() set
n is set
seq . n is set
{(0. (TOP-REAL N))} is non empty set
NonZero (TOP-REAL N) is Element of K6( the carrier of (TOP-REAL N))
K6( the carrier of (TOP-REAL N)) is set
[#] (TOP-REAL N) is non empty non proper Element of K6( the carrier of (TOP-REAL N))
([#] (TOP-REAL N)) \ {(0. (TOP-REAL N))} is Element of K6( the carrier of (TOP-REAL N))
N is V4() V5() V6() V10() V11() V12() V30() V31() ext-real non negative V126() V127() V128() V129() V130() V131() Element of NAT
TOP-REAL N is non empty V70() V138() V139() TopSpace-like V183() V184() V185() V186() V187() V188() V189() V195() L16()
the carrier of (TOP-REAL N) is non empty set
K7(NAT, the carrier of (TOP-REAL N)) is set
K6(K7(NAT, the carrier of (TOP-REAL N))) is set
0. (TOP-REAL N) is Relation-like Function-like V39(N) V40() V51( TOP-REAL N) V116() V117() V118() Element of the carrier of (TOP-REAL N)
the ZeroF of (TOP-REAL N) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
seq is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
n1 is V4() V5() V6() V10() V11() V12() V30() V31() ext-real non negative V126() V127() V128() V129() V130() V131() Element of NAT
seq . n1 is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
n1 is set
seq . n1 is set
N is V4() V5() V6() V10() V11() V12() ext-real non negative set
TOP-REAL N is non empty V70() V138() V139() TopSpace-like V183() V184() V185() V186() V187() V188() V189() V195() L16()
the carrier of (TOP-REAL N) is non empty set
K7(NAT, the carrier of (TOP-REAL N)) is set
K6(K7(NAT, the carrier of (TOP-REAL N))) is set
seq is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
n1 is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
seq + n1 is Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
dom seq is V126() V127() V128() V129() V130() V131() set
dom n1 is V126() V127() V128() V129() V130() V131() set
dom (seq + n1) is V126() V127() V128() V129() V130() V131() set
(dom seq) /\ (dom n1) is V126() V127() V128() V129() V130() V131() set
seq is V4() V5() V6() V10() V11() V12() ext-real non negative set
TOP-REAL seq is non empty V70() V138() V139() TopSpace-like V183() V184() V185() V186() V187() V188() V189() V195() L16()
the carrier of (TOP-REAL seq) is non empty set
K7(NAT, the carrier of (TOP-REAL seq)) is set
K6(K7(NAT, the carrier of (TOP-REAL seq))) is set
n1 is non empty Relation-like NAT -defined the carrier of (TOP-REAL seq) -valued Function-like total V27( NAT , the carrier of (TOP-REAL seq)) Element of K6(K7(NAT, the carrier of (TOP-REAL seq)))
N is V11() V12() ext-real Element of REAL
N (#) n1 is Relation-like NAT -defined the carrier of (TOP-REAL seq) -valued Function-like Element of K6(K7(NAT, the carrier of (TOP-REAL seq)))
dom n1 is V126() V127() V128() V129() V130() V131() set
dom (N (#) n1) is V126() V127() V128() V129() V130() V131() set
N is V4() V5() V6() V10() V11() V12() ext-real non negative set
TOP-REAL N is non empty V70() V138() V139() TopSpace-like V183() V184() V185() V186() V187() V188() V189() V195() L16()
the carrier of (TOP-REAL N) is non empty set
K7(NAT, the carrier of (TOP-REAL N)) is set
K6(K7(NAT, the carrier of (TOP-REAL N))) is set
seq is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
- seq is Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
dom seq is V126() V127() V128() V129() V130() V131() set
dom (- seq) is V126() V127() V128() V129() V130() V131() set
N is V4() V5() V6() V10() V11() V12() ext-real non negative set
TOP-REAL N is non empty V70() V138() V139() TopSpace-like V183() V184() V185() V186() V187() V188() V189() V195() L16()
the carrier of (TOP-REAL N) is non empty set
K7(NAT, the carrier of (TOP-REAL N)) is set
K6(K7(NAT, the carrier of (TOP-REAL N))) is set
seq is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
n1 is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
(N,n1) is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
- n1 is Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
(N,seq,(N,n1)) is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
seq + (N,n1) is Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
N is V4() V5() V6() V10() V11() V12() ext-real non negative set
TOP-REAL N is non empty V70() V138() V139() TopSpace-like V183() V184() V185() V186() V187() V188() V189() V195() L16()
the carrier of (TOP-REAL N) is non empty set
K7(NAT, the carrier of (TOP-REAL N)) is set
K6(K7(NAT, the carrier of (TOP-REAL N))) is set
seq is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
n1 is non empty Relation-like NAT -defined REAL -valued Function-like total V27( NAT , REAL ) V116() V117() V118() Element of K6(K7(NAT,REAL))
n is non empty Relation-like NAT -defined REAL -valued Function-like total V27( NAT , REAL ) V116() V117() V118() Element of K6(K7(NAT,REAL))
m is V4() V5() V6() V10() V11() V12() V30() V31() ext-real non negative V126() V127() V128() V129() V130() V131() Element of NAT
n1 . m is V11() V12() ext-real set
n . m is V11() V12() ext-real set
n . m is V11() V12() ext-real Element of REAL
seq . m is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
|.(seq . m).| is V11() V12() ext-real non negative Element of REAL
n1 . m is V11() V12() ext-real Element of REAL
N is V4() V5() V6() V10() V11() V12() ext-real non negative set
TOP-REAL N is non empty V70() V138() V139() TopSpace-like V183() V184() V185() V186() V187() V188() V189() V195() L16()
the carrier of (TOP-REAL N) is non empty set
K7(NAT, the carrier of (TOP-REAL N)) is set
K6(K7(NAT, the carrier of (TOP-REAL N))) is set
seq is V4() V5() V6() V10() V11() V12() ext-real non negative set
n1 is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
n is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
(N,n1,n) is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
n1 + n is Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
(N,n1,n) . seq is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
n1 . seq is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
n . seq is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
(n1 . seq) + (n . seq) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K288((n1 . seq),(n . seq)) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
dom (N,n1,n) is V126() V127() V128() V129() V130() V131() set
m is V4() V5() V6() V10() V11() V12() V30() V31() ext-real non negative V126() V127() V128() V129() V130() V131() Element of NAT
(N,n1,n) /. m is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K123(NAT, the carrier of (TOP-REAL N),(N,n1,n),m) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
n1 /. m is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K123(NAT, the carrier of (TOP-REAL N),n1,m) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
n /. m is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K123(NAT, the carrier of (TOP-REAL N),n,m) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
(n1 /. m) + (n /. m) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K288((n1 /. m),(n /. m)) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
N is V11() V12() ext-real Element of REAL
seq is V4() V5() V6() V10() V11() V12() ext-real non negative set
TOP-REAL seq is non empty V70() V138() V139() TopSpace-like V183() V184() V185() V186() V187() V188() V189() V195() L16()
the carrier of (TOP-REAL seq) is non empty set
K7(NAT, the carrier of (TOP-REAL seq)) is set
K6(K7(NAT, the carrier of (TOP-REAL seq))) is set
n1 is V4() V5() V6() V10() V11() V12() ext-real non negative set
n is non empty Relation-like NAT -defined the carrier of (TOP-REAL seq) -valued Function-like total V27( NAT , the carrier of (TOP-REAL seq)) Element of K6(K7(NAT, the carrier of (TOP-REAL seq)))
(N,seq,n) is non empty Relation-like NAT -defined the carrier of (TOP-REAL seq) -valued Function-like total V27( NAT , the carrier of (TOP-REAL seq)) Element of K6(K7(NAT, the carrier of (TOP-REAL seq)))
N (#) n is Relation-like NAT -defined the carrier of (TOP-REAL seq) -valued Function-like Element of K6(K7(NAT, the carrier of (TOP-REAL seq)))
(N,seq,n) . n1 is Relation-like Function-like V39(seq) V40() V116() V117() V118() Element of the carrier of (TOP-REAL seq)
n . n1 is Relation-like Function-like V39(seq) V40() V116() V117() V118() Element of the carrier of (TOP-REAL seq)
N * (n . n1) is Relation-like Function-like V39(seq) V40() V116() V117() V118() Element of the carrier of (TOP-REAL seq)
K294((n . n1),N) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
dom (N,seq,n) is V126() V127() V128() V129() V130() V131() set
m is V4() V5() V6() V10() V11() V12() V30() V31() ext-real non negative V126() V127() V128() V129() V130() V131() Element of NAT
(N,seq,n) /. m is Relation-like Function-like V39(seq) V40() V116() V117() V118() Element of the carrier of (TOP-REAL seq)
K123(NAT, the carrier of (TOP-REAL seq),(N,seq,n),m) is Relation-like Function-like V39(seq) V40() V116() V117() V118() Element of the carrier of (TOP-REAL seq)
n /. m is Relation-like Function-like V39(seq) V40() V116() V117() V118() Element of the carrier of (TOP-REAL seq)
K123(NAT, the carrier of (TOP-REAL seq),n,m) is Relation-like Function-like V39(seq) V40() V116() V117() V118() Element of the carrier of (TOP-REAL seq)
N * (n /. m) is Relation-like Function-like V39(seq) V40() V116() V117() V118() Element of the carrier of (TOP-REAL seq)
K294((n /. m),N) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
N is V4() V5() V6() V10() V11() V12() ext-real non negative set
TOP-REAL N is non empty V70() V138() V139() TopSpace-like V183() V184() V185() V186() V187() V188() V189() V195() L16()
the carrier of (TOP-REAL N) is non empty set
K7(NAT, the carrier of (TOP-REAL N)) is set
K6(K7(NAT, the carrier of (TOP-REAL N))) is set
seq is V4() V5() V6() V10() V11() V12() ext-real non negative set
n1 is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
(N,n1) is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
- n1 is Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
(N,n1) . seq is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
n1 . seq is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
- (n1 . seq) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K290((n1 . seq)) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
dom (N,n1) is V126() V127() V128() V129() V130() V131() set
n is V4() V5() V6() V10() V11() V12() V30() V31() ext-real non negative V126() V127() V128() V129() V130() V131() Element of NAT
(N,n1) /. n is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K123(NAT, the carrier of (TOP-REAL N),(N,n1),n) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
n1 /. n is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K123(NAT, the carrier of (TOP-REAL N),n1,n) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
- (n1 /. n) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K290((n1 /. n)) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
N is V4() V5() V6() V10() V11() V12() V30() V31() ext-real non negative V126() V127() V128() V129() V130() V131() Element of NAT
TOP-REAL N is non empty V70() V138() V139() TopSpace-like V183() V184() V185() V186() V187() V188() V189() V195() L16()
the carrier of (TOP-REAL N) is non empty set
seq is V11() V12() ext-real Element of REAL
abs seq is V11() V12() ext-real Element of REAL
n1 is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
|.n1.| is V11() V12() ext-real non negative Element of REAL
(abs seq) * |.n1.| is V11() V12() ext-real Element of REAL
seq * n1 is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K294(n1,seq) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
|.(seq * n1).| is V11() V12() ext-real non negative Element of REAL
N is V4() V5() V6() V10() V11() V12() V30() V31() ext-real non negative V126() V127() V128() V129() V130() V131() Element of NAT
TOP-REAL N is non empty V70() V138() V139() TopSpace-like V183() V184() V185() V186() V187() V188() V189() V195() L16()
the carrier of (TOP-REAL N) is non empty set
K7(NAT, the carrier of (TOP-REAL N)) is set
K6(K7(NAT, the carrier of (TOP-REAL N))) is set
seq is V11() V12() ext-real Element of REAL
abs seq is V11() V12() ext-real Element of REAL
n1 is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
(seq,N,n1) is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
seq (#) n1 is Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
(N,(seq,N,n1)) is non empty Relation-like NAT -defined REAL -valued Function-like total V27( NAT , REAL ) V116() V117() V118() Element of K6(K7(NAT,REAL))
(N,n1) is non empty Relation-like NAT -defined REAL -valued Function-like total V27( NAT , REAL ) V116() V117() V118() Element of K6(K7(NAT,REAL))
(abs seq) (#) (N,n1) is non empty Relation-like NAT -defined REAL -valued Function-like total V27( NAT , REAL ) V116() V117() V118() Element of K6(K7(NAT,REAL))
n is V4() V5() V6() V10() V11() V12() V30() V31() ext-real non negative V126() V127() V128() V129() V130() V131() Element of NAT
(N,(seq,N,n1)) . n is V11() V12() ext-real set
((abs seq) (#) (N,n1)) . n is V11() V12() ext-real set
(N,(seq,N,n1)) . n is V11() V12() ext-real Element of REAL
(seq,N,n1) . n is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
|.((seq,N,n1) . n).| is V11() V12() ext-real non negative Element of REAL
n1 . n is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
seq * (n1 . n) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K294((n1 . n),seq) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
|.(seq * (n1 . n)).| is V11() V12() ext-real non negative Element of REAL
|.(n1 . n).| is V11() V12() ext-real non negative Element of REAL
(abs seq) * |.(n1 . n).| is V11() V12() ext-real Element of REAL
(N,n1) . n is V11() V12() ext-real Element of REAL
(abs seq) * ((N,n1) . n) is V11() V12() ext-real Element of REAL
((abs seq) (#) (N,n1)) . n is V11() V12() ext-real Element of REAL
N is V4() V5() V6() V10() V11() V12() V30() V31() ext-real non negative V126() V127() V128() V129() V130() V131() Element of NAT
TOP-REAL N is non empty V70() V138() V139() TopSpace-like V183() V184() V185() V186() V187() V188() V189() V195() L16()
the carrier of (TOP-REAL N) is non empty set
K7(NAT, the carrier of (TOP-REAL N)) is set
K6(K7(NAT, the carrier of (TOP-REAL N))) is set
seq is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
n1 is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
(N,seq,n1) is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
seq + n1 is Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
(N,n1,seq) is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
n1 + seq is Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
n is V4() V5() V6() V10() V11() V12() V30() V31() ext-real non negative V126() V127() V128() V129() V130() V131() Element of NAT
(N,seq,n1) . n is set
(N,n1,seq) . n is set
(N,seq,n1) . n is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
seq . n is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
n1 . n is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
(seq . n) + (n1 . n) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K288((seq . n),(n1 . n)) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
(N,n1,seq) . n is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
N is V4() V5() V6() V10() V11() V12() V30() V31() ext-real non negative V126() V127() V128() V129() V130() V131() Element of NAT
TOP-REAL N is non empty V70() V138() V139() TopSpace-like V183() V184() V185() V186() V187() V188() V189() V195() L16()
the carrier of (TOP-REAL N) is non empty set
K7(NAT, the carrier of (TOP-REAL N)) is set
K6(K7(NAT, the carrier of (TOP-REAL N))) is set
seq is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
n1 is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
(N,seq,n1) is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
seq + n1 is Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
n is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
(N,(N,seq,n1),n) is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
(N,seq,n1) + n is Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
(N,n1,n) is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
n1 + n is Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
(N,seq,(N,n1,n)) is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
seq + (N,n1,n) is Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
m is V4() V5() V6() V10() V11() V12() V30() V31() ext-real non negative V126() V127() V128() V129() V130() V131() Element of NAT
(N,(N,seq,n1),n) . m is set
(N,seq,(N,n1,n)) . m is set
(N,(N,seq,n1),n) . m is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
(N,seq,n1) . m is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
n . m is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
((N,seq,n1) . m) + (n . m) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K288(((N,seq,n1) . m),(n . m)) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
seq . m is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
n1 . m is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
(seq . m) + (n1 . m) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K288((seq . m),(n1 . m)) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
((seq . m) + (n1 . m)) + (n . m) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K288(((seq . m) + (n1 . m)),(n . m)) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
(n1 . m) + (n . m) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K288((n1 . m),(n . m)) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
(seq . m) + ((n1 . m) + (n . m)) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K288((seq . m),((n1 . m) + (n . m))) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
(N,n1,n) . m is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
(seq . m) + ((N,n1,n) . m) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K288((seq . m),((N,n1,n) . m)) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
(N,seq,(N,n1,n)) . m is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
N is V4() V5() V6() V10() V11() V12() V30() V31() ext-real non negative V126() V127() V128() V129() V130() V131() Element of NAT
TOP-REAL N is non empty V70() V138() V139() TopSpace-like V183() V184() V185() V186() V187() V188() V189() V195() L16()
the carrier of (TOP-REAL N) is non empty set
K7(NAT, the carrier of (TOP-REAL N)) is set
K6(K7(NAT, the carrier of (TOP-REAL N))) is set
seq is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
(N,seq) is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
- seq is Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
((- 1),N,seq) is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
(- 1) (#) seq is Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
n1 is V4() V5() V6() V10() V11() V12() V30() V31() ext-real non negative V126() V127() V128() V129() V130() V131() Element of NAT
(N,seq) . n1 is set
((- 1),N,seq) . n1 is set
((- 1),N,seq) . n1 is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
seq . n1 is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
(- 1) * (seq . n1) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K294((seq . n1),(- 1)) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
- (seq . n1) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K290((seq . n1)) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
(N,seq) . n1 is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
N is V4() V5() V6() V10() V11() V12() V30() V31() ext-real non negative V126() V127() V128() V129() V130() V131() Element of NAT
TOP-REAL N is non empty V70() V138() V139() TopSpace-like V183() V184() V185() V186() V187() V188() V189() V195() L16()
the carrier of (TOP-REAL N) is non empty set
K7(NAT, the carrier of (TOP-REAL N)) is set
K6(K7(NAT, the carrier of (TOP-REAL N))) is set
seq is V11() V12() ext-real Element of REAL
n1 is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
(seq,N,n1) is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
seq (#) n1 is Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
n is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
(N,n1,n) is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
n1 + n is Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
(seq,N,(N,n1,n)) is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
seq (#) (N,n1,n) is Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
(seq,N,n) is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
seq (#) n is Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
(N,(seq,N,n1),(seq,N,n)) is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
(seq,N,n1) + (seq,N,n) is Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
m is V4() V5() V6() V10() V11() V12() V30() V31() ext-real non negative V126() V127() V128() V129() V130() V131() Element of NAT
(seq,N,(N,n1,n)) . m is set
(N,(seq,N,n1),(seq,N,n)) . m is set
(seq,N,(N,n1,n)) . m is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
(N,n1,n) . m is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
seq * ((N,n1,n) . m) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K294(((N,n1,n) . m),seq) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
n1 . m is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
n . m is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
(n1 . m) + (n . m) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K288((n1 . m),(n . m)) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
seq * ((n1 . m) + (n . m)) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K294(((n1 . m) + (n . m)),seq) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
seq * (n1 . m) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K294((n1 . m),seq) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
seq * (n . m) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K294((n . m),seq) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
(seq * (n1 . m)) + (seq * (n . m)) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K288((seq * (n1 . m)),(seq * (n . m))) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
(seq,N,n1) . m is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
((seq,N,n1) . m) + (seq * (n . m)) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K288(((seq,N,n1) . m),(seq * (n . m))) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
(seq,N,n) . m is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
((seq,N,n1) . m) + ((seq,N,n) . m) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K288(((seq,N,n1) . m),((seq,N,n) . m)) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
(N,(seq,N,n1),(seq,N,n)) . m is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
N is V4() V5() V6() V10() V11() V12() V30() V31() ext-real non negative V126() V127() V128() V129() V130() V131() Element of NAT
TOP-REAL N is non empty V70() V138() V139() TopSpace-like V183() V184() V185() V186() V187() V188() V189() V195() L16()
the carrier of (TOP-REAL N) is non empty set
K7(NAT, the carrier of (TOP-REAL N)) is set
K6(K7(NAT, the carrier of (TOP-REAL N))) is set
seq is V11() V12() ext-real Element of REAL
n1 is V11() V12() ext-real Element of REAL
seq * n1 is V11() V12() ext-real Element of REAL
n is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
((seq * n1),N,n) is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
(seq * n1) (#) n is Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
(n1,N,n) is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
n1 (#) n is Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
(seq,N,(n1,N,n)) is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
seq (#) (n1,N,n) is Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
m is V4() V5() V6() V10() V11() V12() V30() V31() ext-real non negative V126() V127() V128() V129() V130() V131() Element of NAT
((seq * n1),N,n) . m is set
(seq,N,(n1,N,n)) . m is set
((seq * n1),N,n) . m is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
n . m is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
(seq * n1) * (n . m) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K294((n . m),(seq * n1)) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
n1 * (n . m) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K294((n . m),n1) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
seq * (n1 * (n . m)) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K294((n1 * (n . m)),seq) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
(n1,N,n) . m is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
seq * ((n1,N,n) . m) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K294(((n1,N,n) . m),seq) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
(seq,N,(n1,N,n)) . m is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
N is V4() V5() V6() V10() V11() V12() V30() V31() ext-real non negative V126() V127() V128() V129() V130() V131() Element of NAT
TOP-REAL N is non empty V70() V138() V139() TopSpace-like V183() V184() V185() V186() V187() V188() V189() V195() L16()
the carrier of (TOP-REAL N) is non empty set
K7(NAT, the carrier of (TOP-REAL N)) is set
K6(K7(NAT, the carrier of (TOP-REAL N))) is set
seq is V11() V12() ext-real Element of REAL
n1 is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
(seq,N,n1) is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
seq (#) n1 is Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
n is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
(N,n1,n) is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
(N,n) is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
- n is Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
(N,n1,(N,n)) is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
n1 + (N,n) is Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
(seq,N,(N,n1,n)) is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
seq (#) (N,n1,n) is Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
(seq,N,n) is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
seq (#) n is Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
(N,(seq,N,n1),(seq,N,n)) is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
(N,(seq,N,n)) is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
- (seq,N,n) is Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
(N,(seq,N,n1),(N,(seq,N,n))) is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
(seq,N,n1) + (N,(seq,N,n)) is Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
(seq,N,(N,n)) is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
seq (#) (N,n) is Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
(N,(seq,N,n1),(seq,N,(N,n))) is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
(seq,N,n1) + (seq,N,(N,n)) is Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
((- 1),N,n) is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
(- 1) (#) n is Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
(seq,N,((- 1),N,n)) is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
seq (#) ((- 1),N,n) is Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
(N,(seq,N,n1),(seq,N,((- 1),N,n))) is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
(seq,N,n1) + (seq,N,((- 1),N,n)) is Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
(- 1) * seq is V11() V12() ext-real Element of REAL
(((- 1) * seq),N,n) is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
((- 1) * seq) (#) n is Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
(N,(seq,N,n1),(((- 1) * seq),N,n)) is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
(seq,N,n1) + (((- 1) * seq),N,n) is Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
((- 1),N,(seq,N,n)) is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
(- 1) (#) (seq,N,n) is Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
(N,(seq,N,n1),((- 1),N,(seq,N,n))) is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
(seq,N,n1) + ((- 1),N,(seq,N,n)) is Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
N is V4() V5() V6() V10() V11() V12() V30() V31() ext-real non negative V126() V127() V128() V129() V130() V131() Element of NAT
TOP-REAL N is non empty V70() V138() V139() TopSpace-like V183() V184() V185() V186() V187() V188() V189() V195() L16()
the carrier of (TOP-REAL N) is non empty set
K7(NAT, the carrier of (TOP-REAL N)) is set
K6(K7(NAT, the carrier of (TOP-REAL N))) is set
seq is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
n1 is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
(N,seq,n1) is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
(N,n1) is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
- n1 is Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
(N,seq,(N,n1)) is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
seq + (N,n1) is Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
n is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
(N,n1,n) is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
n1 + n is Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
(N,seq,(N,n1,n)) is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
(N,(N,n1,n)) is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
- (N,n1,n) is Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
(N,seq,(N,(N,n1,n))) is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
seq + (N,(N,n1,n)) is Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
(N,(N,seq,n1),n) is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
(N,n) is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
- n is Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
(N,(N,seq,n1),(N,n)) is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
(N,seq,n1) + (N,n) is Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
((- 1),N,(N,n1,n)) is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
(- 1) (#) (N,n1,n) is Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
(N,seq,((- 1),N,(N,n1,n))) is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
seq + ((- 1),N,(N,n1,n)) is Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
((- 1),N,n1) is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
(- 1) (#) n1 is Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
((- 1),N,n) is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
(- 1) (#) n is Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
(N,((- 1),N,n1),((- 1),N,n)) is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
((- 1),N,n1) + ((- 1),N,n) is Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
(N,seq,(N,((- 1),N,n1),((- 1),N,n))) is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
seq + (N,((- 1),N,n1),((- 1),N,n)) is Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
(N,(N,n1),((- 1),N,n)) is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
(N,n1) + ((- 1),N,n) is Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
(N,seq,(N,(N,n1),((- 1),N,n))) is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
seq + (N,(N,n1),((- 1),N,n)) is Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
(N,(N,n1),(N,n)) is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
(N,n1) + (N,n) is Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
(N,seq,(N,(N,n1),(N,n))) is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
seq + (N,(N,n1),(N,n)) is Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
N is V4() V5() V6() V10() V11() V12() V30() V31() ext-real non negative V126() V127() V128() V129() V130() V131() Element of NAT
TOP-REAL N is non empty V70() V138() V139() TopSpace-like V183() V184() V185() V186() V187() V188() V189() V195() L16()
the carrier of (TOP-REAL N) is non empty set
K7(NAT, the carrier of (TOP-REAL N)) is set
K6(K7(NAT, the carrier of (TOP-REAL N))) is set
seq is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
(1,N,seq) is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
1 (#) seq is Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
n1 is V4() V5() V6() V10() V11() V12() V30() V31() ext-real non negative V126() V127() V128() V129() V130() V131() Element of NAT
(1,N,seq) . n1 is set
seq . n1 is set
(1,N,seq) . n1 is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
seq . n1 is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
1 * (seq . n1) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K294((seq . n1),1) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
N is V4() V5() V6() V10() V11() V12() V30() V31() ext-real non negative V126() V127() V128() V129() V130() V131() Element of NAT
TOP-REAL N is non empty V70() V138() V139() TopSpace-like V183() V184() V185() V186() V187() V188() V189() V195() L16()
the carrier of (TOP-REAL N) is non empty set
K7(NAT, the carrier of (TOP-REAL N)) is set
K6(K7(NAT, the carrier of (TOP-REAL N))) is set
seq is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
(N,seq) is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
- seq is Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
(N,(N,seq)) is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
- (N,seq) is Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
((- 1),N,(N,seq)) is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
(- 1) (#) (N,seq) is Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
((- 1),N,seq) is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
(- 1) (#) seq is Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
((- 1),N,((- 1),N,seq)) is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
(- 1) (#) ((- 1),N,seq) is Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
(- 1) * (- 1) is V11() V12() ext-real non negative Element of REAL
(((- 1) * (- 1)),N,seq) is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
((- 1) * (- 1)) (#) seq is Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
N is V4() V5() V6() V10() V11() V12() V30() V31() ext-real non negative V126() V127() V128() V129() V130() V131() Element of NAT
TOP-REAL N is non empty V70() V138() V139() TopSpace-like V183() V184() V185() V186() V187() V188() V189() V195() L16()
the carrier of (TOP-REAL N) is non empty set
K7(NAT, the carrier of (TOP-REAL N)) is set
K6(K7(NAT, the carrier of (TOP-REAL N))) is set
seq is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
n1 is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
(N,n1) is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
- n1 is Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
(N,seq,(N,n1)) is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
(N,(N,n1)) is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
- (N,n1) is Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
(N,seq,(N,(N,n1))) is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
seq + (N,(N,n1)) is Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
(N,seq,n1) is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
seq + n1 is Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
N is V4() V5() V6() V10() V11() V12() V30() V31() ext-real non negative V126() V127() V128() V129() V130() V131() Element of NAT
TOP-REAL N is non empty V70() V138() V139() TopSpace-like V183() V184() V185() V186() V187() V188() V189() V195() L16()
the carrier of (TOP-REAL N) is non empty set
K7(NAT, the carrier of (TOP-REAL N)) is set
K6(K7(NAT, the carrier of (TOP-REAL N))) is set
seq is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
n1 is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
(N,seq,n1) is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
(N,n1) is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
- n1 is Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
(N,seq,(N,n1)) is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
seq + (N,n1) is Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
n is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
(N,n1,n) is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
(N,n) is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
- n is Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
(N,n1,(N,n)) is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
n1 + (N,n) is Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
(N,seq,(N,n1,n)) is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
(N,(N,n1,n)) is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
- (N,n1,n) is Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
(N,seq,(N,(N,n1,n))) is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
seq + (N,(N,n1,n)) is Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
(N,(N,seq,n1),n) is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
(N,seq,n1) + n is Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
((- 1),N,(N,n1,n)) is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
(- 1) (#) (N,n1,n) is Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
(N,seq,((- 1),N,(N,n1,n))) is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
seq + ((- 1),N,(N,n1,n)) is Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
((- 1),N,n1) is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
(- 1) (#) n1 is Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
((- 1),N,n) is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
(- 1) (#) n is Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
(N,((- 1),N,n1),((- 1),N,n)) is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
(N,((- 1),N,n)) is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
- ((- 1),N,n) is Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
(N,((- 1),N,n1),(N,((- 1),N,n))) is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
((- 1),N,n1) + (N,((- 1),N,n)) is Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
(N,seq,(N,((- 1),N,n1),((- 1),N,n))) is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
seq + (N,((- 1),N,n1),((- 1),N,n)) is Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
(N,(N,n1),((- 1),N,n)) is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
(N,(N,n1),(N,((- 1),N,n))) is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
(N,n1) + (N,((- 1),N,n)) is Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
(N,seq,(N,(N,n1),((- 1),N,n))) is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
seq + (N,(N,n1),((- 1),N,n)) is Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
(N,(N,n1),(N,n)) is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
(N,(N,n)) is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
- (N,n) is Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
(N,(N,n1),(N,(N,n))) is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
(N,n1) + (N,(N,n)) is Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
(N,seq,(N,(N,n1),(N,n))) is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
seq + (N,(N,n1),(N,n)) is Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
(N,(N,n1),n) is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
(N,n1) + n is Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
(N,seq,(N,(N,n1),n)) is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
seq + (N,(N,n1),n) is Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
N is V4() V5() V6() V10() V11() V12() V30() V31() ext-real non negative V126() V127() V128() V129() V130() V131() Element of NAT
TOP-REAL N is non empty V70() V138() V139() TopSpace-like V183() V184() V185() V186() V187() V188() V189() V195() L16()
the carrier of (TOP-REAL N) is non empty set
K7(NAT, the carrier of (TOP-REAL N)) is set
K6(K7(NAT, the carrier of (TOP-REAL N))) is set
seq is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
n1 is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
n is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
(N,n1,n) is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
(N,n) is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
- n is Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
(N,n1,(N,n)) is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
n1 + (N,n) is Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
(N,seq,(N,n1,n)) is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
seq + (N,n1,n) is Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
(N,seq,n1) is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
seq + n1 is Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
(N,(N,seq,n1),n) is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
(N,(N,seq,n1),(N,n)) is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
(N,seq,n1) + (N,n) is Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
N is V4() V5() V6() V10() V11() V12() V30() V31() ext-real non negative V126() V127() V128() V129() V130() V131() Element of NAT
TOP-REAL N is non empty V70() V138() V139() TopSpace-like V183() V184() V185() V186() V187() V188() V189() V195() L16()
the carrier of (TOP-REAL N) is non empty set
K7(NAT, the carrier of (TOP-REAL N)) is set
K6(K7(NAT, the carrier of (TOP-REAL N))) is set
seq is V11() V12() ext-real Element of REAL
n1 is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
(seq,N,n1) is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
seq (#) n1 is Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
0. (TOP-REAL N) is Relation-like Function-like V39(N) V40() V51( TOP-REAL N) V116() V117() V118() Element of the carrier of (TOP-REAL N)
the ZeroF of (TOP-REAL N) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
n is V4() V5() V6() V10() V11() V12() V30() V31() ext-real non negative V126() V127() V128() V129() V130() V131() Element of NAT
(seq,N,n1) . n is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
n1 . n is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
seq * (n1 . n) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K294((n1 . n),seq) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
N is V4() V5() V6() V10() V11() V12() V30() V31() ext-real non negative V126() V127() V128() V129() V130() V131() Element of NAT
TOP-REAL N is non empty V70() V138() V139() TopSpace-like V183() V184() V185() V186() V187() V188() V189() V195() L16()
the carrier of (TOP-REAL N) is non empty set
K7(NAT, the carrier of (TOP-REAL N)) is set
K6(K7(NAT, the carrier of (TOP-REAL N))) is set
seq is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
(N,seq) is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
- seq is Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
((- 1),N,seq) is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
(- 1) (#) seq is Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
N is V4() V5() V6() V10() V11() V12() V30() V31() ext-real non negative V126() V127() V128() V129() V130() V131() Element of NAT
TOP-REAL N is non empty V70() V138() V139() TopSpace-like V183() V184() V185() V186() V187() V188() V189() V195() L16()
0. (TOP-REAL N) is Relation-like Function-like V39(N) V40() V51( TOP-REAL N) V116() V117() V118() Element of the carrier of (TOP-REAL N)
the carrier of (TOP-REAL N) is non empty set
the ZeroF of (TOP-REAL N) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
|.(0. (TOP-REAL N)).| is V11() V12() ext-real non negative Element of REAL
0* N is Relation-like NAT -defined REAL -valued Function-like V39(N) V40() V116() V117() V118() M11( REAL , REAL N)
REAL N is non empty V42() M10( REAL )
|.(0* N).| is V11() V12() ext-real non negative Element of REAL
N is V4() V5() V6() V10() V11() V12() V30() V31() ext-real non negative V126() V127() V128() V129() V130() V131() Element of NAT
TOP-REAL N is non empty V70() V138() V139() TopSpace-like V183() V184() V185() V186() V187() V188() V189() V195() L16()
the carrier of (TOP-REAL N) is non empty set
0. (TOP-REAL N) is Relation-like Function-like V39(N) V40() V51( TOP-REAL N) V116() V117() V118() Element of the carrier of (TOP-REAL N)
the ZeroF of (TOP-REAL N) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
seq is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
|.seq.| is V11() V12() ext-real non negative Element of REAL
REAL N is non empty V42() M10( REAL )
n1 is V39(N) Element of REAL N
0* N is Relation-like NAT -defined REAL -valued Function-like V39(N) V40() V116() V117() V118() M11( REAL , REAL N)
N is V4() V5() V6() V10() V11() V12() V30() V31() ext-real non negative V126() V127() V128() V129() V130() V131() Element of NAT
TOP-REAL N is non empty V70() V138() V139() TopSpace-like V183() V184() V185() V186() V187() V188() V189() V195() L16()
the carrier of (TOP-REAL N) is non empty set
seq is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
|.seq.| is V11() V12() ext-real non negative Element of REAL
N is V4() V5() V6() V10() V11() V12() V30() V31() ext-real non negative V126() V127() V128() V129() V130() V131() Element of NAT
TOP-REAL N is non empty V70() V138() V139() TopSpace-like V183() V184() V185() V186() V187() V188() V189() V195() L16()
the carrier of (TOP-REAL N) is non empty set
seq is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
- seq is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K290(seq) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
|.(- seq).| is V11() V12() ext-real non negative Element of REAL
|.seq.| is V11() V12() ext-real non negative Element of REAL
N is V4() V5() V6() V10() V11() V12() V30() V31() ext-real non negative V126() V127() V128() V129() V130() V131() Element of NAT
TOP-REAL N is non empty V70() V138() V139() TopSpace-like V183() V184() V185() V186() V187() V188() V189() V195() L16()
the carrier of (TOP-REAL N) is non empty set
seq is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
n1 is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
seq - n1 is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K292(seq,n1) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
|.(seq - n1).| is V11() V12() ext-real non negative Element of REAL
n1 - seq is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K292(n1,seq) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
|.(n1 - seq).| is V11() V12() ext-real non negative Element of REAL
- (seq - n1) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K290((seq - n1)) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
|.(- (seq - n1)).| is V11() V12() ext-real non negative Element of REAL
N is V4() V5() V6() V10() V11() V12() V30() V31() ext-real non negative V126() V127() V128() V129() V130() V131() Element of NAT
TOP-REAL N is non empty V70() V138() V139() TopSpace-like V183() V184() V185() V186() V187() V188() V189() V195() L16()
the carrier of (TOP-REAL N) is non empty set
seq is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
n1 is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
seq - n1 is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K292(seq,n1) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
|.(seq - n1).| is V11() V12() ext-real non negative Element of REAL
0. (TOP-REAL N) is Relation-like Function-like V39(N) V40() V51( TOP-REAL N) V116() V117() V118() Element of the carrier of (TOP-REAL N)
the ZeroF of (TOP-REAL N) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
N is V4() V5() V6() V10() V11() V12() V30() V31() ext-real non negative V126() V127() V128() V129() V130() V131() Element of NAT
TOP-REAL N is non empty V70() V138() V139() TopSpace-like V183() V184() V185() V186() V187() V188() V189() V195() L16()
the carrier of (TOP-REAL N) is non empty set
seq is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
n1 is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
seq - n1 is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K292(seq,n1) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
|.(seq - n1).| is V11() V12() ext-real non negative Element of REAL
0. (TOP-REAL N) is Relation-like Function-like V39(N) V40() V51( TOP-REAL N) V116() V117() V118() Element of the carrier of (TOP-REAL N)
the ZeroF of (TOP-REAL N) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
|.(0. (TOP-REAL N)).| is V11() V12() ext-real non negative Element of REAL
N is V4() V5() V6() V10() V11() V12() V30() V31() ext-real non negative V126() V127() V128() V129() V130() V131() Element of NAT
TOP-REAL N is non empty V70() V138() V139() TopSpace-like V183() V184() V185() V186() V187() V188() V189() V195() L16()
the carrier of (TOP-REAL N) is non empty set
n is V4() V5() V6() V10() V11() V12() V30() V31() ext-real non negative V126() V127() V128() V129() V130() V131() Element of NAT
TOP-REAL n is non empty V70() V138() V139() TopSpace-like V183() V184() V185() V186() V187() V188() V189() V195() L16()
the carrier of (TOP-REAL n) is non empty set
seq is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
n1 is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
seq - n1 is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K292(seq,n1) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
|.(seq - n1).| is V11() V12() ext-real non negative Element of REAL
m is Relation-like Function-like V39(n) V40() V116() V117() V118() Element of the carrier of (TOP-REAL n)
r1 is Relation-like Function-like V39(n) V40() V116() V117() V118() Element of the carrier of (TOP-REAL n)
m - r1 is Relation-like Function-like V39(n) V40() V116() V117() V118() Element of the carrier of (TOP-REAL n)
K292(m,r1) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
|.(m - r1).| is V11() V12() ext-real non negative Element of REAL
N is V4() V5() V6() V10() V11() V12() V30() V31() ext-real non negative V126() V127() V128() V129() V130() V131() Element of NAT
TOP-REAL N is non empty V70() V138() V139() TopSpace-like V183() V184() V185() V186() V187() V188() V189() V195() L16()
the carrier of (TOP-REAL N) is non empty set
seq is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
|.seq.| is V11() V12() ext-real non negative Element of REAL
n1 is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
seq + n1 is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K288(seq,n1) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
|.(seq + n1).| is V11() V12() ext-real non negative Element of REAL
|.n1.| is V11() V12() ext-real non negative Element of REAL
|.seq.| + |.n1.| is V11() V12() ext-real non negative Element of REAL
REAL N is non empty V42() M10( REAL )
n is V39(N) Element of REAL N
m is V39(N) Element of REAL N
n + m is Relation-like NAT -defined REAL -valued Function-like V39(N) V40() V116() V117() V118() M11( REAL , REAL N)
N is V4() V5() V6() V10() V11() V12() V30() V31() ext-real non negative V126() V127() V128() V129() V130() V131() Element of NAT
TOP-REAL N is non empty V70() V138() V139() TopSpace-like V183() V184() V185() V186() V187() V188() V189() V195() L16()
the carrier of (TOP-REAL N) is non empty set
seq is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
|.seq.| is V11() V12() ext-real non negative Element of REAL
n1 is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
seq - n1 is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K292(seq,n1) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
|.(seq - n1).| is V11() V12() ext-real non negative Element of REAL
|.n1.| is V11() V12() ext-real non negative Element of REAL
|.seq.| + |.n1.| is V11() V12() ext-real non negative Element of REAL
REAL N is non empty V42() M10( REAL )
n is V39(N) Element of REAL N
m is V39(N) Element of REAL N
n - m is Relation-like NAT -defined REAL -valued Function-like V39(N) V40() V116() V117() V118() M11( REAL , REAL N)
N is V4() V5() V6() V10() V11() V12() V30() V31() ext-real non negative V126() V127() V128() V129() V130() V131() Element of NAT
TOP-REAL N is non empty V70() V138() V139() TopSpace-like V183() V184() V185() V186() V187() V188() V189() V195() L16()
the carrier of (TOP-REAL N) is non empty set
seq is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
|.seq.| is V11() V12() ext-real non negative Element of REAL
n1 is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
|.n1.| is V11() V12() ext-real non negative Element of REAL
|.seq.| - |.n1.| is V11() V12() ext-real Element of REAL
seq + n1 is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K288(seq,n1) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
|.(seq + n1).| is V11() V12() ext-real non negative Element of REAL
REAL N is non empty V42() M10( REAL )
n is V39(N) Element of REAL N
m is V39(N) Element of REAL N
n + m is Relation-like NAT -defined REAL -valued Function-like V39(N) V40() V116() V117() V118() M11( REAL , REAL N)
N is V4() V5() V6() V10() V11() V12() V30() V31() ext-real non negative V126() V127() V128() V129() V130() V131() Element of NAT
TOP-REAL N is non empty V70() V138() V139() TopSpace-like V183() V184() V185() V186() V187() V188() V189() V195() L16()
the carrier of (TOP-REAL N) is non empty set
seq is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
|.seq.| is V11() V12() ext-real non negative Element of REAL
n1 is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
|.n1.| is V11() V12() ext-real non negative Element of REAL
|.seq.| - |.n1.| is V11() V12() ext-real Element of REAL
seq - n1 is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K292(seq,n1) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
|.(seq - n1).| is V11() V12() ext-real non negative Element of REAL
REAL N is non empty V42() M10( REAL )
n is V39(N) Element of REAL N
m is V39(N) Element of REAL N
n - m is Relation-like NAT -defined REAL -valued Function-like V39(N) V40() V116() V117() V118() M11( REAL , REAL N)
N is V4() V5() V6() V10() V11() V12() V30() V31() ext-real non negative V126() V127() V128() V129() V130() V131() Element of NAT
TOP-REAL N is non empty V70() V138() V139() TopSpace-like V183() V184() V185() V186() V187() V188() V189() V195() L16()
the carrier of (TOP-REAL N) is non empty set
seq is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
n1 is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
seq - n1 is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K292(seq,n1) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
|.(seq - n1).| is V11() V12() ext-real non negative Element of REAL
REAL N is non empty V42() M10( REAL )
n is V39(N) Element of REAL N
m is V39(N) Element of REAL N
n - m is Relation-like NAT -defined REAL -valued Function-like V39(N) V40() V116() V117() V118() M11( REAL , REAL N)
N is V4() V5() V6() V10() V11() V12() V30() V31() ext-real non negative V126() V127() V128() V129() V130() V131() Element of NAT
TOP-REAL N is non empty V70() V138() V139() TopSpace-like V183() V184() V185() V186() V187() V188() V189() V195() L16()
the carrier of (TOP-REAL N) is non empty set
seq is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
n1 is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
seq - n1 is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K292(seq,n1) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
|.(seq - n1).| is V11() V12() ext-real non negative Element of REAL
n is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
seq - n is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K292(seq,n) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
|.(seq - n).| is V11() V12() ext-real non negative Element of REAL
n - n1 is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K292(n,n1) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
|.(n - n1).| is V11() V12() ext-real non negative Element of REAL
|.(seq - n).| + |.(n - n1).| is V11() V12() ext-real non negative Element of REAL
0. (TOP-REAL N) is Relation-like Function-like V39(N) V40() V51( TOP-REAL N) V116() V117() V118() Element of the carrier of (TOP-REAL N)
the ZeroF of (TOP-REAL N) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
n - n is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K292(n,n) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
- n is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K290(n) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
(- n) + n is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K288((- n),n) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
seq + ((- n) + n) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K288(seq,((- n) + n)) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
(seq + ((- n) + n)) - n1 is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K292((seq + ((- n) + n)),n1) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
|.((seq + ((- n) + n)) - n1).| is V11() V12() ext-real non negative Element of REAL
seq + (- n) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K288(seq,(- n)) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
(seq + (- n)) + n is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K288((seq + (- n)),n) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
((seq + (- n)) + n) - n1 is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K292(((seq + (- n)) + n),n1) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
|.(((seq + (- n)) + n) - n1).| is V11() V12() ext-real non negative Element of REAL
(seq - n) + n is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K288((seq - n),n) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
((seq - n) + n) - n1 is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K292(((seq - n) + n),n1) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
|.(((seq - n) + n) - n1).| is V11() V12() ext-real non negative Element of REAL
(seq - n) + (n - n1) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K288((seq - n),(n - n1)) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
|.((seq - n) + (n - n1)).| is V11() V12() ext-real non negative Element of REAL
N is V4() V5() V6() V10() V11() V12() V30() V31() ext-real non negative V126() V127() V128() V129() V130() V131() Element of NAT
TOP-REAL N is non empty V70() V138() V139() TopSpace-like V183() V184() V185() V186() V187() V188() V189() V195() L16()
the carrier of (TOP-REAL N) is non empty set
K7(NAT, the carrier of (TOP-REAL N)) is set
K6(K7(NAT, the carrier of (TOP-REAL N))) is set
N is V4() V5() V6() V10() V11() V12() V30() V31() ext-real non negative V126() V127() V128() V129() V130() V131() Element of NAT
TOP-REAL N is non empty V70() V138() V139() TopSpace-like V183() V184() V185() V186() V187() V188() V189() V195() L16()
the carrier of (TOP-REAL N) is non empty set
K7(NAT, the carrier of (TOP-REAL N)) is set
K6(K7(NAT, the carrier of (TOP-REAL N))) is set
seq is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
n1 is V4() V5() V6() V10() V11() V12() V30() V31() ext-real non negative V126() V127() V128() V129() V130() V131() Element of NAT
n1 + 1 is non empty V4() V5() V6() V10() V11() V12() V30() V31() ext-real positive non negative V126() V127() V128() V129() V130() V131() Element of NAT
n is V11() V12() ext-real Element of REAL
seq . (n1 + 1) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
|.(seq . (n1 + 1)).| is V11() V12() ext-real non negative Element of REAL
|.(seq . (n1 + 1)).| + 1 is non empty V11() V12() ext-real positive non negative Element of REAL
m is non empty V11() V12() ext-real positive non negative Element of REAL
r1 is V4() V5() V6() V10() V11() V12() V30() V31() ext-real non negative V126() V127() V128() V129() V130() V131() Element of NAT
seq . r1 is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
|.(seq . r1).| is V11() V12() ext-real non negative Element of REAL
|.(seq . r1).| + 0 is V11() V12() ext-real non negative Element of REAL
n + 1 is V11() V12() ext-real Element of REAL
m is V11() V12() ext-real Element of REAL
r1 is V4() V5() V6() V10() V11() V12() V30() V31() ext-real non negative V126() V127() V128() V129() V130() V131() Element of NAT
seq . r1 is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
|.(seq . r1).| is V11() V12() ext-real non negative Element of REAL
n + 0 is V11() V12() ext-real Element of REAL
m is V11() V12() ext-real Element of REAL
r1 is non empty V11() V12() ext-real positive non negative Element of REAL
seq . 0 is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
|.(seq . 0).| is V11() V12() ext-real non negative Element of REAL
|.(seq . 0).| + 1 is non empty V11() V12() ext-real positive non negative Element of REAL
n1 is non empty V11() V12() ext-real positive non negative Element of REAL
n is V4() V5() V6() V10() V11() V12() V30() V31() ext-real non negative V126() V127() V128() V129() V130() V131() Element of NAT
seq . n is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
|.(seq . n).| is V11() V12() ext-real non negative Element of REAL
|.(seq . n).| + 0 is V11() V12() ext-real non negative Element of REAL
N is V4() V5() V6() V10() V11() V12() V30() V31() ext-real non negative V126() V127() V128() V129() V130() V131() Element of NAT
TOP-REAL N is non empty V70() V138() V139() TopSpace-like V183() V184() V185() V186() V187() V188() V189() V195() L16()
the carrier of (TOP-REAL N) is non empty set
K7(NAT, the carrier of (TOP-REAL N)) is set
K6(K7(NAT, the carrier of (TOP-REAL N))) is set
N is V4() V5() V6() V10() V11() V12() V30() V31() ext-real non negative V126() V127() V128() V129() V130() V131() Element of NAT
TOP-REAL N is non empty V70() V138() V139() TopSpace-like V183() V184() V185() V186() V187() V188() V189() V195() L16()
the carrier of (TOP-REAL N) is non empty set
K7(NAT, the carrier of (TOP-REAL N)) is set
K6(K7(NAT, the carrier of (TOP-REAL N))) is set
seq is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
n1 is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
n is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
n1 - n is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K292(n1,n) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
|.(n1 - n).| is V11() V12() ext-real non negative Element of REAL
0. (TOP-REAL N) is Relation-like Function-like V39(N) V40() V51( TOP-REAL N) V116() V117() V118() Element of the carrier of (TOP-REAL N)
the ZeroF of (TOP-REAL N) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
(0. (TOP-REAL N)) + n is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K288((0. (TOP-REAL N)),n) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
(n1 - n) + n is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K288((n1 - n),n) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
n - n is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K292(n,n) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
n1 - (n - n) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K292(n1,(n - n)) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
n1 - (0. (TOP-REAL N)) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K292(n1,(0. (TOP-REAL N))) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
- (0. (TOP-REAL N)) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K290((0. (TOP-REAL N))) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
n1 + (- (0. (TOP-REAL N))) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K288(n1,(- (0. (TOP-REAL N)))) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
(- 1) * (0. (TOP-REAL N)) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K294((0. (TOP-REAL N)),(- 1)) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
n1 + ((- 1) * (0. (TOP-REAL N))) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K288(n1,((- 1) * (0. (TOP-REAL N)))) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
n1 + (0. (TOP-REAL N)) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K288(n1,(0. (TOP-REAL N))) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
|.(n1 - n).| / 4 is V11() V12() ext-real non negative Element of REAL
m is V4() V5() V6() V10() V11() V12() V30() V31() ext-real non negative V126() V127() V128() V129() V130() V131() Element of NAT
r1 is V4() V5() V6() V10() V11() V12() V30() V31() ext-real non negative V126() V127() V128() V129() V130() V131() Element of NAT
m + r1 is V4() V5() V6() V10() V11() V12() V30() V31() ext-real non negative V126() V127() V128() V129() V130() V131() Element of NAT
seq . (m + r1) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
(seq . (m + r1)) - n is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K292((seq . (m + r1)),n) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
|.((seq . (m + r1)) - n).| is V11() V12() ext-real non negative Element of REAL
(seq . (m + r1)) - n1 is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K292((seq . (m + r1)),n1) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
|.((seq . (m + r1)) - n1).| is V11() V12() ext-real non negative Element of REAL
(|.(n1 - n).| / 4) + (|.(n1 - n).| / 4) is V11() V12() ext-real non negative Element of REAL
|.((seq . (m + r1)) - n).| + |.((seq . (m + r1)) - n1).| is V11() V12() ext-real non negative Element of REAL
(n1 - n) + (0. (TOP-REAL N)) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K288((n1 - n),(0. (TOP-REAL N))) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
|.((n1 - n) + (0. (TOP-REAL N))).| is V11() V12() ext-real non negative Element of REAL
(n1 - n) + ((- 1) * (0. (TOP-REAL N))) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K288((n1 - n),((- 1) * (0. (TOP-REAL N)))) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
|.((n1 - n) + ((- 1) * (0. (TOP-REAL N)))).| is V11() V12() ext-real non negative Element of REAL
(n1 - n) + (- (0. (TOP-REAL N))) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K288((n1 - n),(- (0. (TOP-REAL N)))) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
|.((n1 - n) + (- (0. (TOP-REAL N)))).| is V11() V12() ext-real non negative Element of REAL
(n1 - n) - (0. (TOP-REAL N)) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K292((n1 - n),(0. (TOP-REAL N))) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
|.((n1 - n) - (0. (TOP-REAL N))).| is V11() V12() ext-real non negative Element of REAL
(seq . (m + r1)) - (seq . (m + r1)) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K292((seq . (m + r1)),(seq . (m + r1))) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
(n1 - n) - ((seq . (m + r1)) - (seq . (m + r1))) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K292((n1 - n),((seq . (m + r1)) - (seq . (m + r1)))) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
|.((n1 - n) - ((seq . (m + r1)) - (seq . (m + r1)))).| is V11() V12() ext-real non negative Element of REAL
(n1 - n) - (seq . (m + r1)) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K292((n1 - n),(seq . (m + r1))) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
((n1 - n) - (seq . (m + r1))) + (seq . (m + r1)) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K288(((n1 - n) - (seq . (m + r1))),(seq . (m + r1))) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
|.(((n1 - n) - (seq . (m + r1))) + (seq . (m + r1))).| is V11() V12() ext-real non negative Element of REAL
(seq . (m + r1)) + n is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K288((seq . (m + r1)),n) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
n1 - ((seq . (m + r1)) + n) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K292(n1,((seq . (m + r1)) + n)) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
(n1 - ((seq . (m + r1)) + n)) + (seq . (m + r1)) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K288((n1 - ((seq . (m + r1)) + n)),(seq . (m + r1))) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
|.((n1 - ((seq . (m + r1)) + n)) + (seq . (m + r1))).| is V11() V12() ext-real non negative Element of REAL
n1 - (seq . (m + r1)) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K292(n1,(seq . (m + r1))) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
(n1 - (seq . (m + r1))) - n is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K292((n1 - (seq . (m + r1))),n) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
((n1 - (seq . (m + r1))) - n) + (seq . (m + r1)) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K288(((n1 - (seq . (m + r1))) - n),(seq . (m + r1))) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
|.(((n1 - (seq . (m + r1))) - n) + (seq . (m + r1))).| is V11() V12() ext-real non negative Element of REAL
n - (seq . (m + r1)) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K292(n,(seq . (m + r1))) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
(n1 - (seq . (m + r1))) - (n - (seq . (m + r1))) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K292((n1 - (seq . (m + r1))),(n - (seq . (m + r1)))) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
|.((n1 - (seq . (m + r1))) - (n - (seq . (m + r1)))).| is V11() V12() ext-real non negative Element of REAL
- (n - (seq . (m + r1))) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K290((n - (seq . (m + r1)))) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
(n1 - (seq . (m + r1))) + (- (n - (seq . (m + r1)))) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K288((n1 - (seq . (m + r1))),(- (n - (seq . (m + r1))))) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
|.((n1 - (seq . (m + r1))) + (- (n - (seq . (m + r1))))).| is V11() V12() ext-real non negative Element of REAL
(n1 - (seq . (m + r1))) + ((seq . (m + r1)) - n) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K288((n1 - (seq . (m + r1))),((seq . (m + r1)) - n)) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
|.((n1 - (seq . (m + r1))) + ((seq . (m + r1)) - n)).| is V11() V12() ext-real non negative Element of REAL
- ((seq . (m + r1)) - n1) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K290(((seq . (m + r1)) - n1)) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
(- ((seq . (m + r1)) - n1)) + ((seq . (m + r1)) - n) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K288((- ((seq . (m + r1)) - n1)),((seq . (m + r1)) - n)) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
|.((- ((seq . (m + r1)) - n1)) + ((seq . (m + r1)) - n)).| is V11() V12() ext-real non negative Element of REAL
|.(- ((seq . (m + r1)) - n1)).| is V11() V12() ext-real non negative Element of REAL
|.(- ((seq . (m + r1)) - n1)).| + |.((seq . (m + r1)) - n).| is V11() V12() ext-real non negative Element of REAL
|.((seq . (m + r1)) - n1).| + |.((seq . (m + r1)) - n).| is V11() V12() ext-real non negative Element of REAL
|.(n1 - n).| / 2 is V11() V12() ext-real non negative Element of REAL
N is V4() V5() V6() V10() V11() V12() V30() V31() ext-real non negative V126() V127() V128() V129() V130() V131() Element of NAT
TOP-REAL N is non empty V70() V138() V139() TopSpace-like V183() V184() V185() V186() V187() V188() V189() V195() L16()
the carrier of (TOP-REAL N) is non empty set
K7(NAT, the carrier of (TOP-REAL N)) is set
K6(K7(NAT, the carrier of (TOP-REAL N))) is set
seq is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
n1 is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
(N,seq,n1) is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
seq + n1 is Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
n is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
m is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
n + m is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K288(n,m) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
r1 is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
r is V11() V12() ext-real Element of REAL
r / 2 is V11() V12() ext-real Element of REAL
m is V4() V5() V6() V10() V11() V12() V30() V31() ext-real non negative V126() V127() V128() V129() V130() V131() Element of NAT
m is V4() V5() V6() V10() V11() V12() V30() V31() ext-real non negative V126() V127() V128() V129() V130() V131() Element of NAT
m + m is V4() V5() V6() V10() V11() V12() V30() V31() ext-real non negative V126() V127() V128() V129() V130() V131() Element of NAT
k is V4() V5() V6() V10() V11() V12() V30() V31() ext-real non negative V126() V127() V128() V129() V130() V131() Element of NAT
m is V4() V5() V6() V10() V11() V12() V30() V31() ext-real non negative V126() V127() V128() V129() V130() V131() Element of NAT
(N,seq,n1) . m is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
((N,seq,n1) . m) - r1 is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K292(((N,seq,n1) . m),r1) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
|.(((N,seq,n1) . m) - r1).| is V11() V12() ext-real non negative Element of REAL
n1 . m is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
(n1 . m) - m is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K292((n1 . m),m) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
|.((n1 . m) - m).| is V11() V12() ext-real non negative Element of REAL
seq . m is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
(seq . m) + (n1 . m) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K288((seq . m),(n1 . m)) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
((seq . m) + (n1 . m)) - (n + m) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K292(((seq . m) + (n1 . m)),(n + m)) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
|.(((seq . m) + (n1 . m)) - (n + m)).| is V11() V12() ext-real non negative Element of REAL
(n1 . m) - (n + m) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K292((n1 . m),(n + m)) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
(seq . m) + ((n1 . m) - (n + m)) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K288((seq . m),((n1 . m) - (n + m))) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
|.((seq . m) + ((n1 . m) - (n + m))).| is V11() V12() ext-real non negative Element of REAL
- (n + m) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K290((n + m)) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
(- (n + m)) + (n1 . m) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K288((- (n + m)),(n1 . m)) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
(seq . m) + ((- (n + m)) + (n1 . m)) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K288((seq . m),((- (n + m)) + (n1 . m))) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
|.((seq . m) + ((- (n + m)) + (n1 . m))).| is V11() V12() ext-real non negative Element of REAL
(seq . m) + (- (n + m)) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K288((seq . m),(- (n + m))) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
((seq . m) + (- (n + m))) + (n1 . m) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K288(((seq . m) + (- (n + m))),(n1 . m)) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
|.(((seq . m) + (- (n + m))) + (n1 . m)).| is V11() V12() ext-real non negative Element of REAL
(seq . m) - (n + m) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K292((seq . m),(n + m)) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
((seq . m) - (n + m)) + (n1 . m) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K288(((seq . m) - (n + m)),(n1 . m)) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
|.(((seq . m) - (n + m)) + (n1 . m)).| is V11() V12() ext-real non negative Element of REAL
(seq . m) - n is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K292((seq . m),n) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
((seq . m) - n) - m is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K292(((seq . m) - n),m) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
(((seq . m) - n) - m) + (n1 . m) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K288((((seq . m) - n) - m),(n1 . m)) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
|.((((seq . m) - n) - m) + (n1 . m)).| is V11() V12() ext-real non negative Element of REAL
- m is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K290(m) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
((seq . m) - n) + (- m) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K288(((seq . m) - n),(- m)) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
(((seq . m) - n) + (- m)) + (n1 . m) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K288((((seq . m) - n) + (- m)),(n1 . m)) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
|.((((seq . m) - n) + (- m)) + (n1 . m)).| is V11() V12() ext-real non negative Element of REAL
(n1 . m) + (- m) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K288((n1 . m),(- m)) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
((seq . m) - n) + ((n1 . m) + (- m)) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K288(((seq . m) - n),((n1 . m) + (- m))) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
|.(((seq . m) - n) + ((n1 . m) + (- m))).| is V11() V12() ext-real non negative Element of REAL
((seq . m) - n) + ((n1 . m) - m) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K288(((seq . m) - n),((n1 . m) - m)) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
|.(((seq . m) - n) + ((n1 . m) - m)).| is V11() V12() ext-real non negative Element of REAL
|.((seq . m) - n).| is V11() V12() ext-real non negative Element of REAL
|.((seq . m) - n).| + |.((n1 . m) - m).| is V11() V12() ext-real non negative Element of REAL
(r / 2) + (r / 2) is V11() V12() ext-real Element of REAL
N is V4() V5() V6() V10() V11() V12() V30() V31() ext-real non negative V126() V127() V128() V129() V130() V131() Element of NAT
TOP-REAL N is non empty V70() V138() V139() TopSpace-like V183() V184() V185() V186() V187() V188() V189() V195() L16()
the carrier of (TOP-REAL N) is non empty set
K7(NAT, the carrier of (TOP-REAL N)) is set
K6(K7(NAT, the carrier of (TOP-REAL N))) is set
seq is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
(N,seq) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
n1 is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
(N,seq,n1) is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
seq + n1 is Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
(N,(N,seq,n1)) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
(N,n1) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
(N,seq) + (N,n1) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K288((N,seq),(N,n1)) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
n is V11() V12() ext-real Element of REAL
n / 2 is V11() V12() ext-real Element of REAL
m is V4() V5() V6() V10() V11() V12() V30() V31() ext-real non negative V126() V127() V128() V129() V130() V131() Element of NAT
r1 is V4() V5() V6() V10() V11() V12() V30() V31() ext-real non negative V126() V127() V128() V129() V130() V131() Element of NAT
m + r1 is V4() V5() V6() V10() V11() V12() V30() V31() ext-real non negative V126() V127() V128() V129() V130() V131() Element of NAT
r is V4() V5() V6() V10() V11() V12() V30() V31() ext-real non negative V126() V127() V128() V129() V130() V131() Element of NAT
m is V4() V5() V6() V10() V11() V12() V30() V31() ext-real non negative V126() V127() V128() V129() V130() V131() Element of NAT
n1 . m is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
(n1 . m) - (N,n1) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K292((n1 . m),(N,n1)) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
|.((n1 . m) - (N,n1)).| is V11() V12() ext-real non negative Element of REAL
(N,seq,n1) . m is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
((N,seq,n1) . m) - ((N,seq) + (N,n1)) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K292(((N,seq,n1) . m),((N,seq) + (N,n1))) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
|.(((N,seq,n1) . m) - ((N,seq) + (N,n1))).| is V11() V12() ext-real non negative Element of REAL
((N,seq,n1) . m) - (N,seq) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K292(((N,seq,n1) . m),(N,seq)) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
(((N,seq,n1) . m) - (N,seq)) - (N,n1) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K292((((N,seq,n1) . m) - (N,seq)),(N,n1)) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
|.((((N,seq,n1) . m) - (N,seq)) - (N,n1)).| is V11() V12() ext-real non negative Element of REAL
seq . m is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
(seq . m) + (n1 . m) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K288((seq . m),(n1 . m)) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
((seq . m) + (n1 . m)) - (N,seq) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K292(((seq . m) + (n1 . m)),(N,seq)) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
(((seq . m) + (n1 . m)) - (N,seq)) - (N,n1) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K292((((seq . m) + (n1 . m)) - (N,seq)),(N,n1)) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
|.((((seq . m) + (n1 . m)) - (N,seq)) - (N,n1)).| is V11() V12() ext-real non negative Element of REAL
(n1 . m) - (N,seq) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K292((n1 . m),(N,seq)) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
(seq . m) + ((n1 . m) - (N,seq)) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K288((seq . m),((n1 . m) - (N,seq))) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
((seq . m) + ((n1 . m) - (N,seq))) - (N,n1) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K292(((seq . m) + ((n1 . m) - (N,seq))),(N,n1)) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
|.(((seq . m) + ((n1 . m) - (N,seq))) - (N,n1)).| is V11() V12() ext-real non negative Element of REAL
- (N,seq) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K290((N,seq)) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
(- (N,seq)) + (n1 . m) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K288((- (N,seq)),(n1 . m)) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
(seq . m) + ((- (N,seq)) + (n1 . m)) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K288((seq . m),((- (N,seq)) + (n1 . m))) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
((seq . m) + ((- (N,seq)) + (n1 . m))) - (N,n1) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K292(((seq . m) + ((- (N,seq)) + (n1 . m))),(N,n1)) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
|.(((seq . m) + ((- (N,seq)) + (n1 . m))) - (N,n1)).| is V11() V12() ext-real non negative Element of REAL
(seq . m) + (- (N,seq)) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K288((seq . m),(- (N,seq))) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
((seq . m) + (- (N,seq))) + (n1 . m) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K288(((seq . m) + (- (N,seq))),(n1 . m)) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
(((seq . m) + (- (N,seq))) + (n1 . m)) - (N,n1) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K292((((seq . m) + (- (N,seq))) + (n1 . m)),(N,n1)) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
|.((((seq . m) + (- (N,seq))) + (n1 . m)) - (N,n1)).| is V11() V12() ext-real non negative Element of REAL
(seq . m) - (N,seq) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K292((seq . m),(N,seq)) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
((seq . m) - (N,seq)) + (n1 . m) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K288(((seq . m) - (N,seq)),(n1 . m)) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
(((seq . m) - (N,seq)) + (n1 . m)) - (N,n1) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K292((((seq . m) - (N,seq)) + (n1 . m)),(N,n1)) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
|.((((seq . m) - (N,seq)) + (n1 . m)) - (N,n1)).| is V11() V12() ext-real non negative Element of REAL
((seq . m) - (N,seq)) + ((n1 . m) - (N,n1)) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K288(((seq . m) - (N,seq)),((n1 . m) - (N,n1))) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
|.(((seq . m) - (N,seq)) + ((n1 . m) - (N,n1))).| is V11() V12() ext-real non negative Element of REAL
|.((seq . m) - (N,seq)).| is V11() V12() ext-real non negative Element of REAL
|.((seq . m) - (N,seq)).| + |.((n1 . m) - (N,n1)).| is V11() V12() ext-real non negative Element of REAL
(n / 2) + (n / 2) is V11() V12() ext-real Element of REAL
N is V4() V5() V6() V10() V11() V12() V30() V31() ext-real non negative V126() V127() V128() V129() V130() V131() Element of NAT
TOP-REAL N is non empty V70() V138() V139() TopSpace-like V183() V184() V185() V186() V187() V188() V189() V195() L16()
the carrier of (TOP-REAL N) is non empty set
K7(NAT, the carrier of (TOP-REAL N)) is set
K6(K7(NAT, the carrier of (TOP-REAL N))) is set
seq is V11() V12() ext-real Element of REAL
n1 is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
(seq,N,n1) is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
seq (#) n1 is Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
n is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
seq * n is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K294(n,seq) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
abs seq is V11() V12() ext-real Element of REAL
0 / (abs seq) is V11() V12() ext-real Element of REAL
r1 is V11() V12() ext-real Element of REAL
r1 / (abs seq) is V11() V12() ext-real Element of REAL
r is V4() V5() V6() V10() V11() V12() V30() V31() ext-real non negative V126() V127() V128() V129() V130() V131() Element of NAT
m is V4() V5() V6() V10() V11() V12() V30() V31() ext-real non negative V126() V127() V128() V129() V130() V131() Element of NAT
m is V4() V5() V6() V10() V11() V12() V30() V31() ext-real non negative V126() V127() V128() V129() V130() V131() Element of NAT
n1 . m is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
(n1 . m) - n is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K292((n1 . m),n) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
|.((n1 . m) - n).| is V11() V12() ext-real non negative Element of REAL
(abs seq) * (r1 / (abs seq)) is V11() V12() ext-real Element of REAL
(abs seq) " is V11() V12() ext-real Element of REAL
((abs seq) ") * r1 is V11() V12() ext-real Element of REAL
(abs seq) * (((abs seq) ") * r1) is V11() V12() ext-real Element of REAL
(abs seq) * ((abs seq) ") is V11() V12() ext-real Element of REAL
((abs seq) * ((abs seq) ")) * r1 is V11() V12() ext-real Element of REAL
1 * r1 is V11() V12() ext-real Element of REAL
(seq,N,n1) . m is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
((seq,N,n1) . m) - (seq * n) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K292(((seq,N,n1) . m),(seq * n)) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
|.(((seq,N,n1) . m) - (seq * n)).| is V11() V12() ext-real non negative Element of REAL
seq * (n1 . m) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K294((n1 . m),seq) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
(seq * (n1 . m)) - (seq * n) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K292((seq * (n1 . m)),(seq * n)) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
|.((seq * (n1 . m)) - (seq * n)).| is V11() V12() ext-real non negative Element of REAL
seq * ((n1 . m) - n) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K294(((n1 . m) - n),seq) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
|.(seq * ((n1 . m) - n)).| is V11() V12() ext-real non negative Element of REAL
(abs seq) * |.((n1 . m) - n).| is V11() V12() ext-real Element of REAL
r1 is V11() V12() ext-real Element of REAL
r is empty V4() V5() V6() V8() V9() V10() V11() V12() V30() V31() ext-real non positive non negative V126() V127() V128() V129() V130() V131() V132() Element of NAT
m is V4() V5() V6() V10() V11() V12() V30() V31() ext-real non negative V126() V127() V128() V129() V130() V131() Element of NAT
(seq,N,n1) . m is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
((seq,N,n1) . m) - (seq * n) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K292(((seq,N,n1) . m),(seq * n)) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
|.(((seq,N,n1) . m) - (seq * n)).| is V11() V12() ext-real non negative Element of REAL
(0,N,n1) is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
0 (#) n1 is Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
(0,N,n1) . m is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
0. (TOP-REAL N) is Relation-like Function-like V39(N) V40() V51( TOP-REAL N) V116() V117() V118() Element of the carrier of (TOP-REAL N)
the ZeroF of (TOP-REAL N) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
((0,N,n1) . m) - (0. (TOP-REAL N)) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K292(((0,N,n1) . m),(0. (TOP-REAL N))) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
|.(((0,N,n1) . m) - (0. (TOP-REAL N))).| is V11() V12() ext-real non negative Element of REAL
(0. (TOP-REAL N)) - ((0,N,n1) . m) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K292((0. (TOP-REAL N)),((0,N,n1) . m)) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
|.((0. (TOP-REAL N)) - ((0,N,n1) . m)).| is V11() V12() ext-real non negative Element of REAL
- ((0,N,n1) . m) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K290(((0,N,n1) . m)) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
(0. (TOP-REAL N)) + (- ((0,N,n1) . m)) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K288((0. (TOP-REAL N)),(- ((0,N,n1) . m))) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
|.((0. (TOP-REAL N)) + (- ((0,N,n1) . m))).| is V11() V12() ext-real non negative Element of REAL
|.(- ((0,N,n1) . m)).| is V11() V12() ext-real non negative Element of REAL
|.((0,N,n1) . m).| is V11() V12() ext-real non negative Element of REAL
n1 . m is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
0 * (n1 . m) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K294((n1 . m),0) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
|.(0 * (n1 . m)).| is V11() V12() ext-real non negative Element of REAL
|.(0. (TOP-REAL N)).| is V11() V12() ext-real non negative Element of REAL
N is V4() V5() V6() V10() V11() V12() V30() V31() ext-real non negative V126() V127() V128() V129() V130() V131() Element of NAT
TOP-REAL N is non empty V70() V138() V139() TopSpace-like V183() V184() V185() V186() V187() V188() V189() V195() L16()
the carrier of (TOP-REAL N) is non empty set
K7(NAT, the carrier of (TOP-REAL N)) is set
K6(K7(NAT, the carrier of (TOP-REAL N))) is set
seq is V11() V12() ext-real Element of REAL
n1 is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
(seq,N,n1) is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
seq (#) n1 is Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
(N,(seq,N,n1)) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
(N,n1) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
seq * (N,n1) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K294((N,n1),seq) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
n is V11() V12() ext-real Element of REAL
m is empty V4() V5() V6() V8() V9() V10() V11() V12() V30() V31() ext-real non positive non negative V126() V127() V128() V129() V130() V131() V132() Element of NAT
r1 is V4() V5() V6() V10() V11() V12() V30() V31() ext-real non negative V126() V127() V128() V129() V130() V131() Element of NAT
0. (TOP-REAL N) is Relation-like Function-like V39(N) V40() V51( TOP-REAL N) V116() V117() V118() Element of the carrier of (TOP-REAL N)
the ZeroF of (TOP-REAL N) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
(seq,N,n1) . r1 is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
((seq,N,n1) . r1) - (seq * (N,n1)) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K292(((seq,N,n1) . r1),(seq * (N,n1))) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
|.(((seq,N,n1) . r1) - (seq * (N,n1))).| is V11() V12() ext-real non negative Element of REAL
n1 . r1 is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
0 * (n1 . r1) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K294((n1 . r1),0) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
(0 * (n1 . r1)) - (0. (TOP-REAL N)) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K292((0 * (n1 . r1)),(0. (TOP-REAL N))) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
|.((0 * (n1 . r1)) - (0. (TOP-REAL N))).| is V11() V12() ext-real non negative Element of REAL
(0. (TOP-REAL N)) - (0 * (n1 . r1)) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K292((0. (TOP-REAL N)),(0 * (n1 . r1))) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
|.((0. (TOP-REAL N)) - (0 * (n1 . r1))).| is V11() V12() ext-real non negative Element of REAL
- (0 * (n1 . r1)) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K290((0 * (n1 . r1))) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
(0. (TOP-REAL N)) + (- (0 * (n1 . r1))) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K288((0. (TOP-REAL N)),(- (0 * (n1 . r1)))) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
|.((0. (TOP-REAL N)) + (- (0 * (n1 . r1)))).| is V11() V12() ext-real non negative Element of REAL
|.(- (0 * (n1 . r1))).| is V11() V12() ext-real non negative Element of REAL
|.(0 * (n1 . r1)).| is V11() V12() ext-real non negative Element of REAL
|.(0. (TOP-REAL N)).| is V11() V12() ext-real non negative Element of REAL
abs seq is V11() V12() ext-real Element of REAL
0 / (abs seq) is V11() V12() ext-real Element of REAL
n is V11() V12() ext-real Element of REAL
n / (abs seq) is V11() V12() ext-real Element of REAL
m is V4() V5() V6() V10() V11() V12() V30() V31() ext-real non negative V126() V127() V128() V129() V130() V131() Element of NAT
r1 is V4() V5() V6() V10() V11() V12() V30() V31() ext-real non negative V126() V127() V128() V129() V130() V131() Element of NAT
r is V4() V5() V6() V10() V11() V12() V30() V31() ext-real non negative V126() V127() V128() V129() V130() V131() Element of NAT
n1 . r is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
(n1 . r) - (N,n1) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K292((n1 . r),(N,n1)) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
|.((n1 . r) - (N,n1)).| is V11() V12() ext-real non negative Element of REAL
(abs seq) * (n / (abs seq)) is V11() V12() ext-real Element of REAL
(abs seq) " is V11() V12() ext-real Element of REAL
((abs seq) ") * n is V11() V12() ext-real Element of REAL
(abs seq) * (((abs seq) ") * n) is V11() V12() ext-real Element of REAL
(abs seq) * ((abs seq) ") is V11() V12() ext-real Element of REAL
((abs seq) * ((abs seq) ")) * n is V11() V12() ext-real Element of REAL
1 * n is V11() V12() ext-real Element of REAL
(seq,N,n1) . r is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
((seq,N,n1) . r) - (seq * (N,n1)) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K292(((seq,N,n1) . r),(seq * (N,n1))) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
|.(((seq,N,n1) . r) - (seq * (N,n1))).| is V11() V12() ext-real non negative Element of REAL
seq * (n1 . r) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K294((n1 . r),seq) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
(seq * (n1 . r)) - (seq * (N,n1)) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K292((seq * (n1 . r)),(seq * (N,n1))) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
|.((seq * (n1 . r)) - (seq * (N,n1))).| is V11() V12() ext-real non negative Element of REAL
seq * ((n1 . r) - (N,n1)) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K294(((n1 . r) - (N,n1)),seq) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
|.(seq * ((n1 . r) - (N,n1))).| is V11() V12() ext-real non negative Element of REAL
(abs seq) * |.((n1 . r) - (N,n1)).| is V11() V12() ext-real Element of REAL
N is V4() V5() V6() V10() V11() V12() V30() V31() ext-real non negative V126() V127() V128() V129() V130() V131() Element of NAT
TOP-REAL N is non empty V70() V138() V139() TopSpace-like V183() V184() V185() V186() V187() V188() V189() V195() L16()
the carrier of (TOP-REAL N) is non empty set
K7(NAT, the carrier of (TOP-REAL N)) is set
K6(K7(NAT, the carrier of (TOP-REAL N))) is set
seq is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
(N,seq) is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
- seq is Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
((- 1),N,seq) is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
(- 1) (#) seq is Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
N is V4() V5() V6() V10() V11() V12() V30() V31() ext-real non negative V126() V127() V128() V129() V130() V131() Element of NAT
TOP-REAL N is non empty V70() V138() V139() TopSpace-like V183() V184() V185() V186() V187() V188() V189() V195() L16()
the carrier of (TOP-REAL N) is non empty set
K7(NAT, the carrier of (TOP-REAL N)) is set
K6(K7(NAT, the carrier of (TOP-REAL N))) is set
seq is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
(N,seq) is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
- seq is Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
(N,(N,seq)) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
(N,seq) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
- (N,seq) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K290((N,seq)) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
((- 1),N,seq) is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
(- 1) (#) seq is Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
(N,((- 1),N,seq)) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
(- 1) * (N,seq) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K294((N,seq),(- 1)) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
1 * (N,seq) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K294((N,seq),1) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
- (1 * (N,seq)) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K290((1 * (N,seq))) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
N is V4() V5() V6() V10() V11() V12() V30() V31() ext-real non negative V126() V127() V128() V129() V130() V131() Element of NAT
TOP-REAL N is non empty V70() V138() V139() TopSpace-like V183() V184() V185() V186() V187() V188() V189() V195() L16()
the carrier of (TOP-REAL N) is non empty set
K7(NAT, the carrier of (TOP-REAL N)) is set
K6(K7(NAT, the carrier of (TOP-REAL N))) is set
seq is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
n1 is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
(N,seq,n1) is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
(N,n1) is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
- n1 is Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
(N,seq,(N,n1)) is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
seq + (N,n1) is Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
N is V4() V5() V6() V10() V11() V12() V30() V31() ext-real non negative V126() V127() V128() V129() V130() V131() Element of NAT
TOP-REAL N is non empty V70() V138() V139() TopSpace-like V183() V184() V185() V186() V187() V188() V189() V195() L16()
the carrier of (TOP-REAL N) is non empty set
K7(NAT, the carrier of (TOP-REAL N)) is set
K6(K7(NAT, the carrier of (TOP-REAL N))) is set
seq is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
(N,seq) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
n1 is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
(N,seq,n1) is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
(N,n1) is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
- n1 is Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
(N,seq,(N,n1)) is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
seq + (N,n1) is Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
(N,(N,seq,n1)) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
(N,n1) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
(N,seq) - (N,n1) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K292((N,seq),(N,n1)) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
(N,(N,n1)) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
(N,seq) + (N,(N,n1)) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K288((N,seq),(N,(N,n1))) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
- (N,n1) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K290((N,n1)) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
(N,seq) + (- (N,n1)) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K288((N,seq),(- (N,n1))) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
N is V4() V5() V6() V10() V11() V12() V30() V31() ext-real non negative V126() V127() V128() V129() V130() V131() Element of NAT
TOP-REAL N is non empty V70() V138() V139() TopSpace-like V183() V184() V185() V186() V187() V188() V189() V195() L16()
the carrier of (TOP-REAL N) is non empty set
K7(NAT, the carrier of (TOP-REAL N)) is set
K6(K7(NAT, the carrier of (TOP-REAL N))) is set
seq is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
n1 is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
n is V4() V5() V6() V10() V11() V12() V30() V31() ext-real non negative V126() V127() V128() V129() V130() V131() Element of NAT
|.n1.| is V11() V12() ext-real non negative Element of REAL
|.n1.| + 1 is non empty V11() V12() ext-real positive non negative Element of REAL
m is non empty V11() V12() ext-real positive non negative Element of REAL
r1 is V4() V5() V6() V10() V11() V12() V30() V31() ext-real non negative V126() V127() V128() V129() V130() V131() Element of NAT
seq . r1 is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
|.(seq . r1).| is V11() V12() ext-real non negative Element of REAL
|.(seq . r1).| - |.n1.| is V11() V12() ext-real Element of REAL
(|.(seq . r1).| - |.n1.|) + |.n1.| is V11() V12() ext-real Element of REAL
(seq . r1) - n1 is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K292((seq . r1),n1) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
|.((seq . r1) - n1).| is V11() V12() ext-real non negative Element of REAL
m is V11() V12() ext-real Element of REAL
r1 is non empty V11() V12() ext-real positive non negative Element of REAL
r1 is V11() V12() ext-real Element of REAL
r1 + m is V11() V12() ext-real Element of REAL
r is V11() V12() ext-real Element of REAL
0 + m is V11() V12() ext-real Element of REAL
m is V4() V5() V6() V10() V11() V12() V30() V31() ext-real non negative V126() V127() V128() V129() V130() V131() Element of NAT
seq . m is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
|.(seq . m).| is V11() V12() ext-real non negative Element of REAL
r1 + 0 is V11() V12() ext-real Element of REAL
m is V11() V12() ext-real Element of REAL
N is V4() V5() V6() V10() V11() V12() V30() V31() ext-real non negative V126() V127() V128() V129() V130() V131() Element of NAT
TOP-REAL N is non empty V70() V138() V139() TopSpace-like V183() V184() V185() V186() V187() V188() V189() V195() L16()
the carrier of (TOP-REAL N) is non empty set
K7(NAT, the carrier of (TOP-REAL N)) is set
K6(K7(NAT, the carrier of (TOP-REAL N))) is set
0. (TOP-REAL N) is Relation-like Function-like V39(N) V40() V51( TOP-REAL N) V116() V117() V118() Element of the carrier of (TOP-REAL N)
the ZeroF of (TOP-REAL N) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
seq is non empty Relation-like NAT -defined the carrier of (TOP-REAL N) -valued Function-like total V27( NAT , the carrier of (TOP-REAL N)) Element of K6(K7(NAT, the carrier of (TOP-REAL N)))
(N,seq) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
|.(N,seq).| is V11() V12() ext-real non negative Element of REAL
|.(N,seq).| / 2 is V11() V12() ext-real non negative Element of REAL
n1 is V4() V5() V6() V10() V11() V12() V30() V31() ext-real non negative V126() V127() V128() V129() V130() V131() Element of NAT
n is V4() V5() V6() V10() V11() V12() V30() V31() ext-real non negative V126() V127() V128() V129() V130() V131() Element of NAT
m is V4() V5() V6() V10() V11() V12() V30() V31() ext-real non negative V126() V127() V128() V129() V130() V131() Element of NAT
seq . m is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
|.(seq . m).| is V11() V12() ext-real non negative Element of REAL
(seq . m) - (N,seq) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K292((seq . m),(N,seq)) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
|.((seq . m) - (N,seq)).| is V11() V12() ext-real non negative Element of REAL
|.(N,seq).| - |.(seq . m).| is V11() V12() ext-real Element of REAL
(N,seq) - (seq . m) is Relation-like Function-like V39(N) V40() V116() V117() V118() Element of the carrier of (TOP-REAL N)
K292((N,seq),(seq . m)) is Relation-like NAT -defined REAL -valued Function-like V40() V116() V117() V118() M7( REAL )
|.((N,seq) - (seq . m)).| is V11() V12() ext-real non negative Element of REAL
|.(seq . m).| - (|.(N,seq).| / 2) is V11() V12() ext-real Element of REAL
(|.(N,seq).| / 2) + (|.(seq . m).| - (|.(N,seq).| / 2)) is V11() V12() ext-real Element of REAL
(|.(N,seq).| - |.(seq . m).|) + (|.(seq . m).| - (|.(N,seq).| / 2)) is V11() V12() ext-real Element of REAL