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