:: SERIES_1 semantic presentation

REAL is non empty V50() complex-membered ext-real-membered real-membered add-closed set

NAT is non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered add-closed Element of K19(REAL)

K19(REAL) is set

COMPLEX is non empty V50() complex-membered add-closed set

omega is non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered add-closed set

K19(omega) is set

K19(NAT) is set

K20(NAT,REAL) is complex-valued ext-real-valued real-valued set

K19(K20(NAT,REAL)) is set

RAT is non empty V50() complex-membered ext-real-membered real-membered rational-membered add-closed set

INT is non empty V50() complex-membered ext-real-membered real-membered rational-membered integer-membered add-closed set

K20(COMPLEX,COMPLEX) is complex-valued set

K19(K20(COMPLEX,COMPLEX)) is set

K20(COMPLEX,REAL) is complex-valued ext-real-valued real-valued set

K19(K20(COMPLEX,REAL)) is set

K20(K20(COMPLEX,COMPLEX),COMPLEX) is complex-valued set

K19(K20(K20(COMPLEX,COMPLEX),COMPLEX)) is set

K20(REAL,REAL) is complex-valued ext-real-valued real-valued set

K19(K20(REAL,REAL)) is set

K20(K20(REAL,REAL),REAL) is complex-valued ext-real-valued real-valued set

K19(K20(K20(REAL,REAL),REAL)) is set

K20(RAT,RAT) is RAT -valued complex-valued ext-real-valued real-valued set

K19(K20(RAT,RAT)) is set

K20(K20(RAT,RAT),RAT) is RAT -valued complex-valued ext-real-valued real-valued set

K19(K20(K20(RAT,RAT),RAT)) is set

K20(INT,INT) is RAT -valued INT -valued complex-valued ext-real-valued real-valued set

K19(K20(INT,INT)) is set

K20(K20(INT,INT),INT) is RAT -valued INT -valued complex-valued ext-real-valued real-valued set

K19(K20(K20(INT,INT),INT)) is set

K20(NAT,NAT) is RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued set

K20(K20(NAT,NAT),NAT) is RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued set

K19(K20(K20(NAT,NAT),NAT)) is set

1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT

{} is empty ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V33() real integer complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered add-closed set

0 is empty ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered add-closed Element of NAT

- 1 is non empty ext-real non positive negative V33() real integer Element of REAL

|.0.| is ext-real V33() real V61() Element of REAL

1r is V33() Element of COMPLEX

|.1r.| is ext-real V33() real Element of REAL

s is ext-real V33() real set

n is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

lim n is ext-real V33() real Element of REAL

1 / s is ext-real V33() real Element of REAL

s " is ext-real V33() real set

1 * (s ") is ext-real V33() real set

(1 / s) - 1 is ext-real V33() real Element of REAL

- 1 is non empty ext-real non positive negative V33() real integer set

(1 / s) + (- 1) is ext-real V33() real set

1 / 1 is non empty ext-real positive non negative V33() real Element of REAL

1 " is non empty ext-real positive non negative V33() real set

1 * (1 ") is non empty ext-real positive non negative V33() real set

n is ext-real V33() real set

n * ((1 / s) - 1) is ext-real V33() real Element of REAL

1 / (n * ((1 / s) - 1)) is ext-real V33() real Element of REAL

(n * ((1 / s) - 1)) " is ext-real V33() real set

1 * ((n * ((1 / s) - 1)) ") is ext-real V33() real set

[\(1 / (n * ((1 / s) - 1)))/] is ext-real V33() real integer set

[\(1 / (n * ((1 / s) - 1)))/] + 1 is ext-real V33() real integer Element of REAL

k is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT

1 / n is ext-real V33() real Element of REAL

n " is ext-real V33() real set

1 * (n ") is ext-real V33() real set

(1 / n) / ((1 / s) - 1) is ext-real V33() real Element of REAL

((1 / s) - 1) " is ext-real V33() real set

(1 / n) * (((1 / s) - 1) ") is ext-real V33() real set

(1 / (n * ((1 / s) - 1))) - 1 is ext-real V33() real Element of REAL

(1 / (n * ((1 / s) - 1))) + (- 1) is ext-real V33() real set

s2 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT

s2 + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT

(s2 + 1) * ((1 / s) - 1) is ext-real V33() real Element of REAL

1 + ((s2 + 1) * ((1 / s) - 1)) is ext-real V33() real Element of REAL

0 + ((s2 + 1) * ((1 / s) - 1)) is ext-real V33() real Element of REAL

1 + ((1 / s) - 1) is ext-real V33() real Element of REAL

(1 + ((1 / s) - 1)) to_power (s2 + 1) is ext-real V33() real Element of REAL

(1 + ((1 / s) - 1)) |^ (s2 + 1) is ext-real V33() real set

1 to_power (s2 + 1) is ext-real V33() real Element of REAL

1 |^ (s2 + 1) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer set

s to_power (s2 + 1) is ext-real V33() real set

s |^ (s2 + 1) is ext-real V33() real set

(1 to_power (s2 + 1)) / (s to_power (s2 + 1)) is ext-real V33() real Element of REAL

(s to_power (s2 + 1)) " is ext-real V33() real set

(1 to_power (s2 + 1)) * ((s to_power (s2 + 1)) ") is ext-real V33() real set

1 / (s to_power (s2 + 1)) is ext-real V33() real Element of REAL

1 * ((s to_power (s2 + 1)) ") is ext-real V33() real set

abs (s to_power (s2 + 1)) is ext-real V33() real Element of REAL

n . s2 is ext-real V33() real Element of REAL

(n . s2) - 0 is ext-real V33() real Element of REAL

- 0 is empty ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V33() real integer complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered add-closed set

(n . s2) + (- 0) is ext-real V33() real set

abs ((n . s2) - 0) is ext-real V33() real Element of REAL

s2 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT

n . s2 is ext-real V33() real Element of REAL

(n . s2) - 0 is ext-real V33() real Element of REAL

(n . s2) + (- 0) is ext-real V33() real set

abs ((n . s2) - 0) is ext-real V33() real Element of REAL

s is ext-real V33() real set

abs s is ext-real V33() real Element of REAL

n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer set

(abs s) to_power n is ext-real V33() real set

(abs s) |^ n is ext-real V33() real set

s to_power n is ext-real V33() real set

s |^ n is ext-real V33() real set

abs (s to_power n) is ext-real V33() real Element of REAL

m is ext-real V33() real integer set

- s is ext-real V33() real set

(- s) to_power m is ext-real V33() real set

s to_power m is ext-real V33() real set

m is ext-real V33() real integer set

- s is ext-real V33() real set

(- s) to_power m is ext-real V33() real set

s to_power m is ext-real V33() real set

- (s to_power m) is ext-real V33() real set

- (s to_power n) is ext-real V33() real set

abs (- (s to_power n)) is ext-real V33() real Element of REAL

m is ext-real V33() real integer set

s is ext-real V33() real set

abs s is ext-real V33() real Element of REAL

n is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

lim n is ext-real V33() real Element of REAL

m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer set

m + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT

s to_power (m + 1) is ext-real V33() real set

s |^ (m + 1) is ext-real V33() real set

n . m is ext-real V33() real Element of REAL

n . 0 is ext-real V33() real Element of REAL

m is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT

m . n is ext-real V33() real Element of REAL

n + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT

(abs s) to_power (n + 1) is ext-real V33() real Element of REAL

(abs s) |^ (n + 1) is ext-real V33() real set

s to_power (n + 1) is ext-real V33() real set

s |^ (n + 1) is ext-real V33() real set

abs (s to_power (n + 1)) is ext-real V33() real Element of REAL

n . n is ext-real V33() real Element of REAL

abs (n . n) is ext-real V33() real Element of REAL

lim m is ext-real V33() real Element of REAL

abs n is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

lim (abs n) is ext-real V33() real Element of REAL

s is non empty complex-membered add-closed set

K20(NAT,s) is complex-valued set

K19(K20(NAT,s)) is set

n is Relation-like NAT -defined s -valued Function-like non empty V14( NAT ) V18( NAT ,s) complex-valued Element of K19(K20(NAT,s))

m is Relation-like NAT -defined s -valued Function-like non empty V14( NAT ) V18( NAT ,s) complex-valued Element of K19(K20(NAT,s))

n + m is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set

n + m is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))

K20(NAT,COMPLEX) is complex-valued set

K19(K20(NAT,COMPLEX)) is set

dom (n + m) is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K19(NAT)

dom n is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K19(NAT)

dom m is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K19(NAT)

(dom n) /\ (dom m) is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K19(NAT)

NAT /\ (dom m) is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K19(NAT)

NAT /\ NAT is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K19(REAL)

n is set

n . n is V33() set

m . n is V33() set

(n + m) . n is V33() set

(n . n) + (m . n) is V33() set

s is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set

s . 0 is V33() set

dom s is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K19(NAT)

rng s is complex-membered set

K20(NAT,COMPLEX) is complex-valued set

K19(K20(NAT,COMPLEX)) is set

m is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))

k is V33() Element of COMPLEX

n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT

n + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT

m . (n + 1) is V33() Element of COMPLEX

k + (m . (n + 1)) is V33() Element of COMPLEX

m . 0 is V33() Element of COMPLEX

n is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))

n . 0 is V33() Element of COMPLEX

n is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set

n . 0 is V33() set

m is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set

m . 0 is V33() set

n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT

n . n is V33() set

m . n is V33() set

n + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT

n . (n + 1) is V33() set

m . (n + 1) is V33() set

s . (n + 1) is V33() set

(m . n) + (s . (n + 1)) is V33() set

s is Relation-like NAT -defined Function-like V14( NAT ) complex-valued ext-real-valued real-valued set

(s) is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set

m is set

dom (s) is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set

(s) . m is V33() set

dom (s) is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K19(NAT)

(s) . 0 is V33() set

s . 0 is ext-real V33() real Element of REAL

k is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer set

(s) . k is V33() set

k + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT

(s) . (k + 1) is V33() set

s2 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT

s2 + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT

(s) . (s2 + 1) is V33() set

(s) . s2 is V33() set

s . (s2 + 1) is ext-real V33() real Element of REAL

((s) . s2) + (s . (s2 + 1)) is V33() set

n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT

(s) . n is V33() set

s is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

(s) is Relation-like NAT -defined Function-like V14( NAT ) complex-valued ext-real-valued real-valued set

dom (s) is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K19(NAT)

rng (s) is complex-membered ext-real-membered real-membered set

s is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

(s) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

lim (s) is ext-real V33() real Element of REAL

s is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

lim s is ext-real V33() real Element of REAL

(s) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT

n + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT

(s) . (n + 1) is ext-real V33() real Element of REAL

(s) . n is ext-real V33() real Element of REAL

s . (n + 1) is ext-real V33() real Element of REAL

((s) . n) + (s . (n + 1)) is ext-real V33() real Element of REAL

s ^\ 1 is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued subsequence of s

(s ^\ 1) . n is ext-real V33() real Element of REAL

((s) . n) + ((s ^\ 1) . n) is ext-real V33() real Element of REAL

(s) ^\ 1 is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued subsequence of (s)

((s) ^\ 1) . n is ext-real V33() real Element of REAL

(REAL,(s),(s ^\ 1)) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

(s) - (s) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

- (s) is Relation-like NAT -defined Function-like V14( NAT ) complex-valued ext-real-valued real-valued set

- 1 is non empty ext-real non positive negative V33() real integer set

(- 1) (#) (s) is Relation-like NAT -defined Function-like V14( NAT ) complex-valued ext-real-valued real-valued set

(s) + (- (s)) is Relation-like NAT -defined Function-like V14( NAT ) complex-valued ext-real-valued real-valued set

(REAL,(s ^\ 1),((s) - (s))) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT

(REAL,(s ^\ 1),((s) - (s))) . n is ext-real V33() real Element of REAL

(s ^\ 1) . n is ext-real V33() real Element of REAL

- (s) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

(REAL,(s),(- (s))) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

(REAL,(s),(- (s))) . n is ext-real V33() real Element of REAL

((s ^\ 1) . n) + ((REAL,(s),(- (s))) . n) is ext-real V33() real Element of REAL

(s) . n is ext-real V33() real Element of REAL

(- (s)) . n is ext-real V33() real Element of REAL

((s) . n) + ((- (s)) . n) is ext-real V33() real Element of REAL

((s ^\ 1) . n) + (((s) . n) + ((- (s)) . n)) is ext-real V33() real Element of REAL

- ((s) . n) is ext-real V33() real Element of REAL

((s) . n) + (- ((s) . n)) is ext-real V33() real Element of REAL

((s ^\ 1) . n) + (((s) . n) + (- ((s) . n))) is ext-real V33() real Element of REAL

((s) ^\ 1) - (s) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

((s) ^\ 1) + (- (s)) is Relation-like NAT -defined Function-like V14( NAT ) complex-valued ext-real-valued real-valued set

lim ((s) ^\ 1) is ext-real V33() real Element of REAL

lim (s) is ext-real V33() real Element of REAL

lim (((s) ^\ 1) - (s)) is ext-real V33() real Element of REAL

(lim (s)) - (lim (s)) is ext-real V33() real Element of REAL

- (lim (s)) is ext-real V33() real set

(lim (s)) + (- (lim (s))) is ext-real V33() real set

s is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set

n is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set

m is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set

n + m is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set

n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT

s . n is V33() set

n . n is V33() set

m . n is V33() set

(n . n) + (m . n) is V33() set

dom s is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K19(NAT)

dom s is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K19(NAT)

n is set

s . n is V33() set

n . n is V33() set

m . n is V33() set

(n . n) + (m . n) is V33() set

NAT /\ NAT is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K19(REAL)

dom m is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K19(NAT)

NAT /\ (dom m) is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K19(NAT)

dom n is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K19(NAT)

(dom n) /\ (dom m) is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K19(NAT)

s is non empty complex-membered add-closed set

K20(NAT,s) is complex-valued set

K19(K20(NAT,s)) is set

n is Relation-like NAT -defined s -valued Function-like non empty V14( NAT ) V18( NAT ,s) complex-valued Element of K19(K20(NAT,s))

(n) is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set

m is Relation-like NAT -defined s -valued Function-like non empty V14( NAT ) V18( NAT ,s) complex-valued Element of K19(K20(NAT,s))

(m) is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set

(n) + (m) is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set

(s,n,m) is Relation-like NAT -defined s -valued Function-like non empty V14( NAT ) V18( NAT ,s) complex-valued Element of K19(K20(NAT,s))

((s,n,m)) is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set

n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT

n + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT

((n) + (m)) . (n + 1) is V33() set

(n) . (n + 1) is V33() set

(m) . (n + 1) is V33() set

((n) . (n + 1)) + ((m) . (n + 1)) is V33() set

(n) . n is V33() set

n . (n + 1) is V33() Element of s

((n) . n) + (n . (n + 1)) is V33() set

(((n) . n) + (n . (n + 1))) + ((m) . (n + 1)) is V33() set

m . (n + 1) is V33() Element of s

(m) . n is V33() set

(m . (n + 1)) + ((m) . n) is V33() set

(((n) . n) + (n . (n + 1))) + ((m . (n + 1)) + ((m) . n)) is V33() set

(n . (n + 1)) + (m . (n + 1)) is V33() set

((n) . n) + ((n . (n + 1)) + (m . (n + 1))) is V33() set

(((n) . n) + ((n . (n + 1)) + (m . (n + 1)))) + ((m) . n) is V33() set

(s,n,m) . (n + 1) is V33() Element of s

((n) . n) + ((s,n,m) . (n + 1)) is V33() set

(((n) . n) + ((s,n,m) . (n + 1))) + ((m) . n) is V33() set

((n) . n) + ((m) . n) is V33() set

(((n) . n) + ((m) . n)) + ((s,n,m) . (n + 1)) is V33() set

((n) + (m)) . n is V33() set

(((n) + (m)) . n) + ((s,n,m) . (n + 1)) is V33() set

((n) + (m)) . 0 is V33() set

(n) . 0 is V33() set

(m) . 0 is V33() set

((n) . 0) + ((m) . 0) is V33() set

n . 0 is V33() Element of s

(n . 0) + ((m) . 0) is V33() set

m . 0 is V33() Element of s

(n . 0) + (m . 0) is V33() set

(s,n,m) . 0 is V33() Element of s

s is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

(s) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) 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 V14( NAT ) 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 V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

(s) - (n) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

- (n) is Relation-like NAT -defined Function-like V14( NAT ) complex-valued ext-real-valued real-valued set

- 1 is non empty ext-real non positive negative V33() real integer set

(- 1) (#) (n) is Relation-like NAT -defined Function-like V14( NAT ) complex-valued ext-real-valued real-valued set

(s) + (- (n)) is Relation-like NAT -defined Function-like V14( NAT ) complex-valued ext-real-valued real-valued set

s - n is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

- n is Relation-like NAT -defined Function-like V14( NAT ) complex-valued ext-real-valued real-valued set

(- 1) (#) n is Relation-like NAT -defined Function-like V14( NAT ) complex-valued ext-real-valued real-valued set

s + (- n) is Relation-like NAT -defined Function-like V14( NAT ) complex-valued ext-real-valued real-valued set

((s - n)) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT

m + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT

((s) - (n)) . (m + 1) is ext-real V33() real Element of REAL

(s) . (m + 1) is ext-real V33() real Element of REAL

(n) . (m + 1) is ext-real V33() real Element of REAL

((s) . (m + 1)) - ((n) . (m + 1)) is ext-real V33() real Element of REAL

- ((n) . (m + 1)) is ext-real V33() real set

((s) . (m + 1)) + (- ((n) . (m + 1))) is ext-real V33() real set

(s) . m is ext-real V33() real Element of REAL

s . (m + 1) is ext-real V33() real Element of REAL

((s) . m) + (s . (m + 1)) is ext-real V33() real Element of REAL

(((s) . m) + (s . (m + 1))) - ((n) . (m + 1)) is ext-real V33() real Element of REAL

(((s) . m) + (s . (m + 1))) + (- ((n) . (m + 1))) is ext-real V33() real set

n . (m + 1) is ext-real V33() real Element of REAL

(n) . m is ext-real V33() real Element of REAL

(n . (m + 1)) + ((n) . m) is ext-real V33() real Element of REAL

(((s) . m) + (s . (m + 1))) - ((n . (m + 1)) + ((n) . m)) is ext-real V33() real Element of REAL

- ((n . (m + 1)) + ((n) . m)) is ext-real V33() real set

(((s) . m) + (s . (m + 1))) + (- ((n . (m + 1)) + ((n) . m))) is ext-real V33() real set

(s . (m + 1)) - (n . (m + 1)) is ext-real V33() real Element of REAL

- (n . (m + 1)) is ext-real V33() real set

(s . (m + 1)) + (- (n . (m + 1))) is ext-real V33() real set

((s) . m) + ((s . (m + 1)) - (n . (m + 1))) is ext-real V33() real Element of REAL

(((s) . m) + ((s . (m + 1)) - (n . (m + 1)))) - ((n) . m) is ext-real V33() real Element of REAL

- ((n) . m) is ext-real V33() real set

(((s) . m) + ((s . (m + 1)) - (n . (m + 1)))) + (- ((n) . m)) is ext-real V33() real set

(s - n) . (m + 1) is ext-real V33() real Element of REAL

((s - n) . (m + 1)) + ((s) . m) is ext-real V33() real Element of REAL

(((s - n) . (m + 1)) + ((s) . m)) - ((n) . m) is ext-real V33() real Element of REAL

(((s - n) . (m + 1)) + ((s) . m)) + (- ((n) . m)) is ext-real V33() real set

((s) . m) - ((n) . m) is ext-real V33() real Element of REAL

((s) . m) + (- ((n) . m)) is ext-real V33() real set

((s - n) . (m + 1)) + (((s) . m) - ((n) . m)) is ext-real V33() real Element of REAL

((s) - (n)) . m is ext-real V33() real Element of REAL

(((s) - (n)) . m) + ((s - n) . (m + 1)) is ext-real V33() real Element of REAL

((s) - (n)) . 0 is ext-real V33() real Element of REAL

(s) . 0 is ext-real V33() real Element of REAL

(n) . 0 is ext-real V33() real Element of REAL

((s) . 0) - ((n) . 0) is ext-real V33() real Element of REAL

- ((n) . 0) is ext-real V33() real set

((s) . 0) + (- ((n) . 0)) is ext-real V33() real set

s . 0 is ext-real V33() real Element of REAL

(s . 0) - ((n) . 0) is ext-real V33() real Element of REAL

(s . 0) + (- ((n) . 0)) is ext-real V33() real set

n . 0 is ext-real V33() real Element of REAL

(s . 0) - (n . 0) is ext-real V33() real Element of REAL

- (n . 0) is ext-real V33() real set

(s . 0) + (- (n . 0)) is ext-real V33() real set

(s - n) . 0 is ext-real V33() real Element of REAL

s is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

(s) is ext-real V33() real Element of REAL

(s) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

lim (s) is ext-real V33() real Element of REAL

n is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

(REAL,s,n) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

((REAL,s,n)) is ext-real V33() real Element of REAL

((REAL,s,n)) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

lim ((REAL,s,n)) is ext-real V33() real Element of REAL

(n) is ext-real V33() real Element of REAL

(n) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

lim (n) is ext-real V33() real Element of REAL

(s) + (n) is ext-real V33() real Element of REAL

(REAL,(s),(n)) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

lim (REAL,(s),(n)) is ext-real V33() real Element of REAL

s is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

(s) is ext-real V33() real Element of REAL

(s) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

lim (s) is ext-real V33() real Element of REAL

n is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

s - n is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

- n is Relation-like NAT -defined Function-like V14( NAT ) complex-valued ext-real-valued real-valued set

- 1 is non empty ext-real non positive negative V33() real integer set

(- 1) (#) n is Relation-like NAT -defined Function-like V14( NAT ) complex-valued ext-real-valued real-valued set

s + (- n) is Relation-like NAT -defined Function-like V14( NAT ) complex-valued ext-real-valued real-valued set

((s - n)) is ext-real V33() real Element of REAL

((s - n)) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

lim ((s - n)) is ext-real V33() real Element of REAL

(n) is ext-real V33() real Element of REAL

(n) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

lim (n) is ext-real V33() real Element of REAL

(s) - (n) is ext-real V33() real Element of REAL

- (n) is ext-real V33() real set

(s) + (- (n)) is ext-real V33() real set

(s) - (n) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

- (n) is Relation-like NAT -defined Function-like V14( NAT ) complex-valued ext-real-valued real-valued set

(- 1) (#) (n) is Relation-like NAT -defined Function-like V14( NAT ) complex-valued ext-real-valued real-valued set

(s) + (- (n)) is Relation-like NAT -defined Function-like V14( NAT ) complex-valued ext-real-valued real-valued set

lim ((s) - (n)) is ext-real V33() real Element of REAL

s is ext-real V33() real set

n is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

s (#) n is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

((s (#) n)) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) 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 V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

s (#) (n) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT

m + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT

(s (#) (n)) . (m + 1) is ext-real V33() real Element of REAL

(n) . (m + 1) is ext-real V33() real Element of REAL

s * ((n) . (m + 1)) is ext-real V33() real Element of REAL

(n) . m is ext-real V33() real Element of REAL

n . (m + 1) is ext-real V33() real Element of REAL

((n) . m) + (n . (m + 1)) is ext-real V33() real Element of REAL

s * (((n) . m) + (n . (m + 1))) is ext-real V33() real Element of REAL

s * ((n) . m) is ext-real V33() real Element of REAL

s * (n . (m + 1)) is ext-real V33() real Element of REAL

(s * ((n) . m)) + (s * (n . (m + 1))) is ext-real V33() real Element of REAL

(s (#) (n)) . m is ext-real V33() real Element of REAL

((s (#) (n)) . m) + (s * (n . (m + 1))) is ext-real V33() real Element of REAL

(s (#) n) . (m + 1) is ext-real V33() real Element of REAL

((s (#) (n)) . m) + ((s (#) n) . (m + 1)) is ext-real V33() real Element of REAL

(s (#) (n)) . 0 is ext-real V33() real Element of REAL

(n) . 0 is ext-real V33() real Element of REAL

s * ((n) . 0) is ext-real V33() real Element of REAL

n . 0 is ext-real V33() real Element of REAL

s * (n . 0) is ext-real V33() real Element of REAL

(s (#) n) . 0 is ext-real V33() real Element of REAL

s is ext-real V33() real set

n is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

s (#) n is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

((s (#) n)) is ext-real V33() real Element of REAL

((s (#) n)) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

lim ((s (#) n)) is ext-real V33() real Element of REAL

(n) is ext-real V33() real Element of REAL

(n) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

lim (n) is ext-real V33() real Element of REAL

s * (n) is ext-real V33() real Element of REAL

s (#) (n) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

lim (s (#) (n)) is ext-real V33() real Element of REAL

s is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

s . 0 is ext-real V33() real Element of REAL

s ^\ 1 is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued subsequence of s

((s ^\ 1)) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

(s) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

(s) ^\ 1 is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued subsequence of (s)

n is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

((s) ^\ 1) - n is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

- n is Relation-like NAT -defined Function-like V14( NAT ) complex-valued ext-real-valued real-valued set

- 1 is non empty ext-real non positive negative V33() real integer set

(- 1) (#) n is Relation-like NAT -defined Function-like V14( NAT ) complex-valued ext-real-valued real-valued set

((s) ^\ 1) + (- n) is Relation-like NAT -defined Function-like V14( NAT ) complex-valued ext-real-valued real-valued set

m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT

m + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT

(((s) ^\ 1) - n) . (m + 1) is ext-real V33() real Element of REAL

((s) ^\ 1) . (m + 1) is ext-real V33() real Element of REAL

n . (m + 1) is ext-real V33() real Element of REAL

(((s) ^\ 1) . (m + 1)) - (n . (m + 1)) is ext-real V33() real Element of REAL

- (n . (m + 1)) is ext-real V33() real set

(((s) ^\ 1) . (m + 1)) + (- (n . (m + 1))) is ext-real V33() real set

(((s) ^\ 1) . (m + 1)) - (s . 0) is ext-real V33() real Element of REAL

- (s . 0) is ext-real V33() real set

(((s) ^\ 1) . (m + 1)) + (- (s . 0)) is ext-real V33() real set

(m + 1) + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT

(s) . ((m + 1) + 1) is ext-real V33() real Element of REAL

((s) . ((m + 1) + 1)) - (s . 0) is ext-real V33() real Element of REAL

((s) . ((m + 1) + 1)) + (- (s . 0)) is ext-real V33() real set

s . ((m + 1) + 1) is ext-real V33() real Element of REAL

(s) . (m + 1) is ext-real V33() real Element of REAL

(s . ((m + 1) + 1)) + ((s) . (m + 1)) is ext-real V33() real Element of REAL

((s . ((m + 1) + 1)) + ((s) . (m + 1))) - (s . 0) is ext-real V33() real Element of REAL

((s . ((m + 1) + 1)) + ((s) . (m + 1))) + (- (s . 0)) is ext-real V33() real set

n . m is ext-real V33() real Element of REAL

((s . ((m + 1) + 1)) + ((s) . (m + 1))) - (n . m) is ext-real V33() real Element of REAL

- (n . m) is ext-real V33() real set

((s . ((m + 1) + 1)) + ((s) . (m + 1))) + (- (n . m)) is ext-real V33() real set

((s) . (m + 1)) - (n . m) is ext-real V33() real Element of REAL

((s) . (m + 1)) + (- (n . m)) is ext-real V33() real set

(s . ((m + 1) + 1)) + (((s) . (m + 1)) - (n . m)) is ext-real V33() real Element of REAL

((s) ^\ 1) . m is ext-real V33() real Element of REAL

(((s) ^\ 1) . m) - (n . m) is ext-real V33() real Element of REAL

(((s) ^\ 1) . m) + (- (n . m)) is ext-real V33() real set

(s . ((m + 1) + 1)) + ((((s) ^\ 1) . m) - (n . m)) is ext-real V33() real Element of REAL

(((s) ^\ 1) - n) . m is ext-real V33() real Element of REAL

(s . ((m + 1) + 1)) + ((((s) ^\ 1) - n) . m) is ext-real V33() real Element of REAL

(s ^\ 1) . (m + 1) is ext-real V33() real Element of REAL

((((s) ^\ 1) - n) . m) + ((s ^\ 1) . (m + 1)) is ext-real V33() real Element of REAL

(((s) ^\ 1) - n) . 0 is ext-real V33() real Element of REAL

((s) ^\ 1) . 0 is ext-real V33() real Element of REAL

n . 0 is ext-real V33() real Element of REAL

(((s) ^\ 1) . 0) - (n . 0) is ext-real V33() real Element of REAL

- (n . 0) is ext-real V33() real set

(((s) ^\ 1) . 0) + (- (n . 0)) is ext-real V33() real set

(((s) ^\ 1) . 0) - (s . 0) is ext-real V33() real Element of REAL

(((s) ^\ 1) . 0) + (- (s . 0)) is ext-real V33() real set

0 + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT

(s) . (0 + 1) is ext-real V33() real Element of REAL

((s) . (0 + 1)) - (s . 0) is ext-real V33() real Element of REAL

((s) . (0 + 1)) + (- (s . 0)) is ext-real V33() real set

(s) . 0 is ext-real V33() real Element of REAL

s . (0 + 1) is ext-real V33() real Element of REAL

((s) . 0) + (s . (0 + 1)) is ext-real V33() real Element of REAL

(((s) . 0) + (s . (0 + 1))) - (s . 0) is ext-real V33() real Element of REAL

(((s) . 0) + (s . (0 + 1))) + (- (s . 0)) is ext-real V33() real set

(s . (0 + 1)) + (s . 0) is ext-real V33() real Element of REAL

((s . (0 + 1)) + (s . 0)) - (s . 0) is ext-real V33() real Element of REAL

((s . (0 + 1)) + (s . 0)) + (- (s . 0)) is ext-real V33() real set

(s ^\ 1) . 0 is ext-real V33() real Element of REAL

s is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT

s ^\ n is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued subsequence of s

n + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT

s ^\ (n + 1) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued subsequence of s

(s ^\ n) . 0 is ext-real V33() real Element of REAL

NAT --> ((s ^\ n) . 0) is Relation-like NAT -defined REAL -valued Function-like constant non empty V14( NAT ) V18( NAT , REAL ) T-Sequence-like complex-valued ext-real-valued real-valued bounded_above bounded_below bounded convergent Element of K19(K20(NAT,REAL))

m is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT

m . n is ext-real V33() real Element of REAL

(s ^\ n) ^\ 1 is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued subsequence of s ^\ n

(((s ^\ n) ^\ 1)) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

((s ^\ n)) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

((s ^\ n)) ^\ 1 is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued subsequence of ((s ^\ n))

(((s ^\ n)) ^\ 1) - m is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

- m is Relation-like NAT -defined Function-like V14( NAT ) complex-valued ext-real-valued real-valued set

- 1 is non empty ext-real non positive negative V33() real integer set

(- 1) (#) m is Relation-like NAT -defined Function-like V14( NAT ) complex-valued ext-real-valued real-valued set

(((s ^\ n)) ^\ 1) + (- m) is Relation-like NAT -defined Function-like V14( NAT ) complex-valued ext-real-valued real-valued set

s ^\ 0 is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued subsequence of s

s is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT

s ^\ n is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued subsequence of s

(s) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

(s) . n is ext-real V33() real Element of REAL

NAT --> ((s) . n) is Relation-like NAT -defined REAL -valued Function-like constant non empty V14( NAT ) V18( NAT , REAL ) T-Sequence-like complex-valued ext-real-valued real-valued bounded_above bounded_below bounded convergent Element of K19(K20(NAT,REAL))

n + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT

(s) ^\ (n + 1) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued subsequence of (s)

s ^\ (n + 1) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued subsequence of s

((s ^\ (n + 1))) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

m is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

((s ^\ (n + 1))) . 0 is ext-real V33() real Element of REAL

(s ^\ (n + 1)) . 0 is ext-real V33() real Element of REAL

0 + (n + 1) is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT

s . (0 + (n + 1)) is ext-real V33() real Element of REAL

s . (n + 1) is ext-real V33() real Element of REAL

n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT

((s) ^\ (n + 1)) . n is ext-real V33() real Element of REAL

((s ^\ (n + 1))) . n is ext-real V33() real Element of REAL

m . n is ext-real V33() real Element of REAL

(((s ^\ (n + 1))) . n) + (m . n) is ext-real V33() real Element of REAL

n + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT

((s) ^\ (n + 1)) . (n + 1) is ext-real V33() real Element of REAL

((s ^\ (n + 1))) . (n + 1) is ext-real V33() real Element of REAL

m . (n + 1) is ext-real V33() real Element of REAL

(((s ^\ (n + 1))) . (n + 1)) + (m . (n + 1)) is ext-real V33() real Element of REAL

(s ^\ (n + 1)) . (n + 1) is ext-real V33() real Element of REAL

(((s ^\ (n + 1))) . n) + ((s ^\ (n + 1)) . (n + 1)) is ext-real V33() real Element of REAL

(m . (n + 1)) + ((((s ^\ (n + 1))) . n) + ((s ^\ (n + 1)) . (n + 1))) is ext-real V33() real Element of REAL

(m . (n + 1)) + (((s ^\ (n + 1))) . n) is ext-real V33() real Element of REAL

((m . (n + 1)) + (((s ^\ (n + 1))) . n)) + ((s ^\ (n + 1)) . (n + 1)) is ext-real V33() real Element of REAL

((s) . n) + (((s ^\ (n + 1))) . n) is ext-real V33() real Element of REAL

(((s) . n) + (((s ^\ (n + 1))) . n)) + ((s ^\ (n + 1)) . (n + 1)) is ext-real V33() real Element of REAL

(((s) ^\ (n + 1)) . n) + ((s ^\ (n + 1)) . (n + 1)) is ext-real V33() real Element of REAL

n + (n + 1) is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT

(s) . (n + (n + 1)) is ext-real V33() real Element of REAL

((s) . (n + (n + 1))) + ((s ^\ (n + 1)) . (n + 1)) is ext-real V33() real Element of REAL

(n + 1) + (n + 1) is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT

s . ((n + 1) + (n + 1)) is ext-real V33() real Element of REAL

((s) . (n + (n + 1))) + (s . ((n + 1) + (n + 1))) is ext-real V33() real Element of REAL

(n + (n + 1)) + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT

(s) . ((n + (n + 1)) + 1) is ext-real V33() real Element of REAL

(s) . ((n + 1) + (n + 1)) is ext-real V33() real Element of REAL

((s) ^\ (n + 1)) . 0 is ext-real V33() real Element of REAL

(s) . (0 + (n + 1)) is ext-real V33() real Element of REAL

(s . (n + 1)) + ((s) . n) is ext-real V33() real Element of REAL

m . 0 is ext-real V33() real Element of REAL

(((s ^\ (n + 1))) . 0) + (m . 0) is ext-real V33() real Element of REAL

(REAL,((s ^\ (n + 1))),m) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

(s ^\ n) ^\ 1 is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued subsequence of s ^\ n

(((s ^\ n) ^\ 1)) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

(REAL,(((s ^\ n) ^\ 1)),m) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

s is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

(s) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) 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 V14( NAT ) 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 V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT

(s) . m is ext-real V33() real Element of REAL

(n) . m is ext-real V33() real Element of REAL

m + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT

(s) . (m + 1) is ext-real V33() real Element of REAL

(n) . (m + 1) is ext-real V33() real Element of REAL

s . (m + 1) is ext-real V33() real Element of REAL

n . (m + 1) is ext-real V33() real Element of REAL

((s) . m) + (s . (m + 1)) is ext-real V33() real Element of REAL

((n) . m) + (n . (m + 1)) is ext-real V33() real Element of REAL

(n) . 0 is ext-real V33() real Element of REAL

n . 0 is ext-real V33() real Element of REAL

(s) . 0 is ext-real V33() real Element of REAL

s . 0 is ext-real V33() real Element of REAL

s is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

(s) is ext-real V33() real Element of REAL

(s) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

lim (s) is ext-real V33() real Element of REAL

n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT

(s) . n is ext-real V33() real Element of REAL

n + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT

s ^\ (n + 1) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued subsequence of s

((s ^\ (n + 1))) is ext-real V33() real Element of REAL

((s ^\ (n + 1))) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

lim ((s ^\ (n + 1))) is ext-real V33() real Element of REAL

((s) . n) + ((s ^\ (n + 1))) is ext-real V33() real Element of REAL

(s) . (n + 1) is ext-real V33() real Element of REAL

(n + 1) + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT

s ^\ ((n + 1) + 1) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued subsequence of s

((s ^\ ((n + 1) + 1))) is ext-real V33() real Element of REAL

((s ^\ ((n + 1) + 1))) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

lim ((s ^\ ((n + 1) + 1))) is ext-real V33() real Element of REAL

((s) . (n + 1)) + ((s ^\ ((n + 1) + 1))) is ext-real V33() real Element of REAL

(s ^\ (n + 1)) . 0 is ext-real V33() real Element of REAL

NAT --> ((s ^\ (n + 1)) . 0) is Relation-like NAT -defined REAL -valued Function-like constant non empty V14( NAT ) V18( NAT , REAL ) T-Sequence-like complex-valued ext-real-valued real-valued bounded_above bounded_below bounded convergent Element of K19(K20(NAT,REAL))

m is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT

m . n is ext-real V33() real Element of REAL

(s ^\ (n + 1)) ^\ 1 is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued subsequence of s ^\ (n + 1)

(((s ^\ (n + 1)) ^\ 1)) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

((s ^\ (n + 1))) ^\ 1 is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued subsequence of ((s ^\ (n + 1)))

(((s ^\ (n + 1))) ^\ 1) - m is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

- m is Relation-like NAT -defined Function-like V14( NAT ) complex-valued ext-real-valued real-valued set

- 1 is non empty ext-real non positive negative V33() real integer set

(- 1) (#) m is Relation-like NAT -defined Function-like V14( NAT ) complex-valued ext-real-valued real-valued set

(((s ^\ (n + 1))) ^\ 1) + (- m) is Relation-like NAT -defined Function-like V14( NAT ) complex-valued ext-real-valued real-valued set

lim (((s ^\ (n + 1)) ^\ 1)) is ext-real V33() real Element of REAL

lim (((s ^\ (n + 1))) ^\ 1) is ext-real V33() real Element of REAL

lim m is ext-real V33() real Element of REAL

(lim (((s ^\ (n + 1))) ^\ 1)) - (lim m) is ext-real V33() real Element of REAL

- (lim m) is ext-real V33() real set

(lim (((s ^\ (n + 1))) ^\ 1)) + (- (lim m)) is ext-real V33() real set

(lim ((s ^\ (n + 1)))) - (lim m) is ext-real V33() real Element of REAL

(lim ((s ^\ (n + 1)))) + (- (lim m)) is ext-real V33() real set

m . 0 is ext-real V33() real Element of REAL

((s ^\ (n + 1))) - (m . 0) is ext-real V33() real Element of REAL

- (m . 0) is ext-real V33() real set

((s ^\ (n + 1))) + (- (m . 0)) is ext-real V33() real set

((s ^\ (n + 1))) - ((s ^\ (n + 1)) . 0) is ext-real V33() real Element of REAL

- ((s ^\ (n + 1)) . 0) is ext-real V33() real set

((s ^\ (n + 1))) + (- ((s ^\ (n + 1)) . 0)) is ext-real V33() real set

((s) . n) + ((s ^\ (n + 1)) . 0) is ext-real V33() real Element of REAL

(s) - (((s) . n) + ((s ^\ (n + 1)) . 0)) is ext-real V33() real Element of REAL

- (((s) . n) + ((s ^\ (n + 1)) . 0)) is ext-real V33() real set

(s) + (- (((s) . n) + ((s ^\ (n + 1)) . 0))) is ext-real V33() real set

0 + (n + 1) is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT

s . (0 + (n + 1)) is ext-real V33() real Element of REAL

((s) . n) + (s . (0 + (n + 1))) is ext-real V33() real Element of REAL

(s) - (((s) . n) + (s . (0 + (n + 1)))) is ext-real V33() real Element of REAL

- (((s) . n) + (s . (0 + (n + 1)))) is ext-real V33() real set

(s) + (- (((s) . n) + (s . (0 + (n + 1))))) is ext-real V33() real set

(s) - ((s) . (n + 1)) is ext-real V33() real Element of REAL

- ((s) . (n + 1)) is ext-real V33() real set

(s) + (- ((s) . (n + 1))) is ext-real V33() real set

(s) . 0 is ext-real V33() real Element of REAL

0 + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT

s ^\ (0 + 1) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued subsequence of s

((s ^\ (0 + 1))) is ext-real V33() real Element of REAL

((s ^\ (0 + 1))) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

lim ((s ^\ (0 + 1))) is ext-real V33() real Element of REAL

((s) . 0) + ((s ^\ (0 + 1))) is ext-real V33() real Element of REAL

s . 0 is ext-real V33()