:: SEQ_1 semantic presentation

REAL is non empty V45() V46() V47() V51() V52() set
NAT is non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() Element of K19(REAL)
K19(REAL) is set
COMPLEX is non empty V45() V51() V52() set
RAT is non empty V45() V46() V47() V48() V51() V52() set
INT is non empty V45() V46() V47() V48() V49() V51() V52() set
{} is empty V21() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V31() real V45() V46() V47() V48() V49() V50() V51() set
1 is non empty V21() epsilon-transitive epsilon-connected ordinal natural V31() real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
0 is empty V21() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V31() real V33() V34() V45() V46() V47() V48() V49() V50() V51() Element of NAT
0 " is V21() V31() real set
K20(NAT,REAL) is complex-valued ext-real-valued real-valued set
K19(K20(NAT,REAL)) is set
r is Relation-like Function-like set
dom r is set
seq is set
r . seq is set
seq is set
rng r is set
n is set
r . n is set
r is Relation-like Function-like set
dom r is set
seq is V21() epsilon-transitive epsilon-connected ordinal natural V31() real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
r . seq is set
seq is set
r . seq is set
r is Relation-like Function-like complex-valued ext-real-valued real-valued set
seq is set
r . seq is V21() V31() real set
NAT --> 1 is Relation-like NAT -defined NAT -valued RAT -valued INT -valued Function-like non empty total V18( NAT , NAT ) complex-valued ext-real-valued real-valued natural-valued Element of K19(K20(NAT,NAT))
K20(NAT,NAT) is RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued set
K19(K20(NAT,NAT)) is set
r is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
rng r is V45() V46() V47() Element of K19(REAL)
{1} is non empty V45() V46() V47() V48() V49() V50() set
{0} is non empty V45() V46() V47() V48() V49() V50() set
REAL \ {0} is V45() V46() V47() Element of K19(REAL)
r is Relation-like non-zero NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
rng r is V45() V46() V47() Element of K19(REAL)
r is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
seq is set
(r,seq) is V21() V31() real Element of REAL
dom r is V45() V46() V47() V48() V49() V50() Element of K19(NAT)
K19(NAT) is set
rng r is V45() V46() V47() Element of K19(REAL)
rng r is V45() V46() V47() Element of K19(REAL)
dom r is V45() V46() V47() V48() V49() V50() Element of K19(NAT)
K19(NAT) is set
seq is set
(r,seq) is V21() V31() real Element of REAL
r is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
seq is V21() epsilon-transitive epsilon-connected ordinal natural V31() real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
(r,seq) is V21() V31() real Element of REAL
seq is set
(r,seq) is V21() V31() real Element of REAL
r is V21() V31() real set
{r} is non empty V45() V46() V47() set
seq is Relation-like Function-like set
dom seq is set
rng seq is set
n is set
n is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
rng n is V45() V46() V47() Element of K19(REAL)
r is set
seq is V21() epsilon-transitive epsilon-connected ordinal natural V31() real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
F₁(seq) is V21() V31() real set
n is set
seq1 is set
r is Relation-like Function-like set
dom r is set
seq is set
r . seq is set
n is V21() epsilon-transitive epsilon-connected ordinal natural V31() real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
F₁(n) is V21() V31() real set
seq is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
n is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
seq1 is V21() epsilon-transitive epsilon-connected ordinal natural V31() real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
(n,seq1) is V21() V31() real Element of REAL
F₁(seq1) is V21() V31() real set
n is V21() epsilon-transitive epsilon-connected ordinal natural V31() real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
F₁(n) is V21() V31() real set
F₁() is non empty set
F₂() is non empty set
K20(F₁(),F₂()) is set
K19(K20(F₁(),F₂())) is set
the Element of F₂() is Element of F₂()
seq is set
n is set
K19(F₁()) is set
seq1 is Element of F₁()
n is Element of F₂()
d is set
c₇ is Element of F₂()
seq1 is Relation-like F₁() -defined F₂() -valued Function-like non empty total V18(F₁(),F₂()) Element of K19(K20(F₁(),F₂()))
n is Element of K19(F₁())
seq1 | n is Relation-like F₁() -defined F₂() -valued Function-like Element of K19(K20(F₁(),F₂()))
n is Relation-like F₁() -defined F₂() -valued Function-like Element of K19(K20(F₁(),F₂()))
dom n is Element of K19(F₁())
dom seq1 is Element of K19(F₁())
d is Element of F₁()
c₇ is Element of F₂()
(dom seq1) /\ n is Element of K19(F₁())
d is Element of F₁()
n . d is set
seq1 . d is Element of F₂()
c₇ is Element of F₂()
F₂() is non empty set
F₁() is non empty set
K20(F₁(),F₂()) is set
K19(K20(F₁(),F₂())) is set
r is Relation-like F₁() -defined F₂() -valued Function-like Element of K19(K20(F₁(),F₂()))
dom r is Element of K19(F₁())
K19(F₁()) is set
seq is Element of F₁()
F₃(seq) is Element of F₂()
n is Element of F₂()
F₃(seq) is Element of F₂()
n is Element of F₂()
seq is Element of F₁()
r . seq is set
F₃(seq) is Element of F₂()
F₁() is set
F₂() is set
K20(F₁(),F₂()) is set
K19(K20(F₁(),F₂())) is set
F₃() is set
r is Relation-like F₁() -defined F₂() -valued Function-like Element of K19(K20(F₁(),F₂()))
dom r is Element of K19(F₁())
K19(F₁()) is set
seq is Relation-like F₁() -defined F₂() -valued Function-like Element of K19(K20(F₁(),F₂()))
dom seq is Element of K19(F₁())
n is Element of F₁()
r . n is set
F₄(n) is set
seq . n is set
r is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
seq is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
n is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
seq + n is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
seq1 is V21() epsilon-transitive epsilon-connected ordinal natural V31() real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
(r,seq1) is V21() V31() real Element of REAL
(seq,seq1) is V21() V31() real Element of REAL
(n,seq1) is V21() V31() real Element of REAL
(seq,seq1) + (n,seq1) is V21() V31() real Element of REAL
dom r is V45() V46() V47() V48() V49() V50() Element of K19(NAT)
K19(NAT) is set
dom r is V45() V46() V47() V48() V49() V50() Element of K19(NAT)
K19(NAT) is set
seq1 is set
(r,seq1) is V21() V31() real Element of REAL
(seq,seq1) is V21() V31() real Element of REAL
(n,seq1) is V21() V31() real Element of REAL
(seq,seq1) + (n,seq1) is V21() V31() real Element of REAL
NAT /\ NAT is V45() V46() V47() V48() V49() V50() Element of K19(REAL)
dom n is V45() V46() V47() V48() V49() V50() Element of K19(NAT)
NAT /\ (dom n) is V45() V46() V47() V48() V49() V50() Element of K19(NAT)
dom seq is V45() V46() V47() V48() V49() V50() Element of K19(NAT)
(dom seq) /\ (dom n) is V45() V46() V47() V48() V49() V50() Element of K19(NAT)
r is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
seq is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
n is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
seq (#) n is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
seq1 is V21() epsilon-transitive epsilon-connected ordinal natural V31() real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
(r,seq1) is V21() V31() real Element of REAL
(seq,seq1) is V21() V31() real Element of REAL
(n,seq1) is V21() V31() real Element of REAL
(seq,seq1) * (n,seq1) is V21() V31() real Element of REAL
dom r is V45() V46() V47() V48() V49() V50() Element of K19(NAT)
K19(NAT) is set
dom r is V45() V46() V47() V48() V49() V50() Element of K19(NAT)
K19(NAT) is set
seq1 is set
(r,seq1) is V21() V31() real Element of REAL
(seq,seq1) is V21() V31() real Element of REAL
(n,seq1) is V21() V31() real Element of REAL
(seq,seq1) * (n,seq1) is V21() V31() real Element of REAL
NAT /\ NAT is V45() V46() V47() V48() V49() V50() Element of K19(REAL)
dom n is V45() V46() V47() V48() V49() V50() Element of K19(NAT)
NAT /\ (dom n) is V45() V46() V47() V48() V49() V50() Element of K19(NAT)
dom seq is V45() V46() V47() V48() V49() V50() Element of K19(NAT)
(dom seq) /\ (dom n) is V45() V46() V47() V48() V49() V50() Element of K19(NAT)
r is V21() V31() real set
seq is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
n is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
r (#) n is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
seq1 is V21() epsilon-transitive epsilon-connected ordinal natural V31() real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
(seq,seq1) is V21() V31() real Element of REAL
(n,seq1) is V21() V31() real Element of REAL
r * (n,seq1) is V21() V31() real Element of REAL
dom seq is V45() V46() V47() V48() V49() V50() Element of K19(NAT)
K19(NAT) is set
seq1 is set
(seq,seq1) is V21() V31() real Element of REAL
(n,seq1) is V21() V31() real Element of REAL
r * (n,seq1) is V21() V31() real Element of REAL
dom n is V45() V46() V47() V48() V49() V50() Element of K19(NAT)
r is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
seq is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
- seq is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
- 1 is V21() V31() real set
(- 1) (#) seq is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
n is V21() epsilon-transitive epsilon-connected ordinal natural V31() real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
(r,n) is V21() V31() real Element of REAL
(seq,n) is V21() V31() real Element of REAL
- (seq,n) is V21() V31() real Element of REAL
dom r is V45() V46() V47() V48() V49() V50() Element of K19(NAT)
K19(NAT) is set
n is set
(r,n) is V21() V31() real Element of REAL
(seq,n) is V21() V31() real Element of REAL
- (seq,n) is V21() V31() real Element of REAL
dom seq is V45() V46() V47() V48() V49() V50() Element of K19(NAT)
r is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
seq is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
r - seq is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
- seq is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
- 1 is V21() V31() real set
(- 1) (#) seq is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
r + (- seq) is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
- seq is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
r + (- seq) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
r is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
seq is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
abs seq is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
n is V21() epsilon-transitive epsilon-connected ordinal natural V31() real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
(r,n) is V21() V31() real Element of REAL
(seq,n) is V21() V31() real Element of REAL
abs (seq,n) is V21() V31() real Element of REAL
dom r is V45() V46() V47() V48() V49() V50() Element of K19(NAT)
K19(NAT) is set
n is set
(r,n) is V21() V31() real Element of REAL
(seq,n) is V21() V31() real Element of REAL
abs (seq,n) is V21() V31() real Element of REAL
dom seq is V45() V46() V47() V48() V49() V50() Element of K19(NAT)
r is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
seq is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
r + seq is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
n is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(r + seq) + n is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
seq + n is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
r + (seq + n) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
seq1 is V21() epsilon-transitive epsilon-connected ordinal natural V31() real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
(((r + seq) + n),seq1) is V21() V31() real Element of REAL
((r + seq),seq1) is V21() V31() real Element of REAL
(n,seq1) is V21() V31() real Element of REAL
((r + seq),seq1) + (n,seq1) is V21() V31() real Element of REAL
(r,seq1) is V21() V31() real Element of REAL
(seq,seq1) is V21() V31() real Element of REAL
(r,seq1) + (seq,seq1) is V21() V31() real Element of REAL
((r,seq1) + (seq,seq1)) + (n,seq1) is V21() V31() real Element of REAL
(seq,seq1) + (n,seq1) is V21() V31() real Element of REAL
(r,seq1) + ((seq,seq1) + (n,seq1)) is V21() V31() real Element of REAL
((seq + n),seq1) is V21() V31() real Element of REAL
(r,seq1) + ((seq + n),seq1) is V21() V31() real Element of REAL
((r + (seq + n)),seq1) is V21() V31() real Element of REAL
r is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
seq is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
r (#) seq is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
n is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(r (#) seq) (#) n is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
seq (#) n is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
r (#) (seq (#) n) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
seq1 is V21() epsilon-transitive epsilon-connected ordinal natural V31() real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
(((r (#) seq) (#) n),seq1) is V21() V31() real Element of REAL
((r (#) seq),seq1) is V21() V31() real Element of REAL
(n,seq1) is V21() V31() real Element of REAL
((r (#) seq),seq1) * (n,seq1) is V21() V31() real Element of REAL
(r,seq1) is V21() V31() real Element of REAL
(seq,seq1) is V21() V31() real Element of REAL
(r,seq1) * (seq,seq1) is V21() V31() real Element of REAL
((r,seq1) * (seq,seq1)) * (n,seq1) is V21() V31() real Element of REAL
(seq,seq1) * (n,seq1) is V21() V31() real Element of REAL
(r,seq1) * ((seq,seq1) * (n,seq1)) is V21() V31() real Element of REAL
((seq (#) n),seq1) is V21() V31() real Element of REAL
(r,seq1) * ((seq (#) n),seq1) is V21() V31() real Element of REAL
((r (#) (seq (#) n)),seq1) is V21() V31() real Element of REAL
r is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
seq is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
r + seq is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
n is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(r + seq) (#) n is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
r (#) n is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
seq (#) n is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(r (#) n) + (seq (#) n) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
seq1 is V21() epsilon-transitive epsilon-connected ordinal natural V31() real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
(((r + seq) (#) n),seq1) is V21() V31() real Element of REAL
((r + seq),seq1) is V21() V31() real Element of REAL
(n,seq1) is V21() V31() real Element of REAL
((r + seq),seq1) * (n,seq1) is V21() V31() real Element of REAL
(r,seq1) is V21() V31() real Element of REAL
(seq,seq1) is V21() V31() real Element of REAL
(r,seq1) + (seq,seq1) is V21() V31() real Element of REAL
((r,seq1) + (seq,seq1)) * (n,seq1) is V21() V31() real Element of REAL
(r,seq1) * (n,seq1) is V21() V31() real Element of REAL
(seq,seq1) * (n,seq1) is V21() V31() real Element of REAL
((r,seq1) * (n,seq1)) + ((seq,seq1) * (n,seq1)) is V21() V31() real Element of REAL
((r (#) n),seq1) is V21() V31() real Element of REAL
((r (#) n),seq1) + ((seq,seq1) * (n,seq1)) is V21() V31() real Element of REAL
((seq (#) n),seq1) is V21() V31() real Element of REAL
((r (#) n),seq1) + ((seq (#) n),seq1) is V21() V31() real Element of REAL
(((r (#) n) + (seq (#) n)),seq1) is V21() V31() real Element of REAL
r is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
seq is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
n is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
seq + n is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
r (#) (seq + n) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
r (#) seq is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
r (#) n is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(r (#) seq) + (r (#) n) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
- 1 is V21() V31() real Element of REAL
r is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
- r is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
- 1 is V21() V31() real set
(- 1) (#) r is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
(- 1) (#) r is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
r is V21() V31() real set
seq is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
r (#) seq is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
n is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
seq (#) n is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
r (#) (seq (#) n) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(r (#) seq) (#) n is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
seq1 is V21() epsilon-transitive epsilon-connected ordinal natural V31() real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
((r (#) (seq (#) n)),seq1) is V21() V31() real Element of REAL
((seq (#) n),seq1) is V21() V31() real Element of REAL
r * ((seq (#) n),seq1) is V21() V31() real Element of REAL
(seq,seq1) is V21() V31() real Element of REAL
(n,seq1) is V21() V31() real Element of REAL
(seq,seq1) * (n,seq1) is V21() V31() real Element of REAL
r * ((seq,seq1) * (n,seq1)) is V21() V31() real Element of REAL
r * (seq,seq1) is V21() V31() real Element of REAL
(r * (seq,seq1)) * (n,seq1) is V21() V31() real Element of REAL
((r (#) seq),seq1) is V21() V31() real Element of REAL
((r (#) seq),seq1) * (n,seq1) is V21() V31() real Element of REAL
(((r (#) seq) (#) n),seq1) is V21() V31() real Element of REAL
r is V21() V31() real set
seq is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
n is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
seq (#) n is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
r (#) (seq (#) n) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
r (#) n is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
seq (#) (r (#) n) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
seq1 is V21() epsilon-transitive epsilon-connected ordinal natural V31() real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
((r (#) (seq (#) n)),seq1) is V21() V31() real Element of REAL
((seq (#) n),seq1) is V21() V31() real Element of REAL
r * ((seq (#) n),seq1) is V21() V31() real Element of REAL
(seq,seq1) is V21() V31() real Element of REAL
(n,seq1) is V21() V31() real Element of REAL
(seq,seq1) * (n,seq1) is V21() V31() real Element of REAL
r * ((seq,seq1) * (n,seq1)) is V21() V31() real Element of REAL
r * (n,seq1) is V21() V31() real Element of REAL
(seq,seq1) * (r * (n,seq1)) is V21() V31() real Element of REAL
((r (#) n),seq1) is V21() V31() real Element of REAL
(seq,seq1) * ((r (#) n),seq1) is V21() V31() real Element of REAL
((seq (#) (r (#) n)),seq1) is V21() V31() real Element of REAL
r is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
seq is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
r - seq is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
- seq is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
- 1 is V21() V31() real set
(- 1) (#) seq is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
r + (- seq) is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
n is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(r - seq) (#) n is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
r (#) n is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
seq (#) n is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(r (#) n) - (seq (#) n) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
- (seq (#) n) is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
(- 1) (#) (seq (#) n) is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
(r (#) n) + (- (seq (#) n)) is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
- seq is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(- seq) (#) n is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(r (#) n) + ((- seq) (#) n) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
r is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
seq is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
r (#) seq is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
n is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
r (#) n is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(r (#) seq) - (r (#) n) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
- (r (#) n) is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
- 1 is V21() V31() real set
(- 1) (#) (r (#) n) is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
(r (#) seq) + (- (r (#) n)) is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
seq - n is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
- n is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
(- 1) (#) n is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
seq + (- n) is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
r (#) (seq - n) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
r is V21() V31() real set
seq is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
r (#) seq is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
n is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
seq + n is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
r (#) (seq + n) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
r (#) n is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(r (#) seq) + (r (#) n) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
seq1 is V21() epsilon-transitive epsilon-connected ordinal natural V31() real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
((r (#) (seq + n)),seq1) is V21() V31() real Element of REAL
((seq + n),seq1) is V21() V31() real Element of REAL
r * ((seq + n),seq1) is V21() V31() real Element of REAL
(seq,seq1) is V21() V31() real Element of REAL
(n,seq1) is V21() V31() real Element of REAL
(seq,seq1) + (n,seq1) is V21() V31() real Element of REAL
r * ((seq,seq1) + (n,seq1)) is V21() V31() real Element of REAL
r * (seq,seq1) is V21() V31() real Element of REAL
r * (n,seq1) is V21() V31() real Element of REAL
(r * (seq,seq1)) + (r * (n,seq1)) is V21() V31() real Element of REAL
((r (#) seq),seq1) is V21() V31() real Element of REAL
((r (#) seq),seq1) + (r * (n,seq1)) is V21() V31() real Element of REAL
((r (#) n),seq1) is V21() V31() real Element of REAL
((r (#) seq),seq1) + ((r (#) n),seq1) is V21() V31() real Element of REAL
(((r (#) seq) + (r (#) n)),seq1) is V21() V31() real Element of REAL
r is V21() V31() real set
seq is V21() V31() real set
r * seq is V21() V31() real set
n is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(r * seq) (#) n is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
seq (#) n is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
r (#) (seq (#) n) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
seq1 is V21() epsilon-transitive epsilon-connected ordinal natural V31() real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
(((r * seq) (#) n),seq1) is V21() V31() real Element of REAL
(n,seq1) is V21() V31() real Element of REAL
(r * seq) * (n,seq1) is V21() V31() real Element of REAL
seq * (n,seq1) is V21() V31() real Element of REAL
r * (seq * (n,seq1)) is V21() V31() real Element of REAL
((seq (#) n),seq1) is V21() V31() real Element of REAL
r * ((seq (#) n),seq1) is V21() V31() real Element of REAL
((r (#) (seq (#) n)),seq1) is V21() V31() real Element of REAL
r is V21() V31() real set
seq is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
r (#) seq is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
n is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
seq - n is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
- n is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
- 1 is V21() V31() real set
(- 1) (#) n is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
seq + (- n) is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
r (#) (seq - n) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
r (#) n is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(r (#) seq) - (r (#) n) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
- (r (#) n) is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
(- 1) (#) (r (#) n) is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
(r (#) seq) + (- (r (#) n)) is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
- n is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
r (#) (- n) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(r (#) seq) + (r (#) (- n)) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(- 1) * r is V21() V31() real Element of REAL
((- 1) * r) (#) n is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(r (#) seq) + (((- 1) * r) (#) n) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
r is V21() V31() real set
seq is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
r (#) seq is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
n is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
seq /" n is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
n " is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
seq (#) (n ") is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
r (#) (seq /" n) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(r (#) seq) /" n is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(r (#) seq) (#) (n ") is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
n " is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
seq (#) (n ") is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
r (#) (seq (#) (n ")) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
r is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
seq is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
r - seq is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
- seq is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
- 1 is V21() V31() real set
(- 1) (#) seq is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
r + (- seq) is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
n is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
seq + n is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
r - (seq + n) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
- (seq + n) is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
(- 1) (#) (seq + n) is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
r + (- (seq + n)) is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
(r - seq) - n is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
- n is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
(- 1) (#) n is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
(r - seq) + (- n) is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
- seq is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(- 1) (#) n is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(- seq) + ((- 1) (#) n) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
r + ((- seq) + ((- 1) (#) n)) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
r is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
1 (#) r is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
seq is V21() epsilon-transitive epsilon-connected ordinal natural V31() real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
((1 (#) r),seq) is V21() V31() real Element of REAL
(r,seq) is V21() V31() real Element of REAL
1 * (r,seq) is V21() V31() real Element of REAL
r is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
seq is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
- seq is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
- 1 is V21() V31() real set
(- 1) (#) seq is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
r - (- seq) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
- (- seq) is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
(- 1) (#) (- seq) is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
r + (- (- seq)) is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
r + seq is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
r is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
seq is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
r - seq is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
- seq is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
- 1 is V21() V31() real set
(- 1) (#) seq is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
r + (- seq) is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
n is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
seq - n is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
- n is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
(- 1) (#) n is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
seq + (- n) is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
r - (seq - n) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
- (seq - n) is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
(- 1) (#) (seq - n) is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
r + (- (seq - n)) is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
(r - seq) + n is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
- seq is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
- n is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(- seq) - (- n) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
- (- n) is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
(- 1) (#) (- n) is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
(- seq) + (- (- n)) is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
r + ((- seq) - (- n)) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
r is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
seq is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
r + seq is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
n is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
seq - n is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
- n is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
- 1 is V21() V31() real set
(- 1) (#) n is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
seq + (- n) is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
r + (seq - n) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(r + seq) - n is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(r + seq) + (- n) is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
- n is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(r + seq) + (- n) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
r is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
- r is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
- 1 is V21() V31() real set
(- 1) (#) r is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
seq is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(- r) (#) seq is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
r (#) seq is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
- (r (#) seq) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(- 1) (#) (r (#) seq) is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
n is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
seq1 is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
- seq1 is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(- 1) (#) seq1 is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
n (#) (- seq1) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
n (#) seq1 is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
- (n (#) seq1) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(- 1) (#) (n (#) seq1) is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
r is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
r " is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
seq is V21() epsilon-transitive epsilon-connected ordinal natural V31() real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
((r "),seq) is V21() V31() real Element of REAL
(r,seq) is V21() V31() real Element of REAL
(r,seq) " is V21() V31() real Element of REAL
r is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
seq is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
r (#) seq is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
n is V21() epsilon-transitive epsilon-connected ordinal natural V31() real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
((r (#) seq),n) is V21() V31() real Element of REAL
(r,n) is V21() V31() real Element of REAL
(seq,n) is V21() V31() real Element of REAL
(r,n) * (seq,n) is V21() V31() real Element of REAL
n is V21() epsilon-transitive epsilon-connected ordinal natural V31() real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
((r (#) seq),n) is V21() V31() real Element of REAL
(r,n) is V21() V31() real Element of REAL
(seq,n) is V21() V31() real Element of REAL
(r,n) * (seq,n) is V21() V31() real Element of REAL
n is V21() epsilon-transitive epsilon-connected ordinal natural V31() real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
((r (#) seq),n) is V21() V31() real Element of REAL
(r,n) is V21() V31() real Element of REAL
(seq,n) is V21() V31() real Element of REAL
(r,n) * (seq,n) is V21() V31() real Element of REAL
r is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
r " is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
seq is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
seq " is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(r ") (#) (seq ") is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
r (#) seq is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(r (#) seq) " is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
n is V21() epsilon-transitive epsilon-connected ordinal natural V31() real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
(((r ") (#) (seq ")),n) is V21() V31() real Element of REAL
((r "),n) is V21() V31() real Element of REAL
((seq "),n) is V21() V31() real Element of REAL
((r "),n) * ((seq "),n) is V21() V31() real Element of REAL
(seq,n) is V21() V31() real Element of REAL
(seq,n) " is V21() V31() real Element of REAL
((r "),n) * ((seq,n) ") is V21() V31() real Element of REAL
(r,n) is V21() V31() real Element of REAL
(r,n) " is V21() V31() real Element of REAL
((r,n) ") * ((seq,n) ") is V21() V31() real Element of REAL
(r,n) * (seq,n) is V21() V31() real Element of REAL
((r,n) * (seq,n)) " is V21() V31() real Element of REAL
((r (#) seq),n) is V21() V31() real Element of REAL
((r (#) seq),n) " is V21() V31() real Element of REAL
(((r (#) seq) "),n) is V21() V31() real Element of REAL
r is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
seq is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
seq /" r is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
r " is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
seq (#) (r ") is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
(seq /" r) (#) r is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
n is V21() epsilon-transitive epsilon-connected ordinal natural V31() real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
(r,n) is V21() V31() real Element of REAL
(((seq /" r) (#) r),n) is V21() V31() real Element of REAL
r " is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
seq (#) (r ") is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
((seq (#) (r ")),n) is V21() V31() real Element of REAL
((seq (#) (r ")),n) * (r,n) is V21() V31() real Element of REAL
(seq,n) is V21() V31() real Element of REAL
((r "),n) is V21() V31() real Element of REAL
(seq,n) * ((r "),n) is V21() V31() real Element of REAL
((seq,n) * ((r "),n)) * (r,n) is V21() V31() real Element of REAL
(r,n) " is V21() V31() real Element of REAL
(seq,n) * ((r,n) ") is V21() V31() real Element of REAL
((seq,n) * ((r,n) ")) * (r,n) is V21() V31() real Element of REAL
((r,n) ") * (r,n) is V21() V31() real Element of REAL
(seq,n) * (((r,n) ") * (r,n)) is V21() V31() real Element of REAL
(seq,n) * 1 is V21() V31() real Element of REAL
r is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
seq is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
r /" seq is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
seq " is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
r (#) (seq ") is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
n is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
r (#) n is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
seq1 is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
n /" seq1 is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
seq1 " is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
n (#) (seq1 ") is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
(r /" seq) (#) (n /" seq1) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
seq (#) seq1 is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(r (#) n) /" (seq (#) seq1) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(seq (#) seq1) " is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
(r (#) n) (#) ((seq (#) seq1) ") is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
n is V21() epsilon-transitive epsilon-connected ordinal natural V31() real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
(((r /" seq) (#) (n /" seq1)),n) is V21() V31() real Element of REAL
seq " is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
r (#) (seq ") is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
((r (#) (seq ")),n) is V21() V31() real Element of REAL
((n /" seq1),n) is V21() V31() real Element of REAL
((r (#) (seq ")),n) * ((n /" seq1),n) is V21() V31() real Element of REAL
(r,n) is V21() V31() real Element of REAL
((seq "),n) is V21() V31() real Element of REAL
(r,n) * ((seq "),n) is V21() V31() real Element of REAL
seq1 " is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
n (#) (seq1 ") is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
((n (#) (seq1 ")),n) is V21() V31() real Element of REAL
((r,n) * ((seq "),n)) * ((n (#) (seq1 ")),n) is V21() V31() real Element of REAL
(n,n) is V21() V31() real Element of REAL
((seq1 "),n) is V21() V31() real Element of REAL
(n,n) * ((seq1 "),n) is V21() V31() real Element of REAL
((r,n) * ((seq "),n)) * ((n,n) * ((seq1 "),n)) is V21() V31() real Element of REAL
((seq "),n) * ((seq1 "),n) is V21() V31() real Element of REAL
(n,n) * (((seq "),n) * ((seq1 "),n)) is V21() V31() real Element of REAL
(r,n) * ((n,n) * (((seq "),n) * ((seq1 "),n))) is V21() V31() real Element of REAL
(seq ") (#) (seq1 ") is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(((seq ") (#) (seq1 ")),n) is V21() V31() real Element of REAL
(n,n) * (((seq ") (#) (seq1 ")),n) is V21() V31() real Element of REAL
(r,n) * ((n,n) * (((seq ") (#) (seq1 ")),n)) is V21() V31() real Element of REAL
(r,n) * (n,n) is V21() V31() real Element of REAL
((r,n) * (n,n)) * (((seq ") (#) (seq1 ")),n) is V21() V31() real Element of REAL
(seq (#) seq1) " is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(((seq (#) seq1) "),n) is V21() V31() real Element of REAL
((r,n) * (n,n)) * (((seq (#) seq1) "),n) is V21() V31() real Element of REAL
((r (#) n),n) is V21() V31() real Element of REAL
((r (#) n),n) * (((seq (#) seq1) "),n) is V21() V31() real Element of REAL
(((r (#) n) /" (seq (#) seq1)),n) is V21() V31() real Element of REAL
r is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
seq is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
r /" seq is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
seq " is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
r (#) (seq ") is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
seq " is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
r is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
seq is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
r /" seq is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
seq " is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
r (#) (seq ") is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
(r /" seq) " is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
seq /" r is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
r " is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
seq (#) (r ") is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
n is V21() epsilon-transitive epsilon-connected ordinal natural V31() real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
(((r /" seq) "),n) is V21() V31() real Element of REAL
r " is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
seq " is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(seq ") " is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(r ") (#) ((seq ") ") is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(((r ") (#) ((seq ") ")),n) is V21() V31() real Element of REAL
((seq /" r),n) is V21() V31() real Element of REAL
r is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
seq is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
r (#) seq is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
n is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
seq /" n is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
n " is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
seq (#) (n ") is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
r (#) (seq /" n) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(r (#) seq) /" n is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(r (#) seq) (#) (n ") is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
n " is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
seq (#) (n ") is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
r (#) (seq (#) (n ")) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
r is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
seq is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
n is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
seq /" n is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
n " is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
seq (#) (n ") is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
r /" (seq /" n) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(seq /" n) " is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
r (#) ((seq /" n) ") is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
r (#) n is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(r (#) n) /" seq is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
seq " is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
(r (#) n) (#) (seq ") is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
n /" seq is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
n (#) (seq ") is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
r (#) (n /" seq) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
seq " is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
n (#) (seq ") is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
r (#) (n (#) (seq ")) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
r is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
seq is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
seq (#) r is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
n is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
seq /" n is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
n " is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
seq (#) (n ") is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
n (#) r is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(seq (#) r) /" (n (#) r) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(n (#) r) " is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
(seq (#) r) (#) ((n (#) r) ") is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
seq1 is V21() epsilon-transitive epsilon-connected ordinal natural V31() real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
(r,seq1) is V21() V31() real Element of REAL
((seq /" n),seq1) is V21() V31() real Element of REAL
(seq,seq1) is V21() V31() real Element of REAL
(seq,seq1) * 1 is V21() V31() real Element of REAL
n " is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
((n "),seq1) is V21() V31() real Element of REAL
((seq,seq1) * 1) * ((n "),seq1) is V21() V31() real Element of REAL
(r,seq1) " is V21() V31() real Element of REAL
(r,seq1) * ((r,seq1) ") is V21() V31() real Element of REAL
(seq,seq1) * ((r,seq1) * ((r,seq1) ")) is V21() V31() real Element of REAL
((seq,seq1) * ((r,seq1) * ((r,seq1) "))) * ((n "),seq1) is V21() V31() real Element of REAL
(seq,seq1) * (r,seq1) is V21() V31() real Element of REAL
((r,seq1) ") * ((n "),seq1) is V21() V31() real Element of REAL
((seq,seq1) * (r,seq1)) * (((r,seq1) ") * ((n "),seq1)) is V21() V31() real Element of REAL
((seq (#) r),seq1) is V21() V31() real Element of REAL
((seq (#) r),seq1) * (((r,seq1) ") * ((n "),seq1)) is V21() V31() real Element of REAL
r " is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
((r "),seq1) is V21() V31() real Element of REAL
((r "),seq1) * ((n "),seq1) is V21() V31() real Element of REAL
((seq (#) r),seq1) * (((r "),seq1) * ((n "),seq1)) is V21() V31() real Element of REAL
(n ") (#) (r ") is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(((n ") (#) (r ")),seq1) is V21() V31() real Element of REAL
((seq (#) r),seq1) * (((n ") (#) (r ")),seq1) is V21() V31() real Element of REAL
(n (#) r) " is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(((n (#) r) "),seq1) is V21() V31() real Element of REAL
((seq (#) r),seq1) * (((n (#) r) "),seq1) is V21() V31() real Element of REAL
(((seq (#) r) /" (n (#) r)),seq1) is V21() V31() real Element of REAL
r is V21() V31() real set
seq is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
r (#) seq is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
n is V21() epsilon-transitive epsilon-connected ordinal natural V31() real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
((r (#) seq),n) is V21() V31() real Element of REAL
(seq,n) is V21() V31() real Element of REAL
r * (seq,n) is V21() V31() real Element of REAL
r is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
- r is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
- 1 is V21() V31() real set
(- 1) (#) r is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
r is V21() V31() real set
r " is V21() V31() real set
seq is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
r (#) seq is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(r (#) seq) " is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
seq " is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(r ") (#) (seq ") is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
n is V21() epsilon-transitive epsilon-connected ordinal natural V31() real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
(((r (#) seq) "),n) is V21() V31() real Element of REAL
((r (#) seq),n) is V21() V31() real Element of REAL
((r (#) seq),n) " is V21() V31() real Element of REAL
(seq,n) is V21() V31() real Element of REAL
r * (seq,n) is V21() V31() real Element of REAL
(r * (seq,n)) " is V21() V31() real Element of REAL
(seq,n) " is V21() V31() real Element of REAL
(r ") * ((seq,n) ") is V21() V31() real Element of REAL
((seq "),n) is V21() V31() real Element of REAL
(r ") * ((seq "),n) is V21() V31() real Element of REAL
(((r ") (#) (seq ")),n) is V21() V31() real Element of REAL
(- 1) " is V21() V31() real Element of REAL
r is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
- r is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
- 1 is V21() V31() real set
(- 1) (#) r is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
(- r) " is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
r " is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(- 1) (#) (r ") is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
r is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
- r is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
- 1 is V21() V31() real set
(- 1) (#) r is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
seq is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
r /" seq is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
seq " is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
r (#) (seq ") is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
- (r /" seq) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(- 1) (#) (r /" seq) is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
(- r) /" seq is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(- r) (#) (seq ") is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
- seq is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(- 1) (#) seq is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
r /" (- seq) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(- seq) " is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
r (#) ((- seq) ") is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
seq " is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
r (#) (seq ") is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(- 1) (#) (r (#) (seq ")) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(- 1) (#) (seq ") is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
r (#) ((- 1) (#) (seq ")) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
r is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
seq is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
r /" seq is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
seq " is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
r (#) (seq ") is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
n is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
n /" seq is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
n (#) (seq ") is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
(r /" seq) + (n /" seq) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
r + n is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(r + n) /" seq is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(r + n) (#) (seq ") is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
(r /" seq) - (n /" seq) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
- (n /" seq) is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
- 1 is V21() V31() real set
(- 1) (#) (n /" seq) is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
(r /" seq) + (- (n /" seq)) is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
r - n is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
- n is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
(- 1) (#) n is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
r + (- n) is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
(r - n) /" seq is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(r - n) (#) (seq ") is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
seq " is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(r + n) (#) (seq ") is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(r - n) (#) (seq ") is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
r is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
seq is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
r (#) seq is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
n is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
n /" r is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
r " is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
n (#) (r ") is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
n (#) seq is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
seq1 is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
seq1 /" seq is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
seq " is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
seq1 (#) (seq ") is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
(n /" r) + (seq1 /" seq) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
seq1 (#) r is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(n (#) seq) + (seq1 (#) r) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
((n (#) seq) + (seq1 (#) r)) /" (r (#) seq) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(r (#) seq) " is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
((n (#) seq) + (seq1 (#) r)) (#) ((r (#) seq) ") is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
(n /" r) - (seq1 /" seq) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
- (seq1 /" seq) is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
- 1 is V21() V31() real set
(- 1) (#) (seq1 /" seq) is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
(n /" r) + (- (seq1 /" seq)) is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
(n (#) seq) - (seq1 (#) r) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
- (seq1 (#) r) is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
(- 1) (#) (seq1 (#) r) is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
(n (#) seq) + (- (seq1 (#) r)) is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
((n (#) seq) - (seq1 (#) r)) /" (r (#) seq) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
((n (#) seq) - (seq1 (#) r)) (#) ((r (#) seq) ") is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
(n (#) seq) /" (r (#) seq) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(n (#) seq) (#) ((r (#) seq) ") is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
((n (#) seq) /" (r (#) seq)) + (seq1 /" seq) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(seq1 (#) r) /" (r (#) seq) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(seq1 (#) r) (#) ((r (#) seq) ") is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
((n (#) seq) /" (r (#) seq)) + ((seq1 (#) r) /" (r (#) seq)) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(r (#) seq) " is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
((n (#) seq) + (seq1 (#) r)) (#) ((r (#) seq) ") is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
((n (#) seq) /" (r (#) seq)) - (seq1 /" seq) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
((n (#) seq) /" (r (#) seq)) + (- (seq1 /" seq)) is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
((n (#) seq) /" (r (#) seq)) - ((seq1 (#) r) /" (r (#) seq)) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
- ((seq1 (#) r) /" (r (#) seq)) is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
(- 1) (#) ((seq1 (#) r) /" (r (#) seq)) is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
((n (#) seq) /" (r (#) seq)) + (- ((seq1 (#) r) /" (r (#) seq))) is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
((n (#) seq) - (seq1 (#) r)) (#) ((r (#) seq) ") is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
r is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
seq is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
r /" seq is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
seq " is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
r (#) (seq ") is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
n is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
seq (#) n is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
seq1 is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
n /" seq1 is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
seq1 " is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
n (#) (seq1 ") is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
(r /" seq) /" (n /" seq1) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(n /" seq1) " is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
(r /" seq) (#) ((n /" seq1) ") is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
r (#) seq1 is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(r (#) seq1) /" (seq (#) n) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(seq (#) n) " is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
(r (#) seq1) (#) ((seq (#) n) ") is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
n " is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
seq1 " is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(seq1 ") " is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(n ") (#) ((seq1 ") ") is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(r /" seq) (#) ((n ") (#) ((seq1 ") ")) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
seq " is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
r (#) (seq ") is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(r (#) (seq ")) (#) seq1 is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
((r (#) (seq ")) (#) seq1) (#) (n ") is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
seq1 (#) (seq ") is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
r (#) (seq1 (#) (seq ")) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(r (#) (seq1 (#) (seq "))) (#) (n ") is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(seq1 (#) (seq ")) (#) (n ") is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
r (#) ((seq1 (#) (seq ")) (#) (n ")) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(seq ") (#) (n ") is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
seq1 (#) ((seq ") (#) (n ")) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
r (#) (seq1 (#) ((seq ") (#) (n "))) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(r (#) seq1) (#) ((seq ") (#) (n ")) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
r is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
abs r is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
seq is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
r (#) seq is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
abs (r (#) seq) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
abs seq is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(abs r) (#) (abs seq) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
n is V21() epsilon-transitive epsilon-connected ordinal natural V31() real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
((abs (r (#) seq)),n) is V21() V31() real Element of REAL
((r (#) seq),n) is V21() V31() real Element of REAL
abs ((r (#) seq),n) is V21() V31() real Element of REAL
(r,n) is V21() V31() real Element of REAL
(seq,n) is V21() V31() real Element of REAL
(r,n) * (seq,n) is V21() V31() real Element of REAL
abs ((r,n) * (seq,n)) is V21() V31() real Element of REAL
abs (r,n) is V21() V31() real Element of REAL
abs (seq,n) is V21() V31() real Element of REAL
(abs (r,n)) * (abs (seq,n)) is V21() V31() real Element of REAL
((abs r),n) is V21() V31() real Element of REAL
((abs r),n) * (abs (seq,n)) is V21() V31() real Element of REAL
((abs seq),n) is V21() V31() real Element of REAL
((abs r),n) * ((abs seq),n) is V21() V31() real Element of REAL
(((abs r) (#) (abs seq)),n) is V21() V31() real Element of REAL
r is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
abs r is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
seq is V21() epsilon-transitive epsilon-connected ordinal natural V31() real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
(r,seq) is V21() V31() real Element of REAL
abs (r,seq) is V21() V31() real Element of REAL
((abs r),seq) is V21() V31() real Element of REAL
r is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
abs r is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(abs r) " is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
r " is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
abs (r ") is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
seq is V21() epsilon-transitive epsilon-connected ordinal natural V31() real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
((abs (r ")),seq) is V21() V31() real Element of REAL
((r "),seq) is V21() V31() real Element of REAL
abs ((r "),seq) is V21() V31() real Element of REAL
(r,seq) is V21() V31() real Element of REAL
(r,seq) " is V21() V31() real Element of REAL
abs ((r,seq) ") is V21() V31() real Element of REAL
1 / (r,seq) is V21() V31() real Element of COMPLEX
abs (1 / (r,seq)) is V21() V31() real Element of REAL
abs (r,seq) is V21() V31() real Element of REAL
1 / (abs (r,seq)) is V21() V31() real Element of COMPLEX
(abs (r,seq)) " is V21() V31() real Element of REAL
((abs r),seq) is V21() V31() real Element of REAL
((abs r),seq) " is V21() V31() real Element of REAL
(((abs r) "),seq) is V21() V31() real Element of REAL
r is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
abs r is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
seq is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
r /" seq is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
seq " is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
r (#) (seq ") is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
abs (r /" seq) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
abs seq is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(abs r) /" (abs seq) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(abs seq) " is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
(abs r) (#) ((abs seq) ") is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
seq " is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
abs (seq ") is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(abs r) (#) (abs (seq ")) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
r is V21() V31() real set
abs r is V21() V31() real Element of REAL
seq is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
r (#) seq is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
abs (r (#) seq) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
abs seq is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(abs r) (#) (abs seq) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
n is V21() epsilon-transitive epsilon-connected ordinal natural V31() real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
((abs (r (#) seq)),n) is V21() V31() real Element of REAL
((r (#) seq),n) is V21() V31() real Element of REAL
abs ((r (#) seq),n) is V21() V31() real Element of REAL
(seq,n) is V21() V31() real Element of REAL
r * (seq,n) is V21() V31() real Element of REAL
abs (r * (seq,n)) is V21() V31() real Element of REAL
abs (seq,n) is V21() V31() real Element of REAL
(abs r) * (abs (seq,n)) is V21() V31() real Element of REAL
((abs seq),n) is V21() V31() real Element of REAL
(abs r) * ((abs seq),n) is V21() V31() real Element of REAL
(((abs r) (#) (abs seq)),n) is V21() V31() real Element of REAL