:: TAYLOR_1 semantic presentation

REAL is non empty V69() V80() V81() V82() V86() V97() V98() V100() set
NAT is non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() Element of K19(REAL)
K19(REAL) is set
COMPLEX is non empty V69() V80() V86() set
K20(REAL,REAL) is V33() V34() V35() set
K19(K20(REAL,REAL)) is set
K20(NAT,REAL) is V33() V34() V35() set
K19(K20(NAT,REAL)) is set
omega is non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() set
K19(omega) is set
K19(NAT) is set
RAT is non empty V69() V80() V81() V82() V83() V86() set
INT is non empty V69() V80() V81() V82() V83() V84() V86() set
K20(NAT,COMPLEX) is V33() set
K19(K20(NAT,COMPLEX)) is set
K20(COMPLEX,COMPLEX) is V33() set
K19(K20(COMPLEX,COMPLEX)) is set
1 is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative integer non irrational V80() V81() V82() V83() V84() V85() V95() V97() Element of NAT

exp_R is V1() V4( REAL ) V5( REAL ) Function-like non empty total quasi_total V33() V34() V35() continuous Element of K19(K20(REAL,REAL))
dom exp_R is V80() V81() V82() Element of K19(REAL)

exp_R 1 is V22() real ext-real Element of REAL
[#] REAL is closed open V80() V81() V82() Element of K19(REAL)

+infty is non empty non real ext-real positive non negative set

f is V1() V4( REAL ) V5( REAL ) Function-like non empty total quasi_total V33() V34() V35() Element of K19(K20(REAL,REAL))
x0 is V22() real ext-real set
f . x0 is V22() real ext-real Element of REAL
x0 #Z n is V22() real ext-real set
f is V1() V4( REAL ) V5( REAL ) Function-like non empty total quasi_total V33() V34() V35() Element of K19(K20(REAL,REAL))
x0 is V1() V4( REAL ) V5( REAL ) Function-like non empty total quasi_total V33() V34() V35() Element of K19(K20(REAL,REAL))
r is V22() real ext-real Element of REAL
f . r is V22() real ext-real Element of REAL
x0 . r is V22() real ext-real Element of REAL
r #Z n is V22() real ext-real Element of REAL
n is V22() real ext-real set

n #Z (x0 + f) is V22() real ext-real set
n #Z x0 is V22() real ext-real set
n #Z f is V22() real ext-real set
(n #Z x0) * (n #Z f) is V22() real ext-real set
0 #Z (x0 + f) is V22() real ext-real Element of REAL

n #Z () is V22() real ext-real set

1 * (n #Z 0) is V22() real ext-real Element of REAL
(n #Z 0) * (n #Z 0) is V22() real ext-real set
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative integer non irrational V80() V81() V82() V83() V84() V85() V95() V97() Element of NAT
0 #Z x0 is V22() real ext-real Element of REAL

(0 #Z x0) * (0 #Z f) is V22() real ext-real Element of REAL

(0 |^ (abs x0)) * (0 #Z f) is V22() real ext-real Element of REAL
(0 |^ x0) * (0 #Z f) is V22() real ext-real Element of REAL
0 * (0 #Z f) is V22() real ext-real Element of REAL

0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative integer non irrational V80() V81() V82() V83() V84() V85() V95() V97() Element of NAT
0 #Z x0 is V22() real ext-real Element of REAL

(0 #Z x0) * (0 #Z f) is V22() real ext-real Element of REAL

(0 |^ (abs f)) * (0 #Z x0) is V22() real ext-real Element of REAL
(0 |^ f) * (0 #Z x0) is V22() real ext-real Element of REAL
0 * (0 #Z x0) is V22() real ext-real Element of REAL

(n) is V1() V4( REAL ) V5( REAL ) Function-like non empty total quasi_total V33() V34() V35() Element of K19(K20(REAL,REAL))
n - 1 is V22() real ext-real integer non irrational Element of REAL
f is V22() real ext-real set
diff ((n),f) is V22() real ext-real Element of REAL
f #Z (n - 1) is V22() real ext-real set
n * (f #Z (n - 1)) is V22() real ext-real set
x0 is V22() real ext-real Element of REAL
(1) is V1() V4( REAL ) V5( REAL ) Function-like non empty total quasi_total V33() V34() V35() Element of K19(K20(REAL,REAL))
(1) . x0 is V22() real ext-real Element of REAL
x0 #Z 1 is V22() real ext-real Element of REAL
1 * x0 is V22() real ext-real Element of REAL
(1 * x0) + 0 is V22() real ext-real Element of REAL
dom (1) is V80() V81() V82() Element of K19(REAL)
x0 is V22() real ext-real set
diff ((1),x0) is V22() real ext-real Element of REAL
(1) `| REAL is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
((1) `| REAL) . x0 is V22() real ext-real Element of REAL

(x0) is V1() V4( REAL ) V5( REAL ) Function-like non empty total quasi_total V33() V34() V35() Element of K19(K20(REAL,REAL))
x0 - 1 is V22() real ext-real integer non irrational Element of REAL
x0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative integer non irrational V80() V81() V82() V83() V84() V85() V95() V97() Element of NAT
((x0 + 1)) is V1() V4( REAL ) V5( REAL ) Function-like non empty total quasi_total V33() V34() V35() Element of K19(K20(REAL,REAL))
(x0 + 1) - 1 is V22() real ext-real integer non irrational Element of REAL
r is V22() real ext-real set
diff (((x0 + 1)),r) is V22() real ext-real Element of REAL
r #Z ((x0 + 1) - 1) is V22() real ext-real set
(x0 + 1) * (r #Z ((x0 + 1) - 1)) is V22() real ext-real set
(x0 + 1) - 1 is V22() real ext-real integer non irrational Element of REAL
r #Z ((x0 + 1) - 1) is V22() real ext-real set
(x0 + 1) * (r #Z ((x0 + 1) - 1)) is V22() real ext-real Element of REAL
1 - 1 is V22() real ext-real integer non irrational Element of REAL
dom ((x0 + 1)) is V80() V81() V82() Element of K19(REAL)
x is V22() real ext-real set
t is set
((x0 + 1)) . t is V22() real ext-real Element of REAL
(x0) . t is V22() real ext-real Element of REAL
(1) . t is V22() real ext-real Element of REAL
((x0) . t) * ((1) . t) is V22() real ext-real Element of REAL
c is V22() real ext-real Element of REAL
c #Z (x0 + 1) is V22() real ext-real Element of REAL
c #Z x0 is V22() real ext-real Element of REAL
c #Z 1 is V22() real ext-real Element of REAL
(c #Z x0) * (c #Z 1) is V22() real ext-real Element of REAL
((x0) . t) * (c #Z 1) is V22() real ext-real Element of REAL
dom (x0) is V80() V81() V82() Element of K19(REAL)
(dom (x0)) /\ (dom (1)) is V80() V81() V82() Element of K19(REAL)
() /\ (dom (1)) is V80() V81() V82() Element of K19(REAL)
() /\ REAL is V80() V81() V82() Element of K19(REAL)
(x0) (#) (1) is V1() V4( REAL ) V5( REAL ) Function-like non empty total quasi_total V33() V34() V35() Element of K19(K20(REAL,REAL))
diff (((x0 + 1)),x) is V22() real ext-real Element of REAL
diff (((x0) (#) (1)),x) is V22() real ext-real Element of REAL
(x0) . x is V22() real ext-real Element of REAL
diff ((1),x) is V22() real ext-real Element of REAL
((x0) . x) * (diff ((1),x)) is V22() real ext-real Element of REAL
diff ((x0),x) is V22() real ext-real Element of REAL
(1) . x is V22() real ext-real Element of REAL
(diff ((x0),x)) * ((1) . x) is V22() real ext-real Element of REAL
(((x0) . x) * (diff ((1),x))) + ((diff ((x0),x)) * ((1) . x)) is V22() real ext-real Element of REAL
((x0) . x) * 1 is V22() real ext-real Element of REAL
(((x0) . x) * 1) + ((diff ((x0),x)) * ((1) . x)) is V22() real ext-real Element of REAL
x #Z x0 is V22() real ext-real set
(x #Z x0) * 1 is V22() real ext-real Element of REAL
((x #Z x0) * 1) + ((diff ((x0),x)) * ((1) . x)) is V22() real ext-real Element of REAL
x #Z 1 is V22() real ext-real set
(diff ((x0),x)) * (x #Z 1) is V22() real ext-real Element of REAL
((x #Z x0) * 1) + ((diff ((x0),x)) * (x #Z 1)) is V22() real ext-real Element of REAL

x #Z r is V22() real ext-real set
x0 * (x #Z r) is V22() real ext-real set
(x0 * (x #Z r)) * (x #Z 1) is V22() real ext-real set
(x #Z x0) + ((x0 * (x #Z r)) * (x #Z 1)) is V22() real ext-real set
(x #Z r) * (x #Z 1) is V22() real ext-real set
x0 * ((x #Z r) * (x #Z 1)) is V22() real ext-real set
(x #Z x0) + (x0 * ((x #Z r) * (x #Z 1))) is V22() real ext-real set
r + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative integer non irrational V80() V81() V82() V83() V84() V85() V95() V97() Element of NAT
x #Z (r + 1) is V22() real ext-real set
x0 * (x #Z (r + 1)) is V22() real ext-real set
(x #Z x0) + (x0 * (x #Z (r + 1))) is V22() real ext-real set
(x0 + 1) - 1 is V22() real ext-real integer non irrational Element of REAL
x #Z ((x0 + 1) - 1) is V22() real ext-real set
(x0 + 1) * (x #Z ((x0 + 1) - 1)) is V22() real ext-real Element of REAL
(x0 + 1) - 1 is V22() real ext-real integer non irrational Element of REAL
(x0 + 1) - 1 is V22() real ext-real integer non irrational Element of REAL
r is V22() real ext-real set
x is V22() real ext-real set
diff (((x0 + 1)),x) is V22() real ext-real Element of REAL
x #Z ((x0 + 1) - 1) is V22() real ext-real set
(x0 + 1) * (x #Z ((x0 + 1) - 1)) is V22() real ext-real set
(0) is V1() V4( REAL ) V5( REAL ) Function-like non empty total quasi_total V33() V34() V35() Element of K19(K20(REAL,REAL))
0 - 1 is non empty V22() real ext-real non positive negative integer non irrational Element of REAL
x0 is V22() real ext-real set
diff ((0),x0) is V22() real ext-real Element of REAL
x0 #Z (0 - 1) is V22() real ext-real set
0 * (x0 #Z (0 - 1)) is V22() real ext-real set
dom (0) is V80() V81() V82() Element of K19(REAL)
x is set
c is set
{1} is non empty V80() V81() V82() V83() V84() V85() V95() V97() set
(0) . x is V22() real ext-real Element of REAL
t is V22() real ext-real Element of REAL

rng (0) is V80() V81() V82() Element of K19(REAL)
x is set
t is set
(0) . t is V22() real ext-real Element of REAL
c is V22() real ext-real Element of REAL
(0) . c is V22() real ext-real Element of REAL

(0) `| (dom (0)) is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
((0) `| (dom (0))) . x0 is V22() real ext-real Element of REAL
0 - 1 is non empty V22() real ext-real non positive negative integer non irrational Element of REAL
x0 #Z (0 - 1) is V22() real ext-real set
0 * (x0 #Z (0 - 1)) is V22() real ext-real Element of REAL

(n) is V1() V4( REAL ) V5( REAL ) Function-like non empty total quasi_total V33() V34() V35() Element of K19(K20(REAL,REAL))
n - 1 is V22() real ext-real integer non irrational Element of REAL
f is V22() real ext-real set
x0 is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
(n) * x0 is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
diff (((n) * x0),f) is V22() real ext-real Element of REAL
x0 . f is V22() real ext-real Element of REAL
(x0 . f) #Z (n - 1) is V22() real ext-real Element of REAL
n * ((x0 . f) #Z (n - 1)) is V22() real ext-real Element of REAL
diff (x0,f) is V22() real ext-real Element of REAL
(n * ((x0 . f) #Z (n - 1))) * (diff (x0,f)) is V22() real ext-real Element of REAL
diff ((n),(x0 . f)) is V22() real ext-real Element of REAL
(diff ((n),(x0 . f))) * (diff (x0,f)) is V22() real ext-real Element of REAL

f is V22() real ext-real set

() #R n is V22() real ext-real set
n * f is V22() real ext-real set
exp_R (n * f) is V22() real ext-real set
x0 is V22() real ext-real Element of REAL
exp_R x0 is V22() real ext-real Element of REAL

(exp_R x0) #R r is V22() real ext-real set
r * x0 is V22() real ext-real Element of REAL
exp_R (r * x0) is V22() real ext-real Element of REAL
r + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative integer non irrational V80() V81() V82() V83() V84() V85() V95() V97() Element of NAT
(exp_R x0) #R (r + 1) is V22() real ext-real set
(r + 1) * x0 is V22() real ext-real Element of REAL
exp_R ((r + 1) * x0) is V22() real ext-real Element of REAL
(exp_R x0) #R (r + 1) is V22() real ext-real Element of REAL
(exp_R x0) #R 1 is V22() real ext-real Element of REAL
((exp_R x0) #R r) * ((exp_R x0) #R 1) is V22() real ext-real Element of REAL
((exp_R x0) #R r) * (exp_R x0) is V22() real ext-real Element of REAL

x * x0 is V22() real ext-real Element of REAL
(x * x0) + x0 is V22() real ext-real Element of REAL
exp_R ((x * x0) + x0) is V22() real ext-real Element of REAL
(r + 1) * x0 is V22() real ext-real Element of REAL
exp_R ((r + 1) * x0) is V22() real ext-real Element of REAL
(exp_R x0) #R 0 is V22() real ext-real set
0 * x0 is V22() real ext-real Element of REAL
exp_R (0 * x0) is V22() real ext-real Element of REAL
n is V22() real ext-real set
- n is V22() real ext-real set
exp_R (- n) is V22() real ext-real set

1 / () is V22() real ext-real Element of REAL
f is V22() real ext-real Element of REAL
- f is V22() real ext-real Element of REAL
exp_R (- f) is V22() real ext-real Element of REAL

(exp_R (- f)) * () is V22() real ext-real Element of REAL
(- f) + f is V22() real ext-real Element of REAL
exp_R ((- f) + f) is V22() real ext-real Element of REAL

f is V22() real ext-real set

() #R n is V22() real ext-real set
n * f is V22() real ext-real set
exp_R (n * f) is V22() real ext-real set

- x0 is V22() real ext-real non positive integer non irrational Element of REAL
x0 * f is V22() real ext-real Element of REAL
- (x0 * f) is V22() real ext-real Element of REAL
exp_R (- (x0 * f)) is V22() real ext-real Element of REAL
exp_R (x0 * f) is V22() real ext-real Element of REAL
1 / (exp_R (x0 * f)) is V22() real ext-real Element of REAL
() #R x0 is V22() real ext-real set
1 / (() #R x0) is V22() real ext-real Element of REAL

1 / n is V22() real ext-real non irrational Element of REAL
f is V22() real ext-real set

() #R (1 / n) is V22() real ext-real set
f / n is V22() real ext-real Element of COMPLEX
exp_R (f / n) is V22() real ext-real set
(f / n) * n is V22() real ext-real set
exp_R ((f / n) * n) is V22() real ext-real set
(exp_R (f / n)) #R n is V22() real ext-real set
n * (1 / n) is V22() real ext-real non irrational Element of REAL
(exp_R (f / n)) #R (n * (1 / n)) is V22() real ext-real set
(exp_R (f / n)) #R 1 is V22() real ext-real set

() #R (1 / 0) is V22() real ext-real set
f / 0 is V22() real ext-real Element of REAL
exp_R (f / 0) is V22() real ext-real Element of REAL
n is V22() real ext-real set

x0 is V22() real ext-real integer non irrational set
f / x0 is V22() real ext-real non irrational Element of COMPLEX
() #R (f / x0) is V22() real ext-real set
(f / x0) * n is V22() real ext-real set
exp_R ((f / x0) * n) is V22() real ext-real set
n / x0 is V22() real ext-real Element of COMPLEX
(n / x0) * f is V22() real ext-real set
exp_R ((n / x0) * f) is V22() real ext-real set
exp_R (n / x0) is V22() real ext-real set
(exp_R (n / x0)) #R f is V22() real ext-real set
1 / x0 is V22() real ext-real non irrational Element of REAL
() #R (1 / x0) is V22() real ext-real set
(() #R (1 / x0)) #R f is V22() real ext-real set
(1 / x0) * f is V22() real ext-real non irrational Element of REAL
() #R ((1 / x0) * f) is V22() real ext-real set
(f / x0) * 1 is V22() real ext-real non irrational Element of REAL
() #R ((f / x0) * 1) is V22() real ext-real set
n is V22() real ext-real set

f is V22() real ext-real non irrational set
() #R f is V22() real ext-real set
f * n is V22() real ext-real set
exp_R (f * n) is V22() real ext-real set

x0 is V22() real ext-real integer non irrational set
x0 / r is V22() real ext-real non irrational Element of REAL
n is V22() real ext-real set

f is V22() real ext-real non irrational set
() #Q f is V22() real ext-real set
f * n is V22() real ext-real set
exp_R (f * n) is V22() real ext-real set
() #R f is V22() real ext-real set
n is V22() real ext-real set

f is V22() real ext-real set
() #R f is V22() real ext-real set
f * n is V22() real ext-real set
exp_R (f * n) is V22() real ext-real set
x0 is V1() V4( NAT ) V5( REAL ) V5( RAT ) Function-like non empty total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
lim x0 is V22() real ext-real Element of REAL
() #Q x0 is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
lim (() #Q x0) is V22() real ext-real Element of REAL
n * f is V22() real ext-real set
n (#) x0 is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
rng (n (#) x0) is V80() V81() V82() Element of K19(REAL)
r is set
(() #Q x0) . r is V22() real ext-real Element of REAL

x0 . x is V22() real ext-real non irrational Element of REAL
() #Q (x0 . x) is V22() real ext-real set
(x0 . x) * n is V22() real ext-real Element of REAL
exp_R ((x0 . x) * n) is V22() real ext-real Element of REAL
(n (#) x0) . x is V22() real ext-real Element of REAL
exp_R ((n (#) x0) . x) is V22() real ext-real Element of REAL
exp_R . ((n (#) x0) . x) is V22() real ext-real Element of REAL
exp_R /* (n (#) x0) is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
(exp_R /* (n (#) x0)) . r is V22() real ext-real Element of REAL
lim (n (#) x0) is V22() real ext-real Element of REAL
lim (exp_R /* (n (#) x0)) is V22() real ext-real Element of REAL
exp_R . (n * f) is V22() real ext-real Element of REAL

n is V22() real ext-real set
() #R n is V22() real ext-real set

() to_power n is V22() real ext-real set

n * 1 is V22() real ext-real Element of REAL
exp_R (n * 1) is V22() real ext-real Element of REAL
exp_R . 1 is V22() real ext-real Element of REAL
n is V22() real ext-real set
() #R n is V22() real ext-real set

() to_power n is V22() real ext-real set

() #R n is V22() real ext-real set

() to_power n is V22() real ext-real set
2 is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative integer non irrational V80() V81() V82() V83() V84() V85() V95() V97() Element of NAT
- 1 is V22() real ext-real non positive integer non irrational Element of REAL
n is V22() real ext-real set

n |^ 1 is V22() real ext-real set
n |^ 2 is V22() real ext-real set
n * n is V22() real ext-real set

n |^ (2 * x) is V22() real ext-real set
n |^ x is V22() real ext-real set
(n |^ x) |^ 2 is V22() real ext-real set
(- 1) |^ (2 * x) is V22() real ext-real Element of REAL
(2 * x) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative integer non irrational V80() V81() V82() V83() V84() V85() V95() V97() V110() Element of NAT
(- 1) |^ ((2 * x) + 1) is V22() real ext-real Element of REAL
n GeoSeq is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
() . 0 is V22() real ext-real Element of REAL
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative integer non irrational V80() V81() V82() V83() V84() V85() V95() V97() Element of NAT
() . (0 + 1) is V22() real ext-real Element of REAL
(() . 0) * n is V22() real ext-real Element of REAL
1 * n is V22() real ext-real Element of REAL
1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative integer non irrational V80() V81() V82() V83() V84() V85() V95() V97() Element of NAT
n |^ (1 + 1) is V22() real ext-real set
1 |^ (2 * x) is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative integer non irrational V80() V81() V82() V83() V84() V85() V97() Element of NAT
((- 1) |^ (2 * x)) * (- 1) is V22() real ext-real Element of REAL
1 rExpSeq is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
Partial_Sums () is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))

() . n is V22() real ext-real Element of REAL
n + 1 is V22() real ext-real integer non irrational Element of REAL
() . (n + 1) is V22() real ext-real Element of REAL

f + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative integer non irrational V80() V81() V82() V83() V84() V85() V95() V97() Element of NAT
() . (f + 1) is V22() real ext-real Element of REAL
() . f is V22() real ext-real Element of REAL
() . (f + 1) is V22() real ext-real Element of REAL
(() . f) + (() . (f + 1)) is V22() real ext-real Element of REAL
1 |^ (f + 1) is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative integer non irrational V80() V81() V82() V83() V84() V85() V97() Element of NAT

(1 |^ (f + 1)) / ((f + 1) !) is V22() real ext-real non negative non irrational Element of REAL
(() . f) + ((1 |^ (f + 1)) / ((f + 1) !)) is V22() real ext-real Element of REAL
() . 1 is V22() real ext-real Element of REAL
() . 0 is V22() real ext-real Element of REAL
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative integer non irrational V80() V81() V82() V83() V84() V85() V95() V97() Element of NAT
() . (0 + 1) is V22() real ext-real Element of REAL
(() . 0) + (() . (0 + 1)) is V22() real ext-real Element of REAL
() . 0 is V22() real ext-real Element of REAL
() . 1 is V22() real ext-real Element of REAL
(() . 0) + (() . 1) is V22() real ext-real Element of REAL

(1 |^ 1) / (1 !) is V22() real ext-real non negative non irrational Element of REAL
(() . 0) + ((1 |^ 1) / (1 !)) is V22() real ext-real Element of REAL

(1 |^ 0) / () is V22() real ext-real non negative non irrational Element of REAL
((1 |^ 0) / ()) + ((1 |^ 1) / (1 !)) is V22() real ext-real non negative non irrational Element of REAL
1 + ((1 |^ 1) / (1 !)) is non empty V22() real ext-real positive non negative non irrational Element of REAL
1 / 1 is V22() real ext-real non negative non irrational Element of REAL
1 + (1 / 1) is non empty V22() real ext-real positive non negative non irrational Element of REAL

() . n is V22() real ext-real Element of REAL
() ^\ 1 is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))

(() ^\ 1) . n is V22() real ext-real Element of REAL
n + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative integer non irrational V80() V81() V82() V83() V84() V85() V95() V97() Element of NAT
() . (n + 1) is V22() real ext-real Element of REAL
lim () is V22() real ext-real Element of REAL
Sum () is V22() real ext-real Element of REAL
lim (() ^\ 1) is V22() real ext-real Element of REAL
n is V22() real ext-real set

log (number_e,()) is V22() real ext-real set

n is V22() real ext-real set

log (number_e,()) is V22() real ext-real Element of REAL

log (number_e,()) is V22() real ext-real set
n is V22() real ext-real set
log (number_e,n) is V22() real ext-real set
exp_R (log (number_e,n)) is V22() real ext-real set

n is V22() real ext-real set
log (number_e,n) is V22() real ext-real set
exp_R . (log (number_e,n)) is V22() real ext-real Element of REAL
exp_R (log (number_e,n)) is V22() real ext-real set
rng exp_R is V80() V81() V82() Element of K19(REAL)
right_open_halfline 0 is open V80() V81() V82() Element of K19(REAL)
K140(0,+infty) is V95() V96() V100() set
n is set
f is set

r is V22() real ext-real Element of REAL

log (number_e,()) is V22() real ext-real Element of REAL
x0 is V22() real ext-real Element of REAL
exp_R . x0 is V22() real ext-real Element of REAL
log (number_e,(exp_R . x0)) is V22() real ext-real Element of REAL
n is V22() real ext-real Element of REAL
diff (exp_R,n) is V22() real ext-real Element of REAL

n is V22() real ext-real Element of REAL
diff (exp_R,n) is V22() real ext-real Element of REAL

n is set
f is set

r is V22() real ext-real Element of REAL

x0 is V22() real ext-real Element of REAL
{ b1 where b1 is V22() real ext-real Element of REAL : not b1 <= 0 } is set
n is set
x0 is V22() real ext-real Element of REAL
f is V22() real ext-real Element of REAL
log (number_e,f) is V22() real ext-real Element of REAL
exp_R . (log (number_e,f)) is V22() real ext-real Element of REAL
x0 is V22() real ext-real Element of REAL
exp_R " is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
dom () is V80() V81() V82() Element of K19(REAL)
n is V22() real ext-real set
diff ((),n) is V22() real ext-real Element of REAL
1 / n is V22() real ext-real Element of REAL
() . n is V22() real ext-real Element of REAL
diff (exp_R,(() . n)) is V22() real ext-real Element of REAL
exp_R . (() . n) is V22() real ext-real Element of REAL
{ b1 where b1 is V22() real ext-real Element of REAL : not b1 <= 0 } is set
n is V22() real ext-real set
f is V22() real ext-real Element of REAL
x0 is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
dom x0 is V80() V81() V82() Element of K19(REAL)
r is set
r is set

x0 . r is V22() real ext-real Element of REAL
log (n,r) is V22() real ext-real set
x0 /. r is V22() real ext-real Element of REAL
log (f,r) is V22() real ext-real Element of REAL
f is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
dom f is V80() V81() V82() Element of K19(REAL)
x0 is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
dom x0 is V80() V81() V82() Element of K19(REAL)
r is V22() real ext-real Element of REAL
f . r is V22() real ext-real Element of REAL
x0 . r is V22() real ext-real Element of REAL
log (n,r) is V22() real ext-real set
(number_e) is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
() is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
dom () is V80() V81() V82() Element of K19(REAL)
rng () is V80() V81() V82() Element of K19(REAL)
n is V22() real ext-real Element of REAL
() . n is V22() real ext-real Element of REAL
() . n is V22() real ext-real Element of REAL
log (number_e,n) is V22() real ext-real Element of REAL
{ b1 where b1 is V22() real ext-real Element of REAL : not b1 <= 0 } is set
exp_R . (log (number_e,n)) is V22() real ext-real Element of REAL
f is V22() real ext-real Element of REAL
n is V22() real ext-real Element of REAL
{ b1 where b1 is V22() real ext-real Element of REAL : not b1 <= 0 } is set

diff ((),n) is V22() real ext-real Element of REAL
{ b1 where b1 is V22() real ext-real Element of REAL : not b1 <= 0 } is set
1 / n is V22() real ext-real Element of REAL
n " is V22() real ext-real Element of REAL
f is V22() real ext-real Element of REAL
n is V22() real ext-real Element of REAL

diff ((),f) is V22() real ext-real Element of REAL
1 / f is V22() real ext-real Element of REAL

diff ((),x0) is V22() real ext-real Element of REAL
n is V22() real ext-real set
f is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
exp_R * f is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
diff ((),n) is V22() real ext-real Element of REAL
f . n is V22() real ext-real Element of REAL
exp_R . (f . n) is V22() real ext-real Element of REAL
diff (f,n) is V22() real ext-real Element of REAL
(exp_R . (f . n)) * (diff (f,n)) is V22() real ext-real Element of REAL
diff (exp_R,(f . n)) is V22() real ext-real Element of REAL
(diff (exp_R,(f . n))) * (diff (f,n)) is V22() real ext-real Element of REAL
n is V22() real ext-real set
f is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
f . n is V22() real ext-real Element of REAL
() * f is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
diff ((() * f),n) is V22() real ext-real Element of REAL
diff (f,n) is V22() real ext-real Element of REAL
(diff (f,n)) / (f . n) is V22() real ext-real Element of REAL
{ b1 where b1 is V22() real ext-real Element of REAL : not b1 <= 0 } is set
diff ((),(f . n)) is V22() real ext-real Element of REAL
(diff ((),(f . n))) * (diff (f,n)) is V22() real ext-real Element of REAL
1 / (f . n) is V22() real ext-real Element of REAL
(1 / (f . n)) * (diff (f,n)) is V22() real ext-real Element of REAL
((diff (f,n)) / (f . n)) * 1 is V22() real ext-real Element of REAL
n is V22() real ext-real set
f is V22() real ext-real Element of REAL
x0 is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
dom x0 is V80() V81() V82() Element of K19(REAL)
r is set
r is set

x0 . r is V22() real ext-real Element of REAL
r #R n is V22() real ext-real set
x0 /. r is V22() real ext-real Element of REAL
r #R f is V22() real ext-real Element of REAL
f is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
dom f is V80() V81() V82() Element of K19(REAL)
x0 is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
dom x0 is V80() V81() V82() Element of K19(REAL)
r is V22() real ext-real Element of REAL
f . r is V22() real ext-real Element of REAL
x0 . r is V22() real ext-real Element of REAL
r #R n is V22() real ext-real set
n is V22() real ext-real set
f is V22() real ext-real set
(f) is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
diff ((f),n) is V22() real ext-real Element of REAL
f - 1 is V22() real ext-real Element of REAL
n #R (f - 1) is V22() real ext-real set
f * (n #R (f - 1)) is V22() real ext-real set
f (#) () is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
exp_R * (f (#) ()) is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
r is V22() real ext-real Element of REAL
diff ((exp_R * (f (#) ())),r) is V22() real ext-real Element of REAL
r #R (f - 1) is V22() real ext-real Element of REAL
f * (r #R (f - 1)) is V22() real ext-real Element of REAL
{ b1 where b1 is V22() real ext-real Element of REAL : not b1 <= 0 } is set
dom (f (#) ()) is V80() V81() V82() Element of K19(REAL)
diff ((f (#) ()),r) is V22() real ext-real Element of REAL
diff ((),r) is V22() real ext-real Element of REAL
f * (diff ((),r)) is V22() real ext-real Element of REAL
1 / r is V22() real ext-real Element of REAL
f * (1 / r) is V22() real ext-real Element of REAL
(f (#) ()) . r is V22() real ext-real Element of REAL
diff (exp_R,((f (#) ()) . r)) is V22() real ext-real Element of REAL
exp_R . ((f (#) ()) . r) is V22() real ext-real Element of REAL
() . r is V22() real ext-real Element of REAL
f * (() . r) is V22() real ext-real Element of REAL
exp_R . (f * (() . r)) is V22() real ext-real Element of REAL
log (number_e,r) is V22() real ext-real Element of REAL
f * (log (number_e,r)) is V22() real ext-real Element of REAL
exp_R . (f * (log (number_e,r))) is V22() real ext-real Element of REAL

log (number_e,(r to_power f)) is V22() real ext-real set
exp_R . (log (number_e,(r to_power f))) is V22() real ext-real Element of REAL
(r to_power f) * (f * (1 / r)) is V22() real ext-real Element of REAL
(r to_power f) * (1 / r) is V22() real ext-real Element of REAL
f * ((r to_power f) * (1 / r)) is V22() real ext-real Element of REAL
r to_power 1 is V22() real ext-real Element of REAL
1 / (r to_power 1) is V22() real ext-real Element of REAL
(r to_power f) * (1 / (r to_power 1)) is V22() real ext-real Element of REAL
f * ((r to_power f) * (1 / (r to_power 1))) is V22() real ext-real Element of REAL
- 1 is V22() real ext-real non positive integer non irrational Element of REAL
r to_power (- 1) is V22() real ext-real Element of REAL
(r to_power f) * (r to_power (- 1)) is V22() real ext-real Element of REAL
f * ((r to_power f) * (r to_power (- 1))) is V22() real ext-real Element of REAL
f + (- 1) is V22() real ext-real Element of REAL
r to_power (f + (- 1)) is V22() real ext-real Element of REAL
f * (r to_power (f + (- 1))) is V22() real ext-real Element of REAL
rng (f (#) ()) is V80() V81() V82() Element of K19(REAL)
dom (exp_R * (f (#) ())) is V80() V81() V82() Element of K19(REAL)
dom (f (#) ()) is V80() V81() V82() Element of K19(REAL)
r is V22() real ext-real Element of REAL
(exp_R * (f (#) ())) . r is V22() real ext-real Element of REAL
(f) . r is V22() real ext-real Element of REAL
{ b1 where b1 is V22() real ext-real Element of REAL : not b1 <= 0 } is set
(exp_R * (f (#) ())) /. r is V22() real ext-real Element of REAL
(f (#) ()) /. r is V22() real ext-real Element of REAL
exp_R /. ((f (#) ()) /. r) is V22() real ext-real Element of REAL
exp_R . ((f (#) ()) /. r) is V22() real ext-real Element of REAL
(f (#) ()) . r is V22() real ext-real Element of REAL
exp_R . ((f (#) ()) . r) is V22() real ext-real Element of REAL
() . r is V22() real ext-real Element of REAL
f * (() . r) is V22() real ext-real Element of REAL
exp_R . (f * (() . r)) is V22() real ext-real Element of REAL
log (number_e,r) is V22() real ext-real Element of REAL
f * (log (number_e,r)) is V22() real ext-real Element of REAL
exp_R . (f * (log (number_e,r))) is V22() real ext-real Element of REAL

log (number_e,(r to_power f)) is V22() real ext-real set
exp_R . (log (number_e,(r to_power f))) is V22() real ext-real Element of REAL
r #R f is V22() real ext-real set
x is V22() real ext-real Element of REAL
x is V22() real ext-real Element of REAL
x is V22() real ext-real Element of REAL
dom (f) is V80() V81() V82() Element of K19(REAL)
n is V22() real ext-real set
f is V22() real ext-real set
(f) is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
f - 1 is V22() real ext-real Element of REAL
x0 is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
x0 . n is V22() real ext-real Element of REAL
(f) * x0 is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
diff (((f) * x0),n) is V22() real ext-real Element of REAL
(x0 . n) #R (f - 1) is V22() real ext-real Element of REAL
f * ((x0 . n) #R (f - 1)) is V22() real ext-real Element of REAL
diff (x0,n) is V22() real ext-real Element of REAL
(f * ((x0 . n) #R (f - 1))) * (diff (x0,n)) is V22() real ext-real Element of REAL
diff ((f),(x0 . n)) is V22() real ext-real Element of REAL
(diff ((f),(x0 . n))) * (diff (x0,n)) is V22() real ext-real Element of REAL
PFuncs (REAL,REAL) is functional non empty set
K20(NAT,()) is set
K19(K20(NAT,())) is set
n is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
f is V80() V81() V82() Element of K19(REAL)
n | f is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))

x is Element of PFuncs (REAL,REAL)
t is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
t `| f is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
c is Element of PFuncs (REAL,REAL)
s is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
s `| f is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
x0 is Element of PFuncs (REAL,REAL)
r is V1() V4( NAT ) V5( PFuncs (REAL,REAL)) Function-like non empty total quasi_total Element of K19(K20(NAT,()))
r . 0 is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
x is V1() V4( NAT ) V5( PFuncs (REAL,REAL)) Function-like non empty total quasi_total Element of K19(K20(NAT,()))
x . 0 is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))

t + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative integer non irrational V80() V81() V82() V83() V84() V85() V95() V97() Element of NAT
x . (t + 1) is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
x . t is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
(x . t) `| f is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
c is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
c `| f is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
x0 is V1() V4( NAT ) V5( PFuncs (REAL,REAL)) Function-like non empty total quasi_total Element of K19(K20(NAT,()))
x0 . 0 is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
r is V1() V4( NAT ) V5( PFuncs (REAL,REAL)) Function-like non empty total quasi_total Element of K19(K20(NAT,()))
r . 0 is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))

x0 . x is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
r . x is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
x + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative integer non irrational V80() V81() V82() V83() V84() V85() V95() V97() Element of NAT
x0 . (x + 1) is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
r . (x + 1) is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
(x0 . x) `| f is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
n is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
f is V80() V81() V82() Element of K19(REAL)

r - 1 is V22() real ext-real integer non irrational Element of REAL
x0 - 1 is V22() real ext-real integer non irrational Element of REAL

(n,f) is V1() V4( NAT ) V5( PFuncs (REAL,REAL)) Function-like non empty total quasi_total Element of K19(K20(NAT,()))
(n,f) . x is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
n is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
f is V80() V81() V82() Element of K19(REAL)
(n,f) is V1() V4( NAT ) V5( PFuncs (REAL,REAL)) Function-like non empty total quasi_total Element of K19(K20(NAT,()))
x0 is V22() real ext-real set
r is V22() real ext-real set
r - x0 is V22() real ext-real set
x is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))

x . t is V22() real ext-real Element of REAL
(n,f) . t is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
((n,f) . t) . x0 is V22() real ext-real Element of REAL
(r - x0) |^ t is V22() real ext-real set
(((n,f) . t) . x0) * ((r - x0) |^ t) is V22() real ext-real Element of REAL

((((n,f) . t) . x0) * ((r - x0) |^ t)) / (t !) is V22() real ext-real Element of REAL
x is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
t is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
c is set
x . c is V22() real ext-real Element of REAL

(n,f) . s is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
((n,f) . s) . x0 is V22() real ext-real Element of REAL
(r - x0) |^ s is V22() real ext-real set
(((n,f) . s) . x0) * ((r - x0) |^ s) is V22() real ext-real Element of REAL

((((n,f) . s) . x0) * ((r - x0) |^ s)) / (s !) is V22() real ext-real Element of REAL
t . c is V22() real ext-real Element of REAL
- 1 is V22() real ext-real non positive integer non irrational Element of REAL
n is V22() real ext-real Element of REAL
f is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
dom f is V80() V81() V82() Element of K19(REAL)
x0 is set
x0 is V22() real ext-real Element of REAL
f . x0 is V22() real ext-real Element of REAL
n - x0 is V22() real ext-real Element of REAL
f /. x0 is V22() real ext-real Element of REAL
x0 is V22() real ext-real Element of REAL
f . x0 is V22() real ext-real Element of REAL
(- 1) * x0 is V22() real ext-real Element of REAL
((- 1) * x0) + n is V22() real ext-real Element of REAL
n - x0 is V22() real ext-real Element of REAL
x0 is V22() real ext-real Element of REAL
diff (f,x0) is V22() real ext-real Element of REAL
f `| (dom f) is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
(f `| (dom f)) . x0 is V22() real ext-real Element of REAL
x0 is V22() real ext-real Element of REAL
f . x0 is V22() real ext-real Element of REAL
n - x0 is V22() real ext-real Element of REAL
r is V22() real ext-real Element of REAL
x is V22() real ext-real Element of REAL
diff (f,x) is V22() real ext-real Element of REAL

n + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative integer non irrational V80() V81() V82() V83() V84() V85() V95() V97() Element of NAT

f is V22() real ext-real Element of REAL
x0 is V22() real ext-real Element of REAL
r is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
dom r is V80() V81() V82() Element of K19(REAL)
x is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
dom x is V80() V81() V82() Element of K19(REAL)
((n + 1)) is V1() V4( REAL ) V5( REAL ) Function-like non empty total quasi_total V33() V34() V35() Element of K19(K20(REAL,REAL))
dom ((n + 1)) is V80() V81() V82() Element of K19(REAL)
rng x is V80() V81() V82() Element of K19(REAL)
((n + 1)) * x is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
dom (((n + 1)) * x) is V80() V81() V82() Element of K19(REAL)
t is set
t is V22() real ext-real Element of REAL
r . t is V22() real ext-real Element of REAL
x0 - t is V22() real ext-real Element of REAL
(x0 - t) |^ (n + 1) is V22() real ext-real Element of REAL
f * ((x0 - t) |^ (n + 1)) is V22() real ext-real Element of REAL
(f * ((x0 - t) |^ (n + 1))) / ((n + 1) !) is V22() real ext-real Element of REAL
r /. t is V22() real ext-real Element of REAL
t is V22() real ext-real Element of REAL
f / ((n + 1) !) is V22() real ext-real Element of REAL
(f / ((n + 1) !)) (#) (((n + 1)) * x) is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
dom ((f / ((n + 1) !)) (#) (((n + 1)) * x)) is V80() V81() V82() Element of K19(REAL)
((f / ((n + 1) !)) (#) (((n + 1)) * x)) . t is V22() real ext-real Element of REAL
(((n + 1)) * x) . t is V22() real ext-real Element of REAL
(f / ((n + 1) !)) * ((((n + 1)) * x) . t) is V22() real ext-real Element of REAL
(((n + 1)) * x) /. t is V22() real ext-real Element of REAL
(f / ((n + 1) !)) * ((((n + 1)) * x) /. t) is V22() real ext-real Element of REAL
x /. t is V22() real ext-real Element of REAL
((n + 1)) /. (x /. t) is V22() real ext-real Element of REAL
((n + 1)) . (x /. t) is V22() real ext-real Element of REAL
(f / ((n + 1) !)) * (((n + 1)) /. (x /. t)) is V22() real ext-real Element of REAL
x . t is V22() real ext-real Element of REAL
((n + 1)) . (x . t) is V22() real ext-real Element of REAL
(f / ((n + 1) !)) * (((n + 1)) . (x . t)) is V22() real ext-real Element of REAL
(x . t) #Z (n + 1) is V22() real ext-real Element of REAL
(f / ((n + 1) !)) * ((x . t) #Z (n + 1)) is V22() real ext-real Element of REAL
(x . t) |^ (n + 1) is V22() real ext-real Element of REAL
(f / ((n + 1) !)) * ((x . t) |^ (n + 1)) is V22() real ext-real Element of REAL
x0 - t is V22() real ext-real Element of REAL
(x0 - t) |^ (n + 1) is V22() real ext-real Element of REAL
(f / ((n + 1) !)) * ((x0 - t) |^ (n + 1)) is V22() real ext-real Element of REAL
f * ((x0 - t) |^ (n + 1)) is V22() real ext-real Element of REAL
(f * ((x0 - t) |^ (n + 1))) / ((n + 1) !) is V22() real ext-real Element of REAL
r . t is V22() real ext-real Element of REAL
t is V22() real ext-real Element of REAL
diff ((((n + 1)) * x),t) is V22() real ext-real Element of REAL
x0 - t is V22() real ext-real Element of REAL
(x0 - t) #Z n is V22() real ext-real Element of REAL
(n + 1) * ((x0 - t) #Z n) is V22() real ext-real Element of REAL
- ((n + 1) * ((x0 - t) #Z n)) is V22() real ext-real Element of REAL
x . t is V22() real ext-real Element of REAL
diff (((n + 1)),(x . t)) is V22() real ext-real Element of REAL
(n + 1) - 1 is V22() real ext-real integer non irrational Element of REAL
(x . t) #Z ((n + 1) - 1) is V22() real ext-real Element of REAL
(n + 1) * ((x . t) #Z ((n + 1) - 1)) is V22() real ext-real Element of REAL
diff (x,t) is V22() real ext-real Element of REAL
((n + 1) * ((x . t) #Z ((n + 1) - 1))) * (diff (x,t)) is V22() real ext-real Element of REAL
((n + 1) * ((x . t) #Z ((n + 1) - 1))) * (- 1) is V22() real ext-real Element of REAL
(x0 - t) #Z ((n + 1) - 1) is V22() real ext-real Element of REAL
(n + 1) * ((x0 - t) #Z ((n + 1) - 1)) is V22() real ext-real Element of REAL
((n + 1) * ((x0 - t) #Z ((n + 1) - 1))) * (- 1) is V22() real ext-real Element of REAL
(n + 1) / ((n + 1) !) is V22() real ext-real non negative non irrational Element of REAL
1 * (n + 1) is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative integer non irrational V80() V81() V82() V83() V84() V85() V97() Element of NAT
(n !) * (n + 1) is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative integer non irrational V80() V81() V82() V83() V84() V85() V97() Element of NAT
(1 * (n + 1)) / ((n !) * (n + 1)) is V22() real ext-real non negative non irrational Element of REAL
1 / (n !) is V22() real ext-real non negative non irrational Element of REAL
t is V22() real ext-real Element of REAL
diff (((f / ((n + 1) !)) (#) (((n + 1)) * x)),t) is V22() real ext-real Element of REAL
diff ((((n + 1)) * x),t) is V22() real ext-real Element of REAL
(f / ((n + 1) !)) * (diff ((((n + 1)) * x),t)) is V22() real ext-real Element of REAL
(diff ((((n + 1)) * x),t)) / ((n + 1) !) is V22() real ext-real Element of REAL
((diff ((((n + 1)) * x),t)) / ((n + 1) !)) * f is V22() real ext-real Element of REAL
x0 - t is V22() real ext-real Element of REAL
(x0 - t) #Z n is V22() real ext-real Element of REAL
(n + 1) * ((x0 - t) #Z n) is V22() real ext-real Element of REAL
- ((n + 1) * ((x0 - t) #Z n)) is V22() real ext-real Element of REAL
(- ((n + 1) * ((x0 - t) #Z n))) / ((n + 1) !) is V22() real ext-real Element of REAL
f * ((- ((n + 1) * ((x0 - t)</