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

0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() real ext-real non positive non negative integer non irrational V80() V81() V82() V83() V84() V85() V86() V97() V100() 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 0 is V22() real ext-real Element of REAL

0 ! is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative integer non irrational Element of REAL

1 ! is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative integer non irrational Element of REAL

number_e is V22() real ext-real set

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

[#] REAL is closed open V80() V81() V82() Element of K19(REAL)

{} is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() real ext-real non positive non negative integer non irrational V80() V81() V82() V83() V84() V85() V86() V97() V100() set

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

n is V22() real ext-real integer non irrational 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

x0 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative integer non irrational set

f is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative integer non irrational set

x0 + f is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative integer non irrational 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

abs (x0 + f) is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative integer non irrational Element of REAL

0 |^ (abs (x0 + f)) is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative integer non irrational Element of REAL

0 |^ (x0 + f) is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative integer non irrational Element of REAL

0 |^ x0 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative integer non irrational Element of REAL

0 |^ f is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative integer non irrational Element of REAL

(0 |^ x0) * (0 |^ f) is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative integer non irrational Element of REAL

0 + 0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() real ext-real non positive non negative integer non irrational V80() V81() V82() V83() V84() V85() V86() V97() V100() Element of NAT

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

n #Z 0 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 f is V22() real ext-real Element of REAL

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

abs x0 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative integer non irrational Element of REAL

0 |^ (abs x0) is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative integer non irrational 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 * (0 |^ f) is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() real ext-real non positive non negative integer non irrational V80() V81() V82() V83() V84() V85() V86() V97() V100() Element of NAT

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 f is V22() real ext-real Element of REAL

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

abs f is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative integer non irrational Element of REAL

0 |^ (abs f) is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative integer non irrational 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

0 * (0 |^ x0) is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() real ext-real non positive non negative integer non irrational V80() V81() V82() V83() V84() V85() V86() V97() V100() Element of NAT

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

(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 epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative integer non irrational set

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

([#] REAL) /\ (dom (1)) is V80() V81() V82() Element of K19(REAL)

([#] 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

r 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

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

t #Z 0 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

c #Z 0 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 epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative integer non irrational set

(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

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

f is V22() real ext-real set

exp_R f is V22() real ext-real set

(exp_R f) #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

r is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative integer non irrational set

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

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

exp_R n is V22() real ext-real set

1 / (exp_R n) 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

(exp_R (- f)) * (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

n is V22() real ext-real integer non irrational set

f is V22() real ext-real set

exp_R f is V22() real ext-real set

(exp_R f) #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 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

- 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

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

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

n is V22() real ext-real integer non irrational set

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

f is V22() real ext-real set

exp_R f is V22() real ext-real set

(exp_R f) #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

1 / 0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() real ext-real non positive non negative integer non irrational V80() V81() V82() V83() V84() V85() V86() V97() V100() Element of REAL

(exp_R f) #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

exp_R n is V22() real ext-real set

f is V22() real ext-real integer non irrational set

x0 is V22() real ext-real integer non irrational set

f / x0 is V22() real ext-real non irrational Element of COMPLEX

(exp_R n) #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

(exp_R n) #R (1 / x0) is V22() real ext-real set

((exp_R n) #R (1 / x0)) #R f is V22() real ext-real set

(1 / x0) * f is V22() real ext-real non irrational Element of REAL

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

(f / x0) * 1 is V22() real ext-real non irrational Element of REAL

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

n is V22() real ext-real set

exp_R n is V22() real ext-real set

f is V22() real ext-real non irrational set

(exp_R n) #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

r 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

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

exp_R n is V22() real ext-real set

f is V22() real ext-real non irrational set

(exp_R n) #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

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

n is V22() real ext-real set

exp_R n is V22() real ext-real set

f is V22() real ext-real set

(exp_R n) #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

(exp_R n) #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 ((exp_R n) #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

((exp_R n) #Q x0) . r is V22() real ext-real Element of REAL

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

x0 . x is V22() real ext-real non irrational Element of REAL

(exp_R n) #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

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

n is V22() real ext-real set

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

exp_R n is V22() real ext-real set

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

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

number_e #R 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

(exp_R . 1) #R n is V22() real ext-real set

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

(exp_R . 1) to_power n is V22() real ext-real set

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

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

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

exp_R n is V22() real ext-real set

(exp_R 1) 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 |^ 0 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

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

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() V110() Element of NAT

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

(n GeoSeq) . 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

(n GeoSeq) . (0 + 1) is V22() real ext-real Element of REAL

((n GeoSeq) . 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 (1 rExpSeq) 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 integer non irrational set

(Partial_Sums (1 rExpSeq)) . n is V22() real ext-real Element of REAL

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

(Partial_Sums (1 rExpSeq)) . (n + 1) is V22() real ext-real Element of REAL

f 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

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

(Partial_Sums (1 rExpSeq)) . (f + 1) is V22() real ext-real Element of REAL

(Partial_Sums (1 rExpSeq)) . f is V22() real ext-real Element of REAL

(1 rExpSeq) . (f + 1) is V22() real ext-real Element of REAL

((Partial_Sums (1 rExpSeq)) . f) + ((1 rExpSeq) . (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

(f + 1) ! is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative integer non irrational Element of REAL

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

((Partial_Sums (1 rExpSeq)) . f) + ((1 |^ (f + 1)) / ((f + 1) !)) is V22() real ext-real Element of REAL

(Partial_Sums (1 rExpSeq)) . 1 is V22() real ext-real Element of REAL

(Partial_Sums (1 rExpSeq)) . 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

(1 rExpSeq) . (0 + 1) is V22() real ext-real Element of REAL

((Partial_Sums (1 rExpSeq)) . 0) + ((1 rExpSeq) . (0 + 1)) is V22() real ext-real Element of REAL

(1 rExpSeq) . 0 is V22() real ext-real Element of REAL

(1 rExpSeq) . 1 is V22() real ext-real Element of REAL

((1 rExpSeq) . 0) + ((1 rExpSeq) . 1) is V22() real ext-real Element of REAL

1 |^ 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 |^ 1) / (1 !) is V22() real ext-real non negative non irrational Element of REAL

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

1 |^ 0 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 |^ 0) / (0 !) is V22() real ext-real non negative non irrational Element of REAL

((1 |^ 0) / (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 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

(Partial_Sums (1 rExpSeq)) . n is V22() real ext-real Element of REAL

(Partial_Sums (1 rExpSeq)) ^\ 1 is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))

n 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

((Partial_Sums (1 rExpSeq)) ^\ 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

(Partial_Sums (1 rExpSeq)) . (n + 1) is V22() real ext-real Element of REAL

lim (Partial_Sums (1 rExpSeq)) is V22() real ext-real Element of REAL

Sum (1 rExpSeq) is V22() real ext-real Element of REAL

lim ((Partial_Sums (1 rExpSeq)) ^\ 1) is V22() real ext-real Element of REAL

n is V22() real ext-real set

exp_R n is V22() real ext-real set

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

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

n is V22() real ext-real set

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

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

exp_R n is V22() real ext-real set

log (number_e,(exp_R 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 set

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

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

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

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

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

log (number_e,(exp_R . r)) 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

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

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

n is set

f is set

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

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

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

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

{ b

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 (exp_R ") is V80() V81() V82() Element of K19(REAL)

n is V22() real ext-real set

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

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

(exp_R ") . n is V22() real ext-real Element of REAL

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

exp_R . ((exp_R ") . n) is V22() real ext-real Element of REAL

{ b

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

r is V22() real ext-real Element of right_open_halfline 0

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

(exp_R ") . 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

{ b

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

{ b

n is V22() real ext-real Element of right_open_halfline 0

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

{ b

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

f is V22() real ext-real Element of right_open_halfline 0

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

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

x0 is V22() real ext-real Element of right_open_halfline 0

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 ((exp_R * f),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

{ b

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

r is V22() real ext-real Element of right_open_halfline 0

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

{ b

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

r to_power f is V22() real ext-real set

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

{ b

(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

r to_power f is V22() real ext-real set

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,(PFuncs (REAL,REAL))) is set

K19(K20(NAT,(PFuncs (REAL,REAL)))) 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))

r 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

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,(PFuncs (REAL,REAL))))

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,(PFuncs (REAL,REAL))))

x . 0 is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))

t is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative integer non irrational set

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,(PFuncs (REAL,REAL))))

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,(PFuncs (REAL,REAL))))

r . 0 is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))

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

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)

x0 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative integer non irrational set

r is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative integer non irrational set

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

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

(n,f) is V1() V4( NAT ) V5( PFuncs (REAL,REAL)) Function-like non empty total quasi_total Element of K19(K20(NAT,(PFuncs (REAL,REAL))))

(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,(PFuncs (REAL,REAL))))

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

t is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative integer non irrational set

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

t ! is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative integer non irrational 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

s 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,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

s ! is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative integer non irrational 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 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 + 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 non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative integer non irrational Element of REAL

n ! is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative integer non irrational Element of REAL

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