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

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

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

n is V21() epsilon-transitive epsilon-connected ordinal natural V31() real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT

F

F

F

K20(F

K19(K20(F

the Element of F

seq is set

n is set

K19(F

seq1 is Element of F

n is Element of F

d is set

c

seq1 is Relation-like F

n is Element of K19(F

seq1 | n is Relation-like F

n is Relation-like F

dom n is Element of K19(F

dom seq1 is Element of K19(F

d is Element of F

c

(dom seq1) /\ n is Element of K19(F

d is Element of F

n . d is set

seq1 . d is Element of F

c

F

F

K20(F

K19(K20(F

r is Relation-like F

dom r is Element of K19(F

K19(F

seq is Element of F

F

n is Element of F

F

n is Element of F

seq is Element of F

r . seq is set

F

F

F

K20(F

K19(K20(F

F

r is Relation-like F

dom r is Element of K19(F

K19(F

seq is Relation-like F

dom seq is Element of K19(F

n is Element of F

r . n is set

F

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