:: SERIES_1 semantic presentation

K19(REAL) is set

K19(omega) is set
K19(NAT) is set

K19(K20(NAT,REAL)) is set

K19(K20(COMPLEX,COMPLEX)) is set

K19(K20(COMPLEX,REAL)) is set

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

K19(K20(REAL,REAL)) is set

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

K19(K20(RAT,RAT)) is set

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

K19(K20(INT,INT)) is set

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

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

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

1r is V33() Element of COMPLEX

s is ext-real V33() real set

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

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

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

(n . s2) + () is ext-real V33() real set
abs ((n . s2) - 0) 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
(n . s2) + () 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) to_power n is ext-real V33() real set
(abs s) |^ 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

- s is ext-real V33() real set
(- s) to_power m is ext-real V33() real 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 n) is ext-real V33() real set
abs (- (s to_power n)) is ext-real V33() real Element of REAL

s is ext-real V33() real set

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 . n is ext-real V33() real Element of REAL

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

K19(K20(NAT,COMPLEX)) is set

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 . 0 is V33() set

K19(K20(NAT,COMPLEX)) is set

k is V33() Element of COMPLEX

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 . 0 is V33() Element of COMPLEX

n . 0 is V33() set

m . 0 is V33() set

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

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

m is set

(s) . m is V33() set

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

(s) . k is V33() set

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

(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

(s) . n is V33() set

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

(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) . n is ext-real V33() real Element of REAL
((s) . n) + ((s ^\ 1) . n) is ext-real V33() real Element of REAL

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

- 1 is non empty ext-real non positive negative V33() real integer 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))

(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

(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

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 . n is V33() set
n . n is V33() set
m . n is V33() set
(n . n) + (m . n) is V33() set

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

s is non empty complex-membered add-closed set
K20(NAT,s) is complex-valued set
K19(K20(NAT,s)) is 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))

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

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

((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 ext-real V33() real Element of REAL

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

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

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

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

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

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

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

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

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

lim ((s - n)) is ext-real V33() real Element of REAL
(n) is ext-real V33() real Element of 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

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

(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

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

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

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

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

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

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

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

(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

(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 ^\ n) . 0 is ext-real V33() real Element of REAL

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

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

(s) . n is ext-real V33() real Element of 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

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

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

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

(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

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

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

(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) . m is ext-real V33() real Element of REAL
(n) . m 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) 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 ext-real V33() real Element of REAL

lim (s) 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

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

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

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

- 1 is non empty ext-real non positive negative V33() real integer 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 (((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

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

((s ^\ (0 + 1))) is ext-real V33() real Element of 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()