:: 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₁ where b₁ is V22() real ext-real Element of REAL : not b₁ <= 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 (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₁ where b₁ is V22() real ext-real Element of REAL : not b₁ <= 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
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₁ where b₁ is V22() real ext-real Element of REAL : not b₁ <= 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
{ b₁ where b₁ is V22() real ext-real Element of REAL : not b₁ <= 0 } is set
n is V22() real ext-real Element of right_open_halfline 0
diff ((),n) is V22() real ext-real Element of REAL
{ b₁ where b₁ is V22() real ext-real Element of REAL : not b₁ <= 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
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₁ where b₁ is V22() real ext-real Element of REAL : not b₁ <= 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
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₁ where b₁ is V22() real ext-real Element of REAL : not b₁ <= 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
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₁ where b₁ is V22() real ext-real Element of REAL : not b₁ <= 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
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) #Z n))) / ((n + 1) !)) is V22() real ext-real Element of REAL
(x0 - t) |^ n is V22() real ext-real Element of REAL
(n + 1) * ((x0 - t) |^ n) is V22() real ext-real Element of REAL
- ((n + 1) * ((x0 - t) |^ n)) is V22() real ext-real Element of REAL
(- ((n + 1) * ((x0 - t) |^ n))) / ((n + 1) !) is V22() real ext-real Element of REAL
f * ((- ((n + 1) * ((x0 - t) |^ n))) / ((n + 1) !)) is V22() real ext-real Element of REAL
f * (- ((n + 1) * ((x0 - t) |^ n))) is V22() real ext-real Element of REAL
(f * (- ((n + 1) * ((x0 - t) |^ n)))) / ((n + 1) !) is V22() real ext-real Element of REAL
- f is V22() real ext-real Element of REAL
(- f) * ((n + 1) * ((x0 - t) |^ n)) is V22() real ext-real Element of REAL
((- f) * ((n + 1) * ((x0 - t) |^ n))) / ((n + 1) !) is V22() real ext-real Element of REAL
((n + 1) * ((x0 - t) |^ n)) / ((n + 1) !) is V22() real ext-real Element of REAL
(- f) * (((n + 1) * ((x0 - t) |^ n)) / ((n + 1) !)) is V22() real ext-real Element of REAL
((x0 - t) |^ n) * ((n + 1) / ((n + 1) !)) is V22() real ext-real Element of REAL
(- f) * (((x0 - t) |^ n) * ((n + 1) / ((n + 1) !))) is V22() real ext-real Element of REAL
((x0 - t) |^ n) / (n !) is V22() real ext-real Element of REAL
(- f) * (((x0 - t) |^ n) / (n !)) is V22() real ext-real Element of REAL
f * (((x0 - t) |^ n) / (n !)) is V22() real ext-real Element of REAL
- (f * (((x0 - t) |^ n) / (n !))) is V22() real ext-real Element of REAL
f * ((x0 - t) |^ n) is V22() real ext-real Element of REAL
(f * ((x0 - t) |^ n)) / (n !) is V22() real ext-real Element of REAL
- ((f * ((x0 - t) |^ n)) / (n !)) is V22() real ext-real Element of REAL
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
c is V22() real ext-real Element of REAL
s is V22() real ext-real Element of REAL
diff (r,s) is V22() real ext-real Element of REAL
x0 - s is V22() real ext-real Element of REAL
(x0 - s) |^ n is V22() real ext-real Element of REAL
f * ((x0 - s) |^ n) is V22() real ext-real Element of REAL
(f * ((x0 - s) |^ n)) / (n !) is V22() real ext-real Element of REAL
- ((f * ((x0 - s) |^ n)) / (n !)) 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
f is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
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
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)
t is set
t is set
t is V22() real ext-real Element of REAL
x . t is V22() real ext-real Element of REAL
(f,x0,t,r) is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
Partial_Sums (f,x0,t,r) is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
(Partial_Sums (f,x0,t,r)) . n is V22() real ext-real Element of REAL
(f . r) - ((Partial_Sums (f,x0,t,r)) . n) is V22() real ext-real Element of REAL
x /. t is V22() real ext-real Element of REAL
t is V22() real ext-real Element of REAL
x . t is V22() real ext-real Element of REAL
(f,x0,t,r) is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
Partial_Sums (f,x0,t,r) is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
(Partial_Sums (f,x0,t,r)) . n is V22() real ext-real Element of REAL
(f . r) - ((Partial_Sums (f,x0,t,r)) . n) is V22() real ext-real Element of 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 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) . x0 is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,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
(n,f) . (x0 + 1) is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
x is V22() real ext-real Element of REAL
r is V22() real ext-real Element of REAL
].r,x.[ is open V80() V81() V82() V95() V96() V100() Element of K19(REAL)
((n,f) . (x0 + 1)) | ].r,x.[ is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
(n,].r,x.[) is V1() V4( NAT ) V5( PFuncs (REAL,REAL)) Function-like non empty total quasi_total Element of K19(K20(NAT,(PFuncs (REAL,REAL))))
(n,].r,x.[) . (x0 + 1) is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
(x0 + 1) - 1 is V22() real ext-real integer non irrational Element of REAL
((n,f) . x0) `| ].r,x.[ is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
dom (((n,f) . x0) `| ].r,x.[) is V80() V81() V82() Element of K19(REAL)
((n,f) . x0) `| f is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
(((n,f) . x0) `| f) | ].r,x.[ is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
dom ((((n,f) . x0) `| f) | ].r,x.[) is V80() V81() V82() Element of K19(REAL)
dom (((n,f) . x0) `| f) is V80() V81() V82() Element of K19(REAL)
(dom (((n,f) . x0) `| f)) /\ ].r,x.[ is V80() V81() V82() Element of K19(REAL)
f /\ ].r,x.[ is V80() V81() V82() Element of K19(REAL)
t is V22() real ext-real Element of REAL
((((n,f) . x0) `| f) | ].r,x.[) . t is V22() real ext-real Element of REAL
(((n,f) . x0) `| f) . t is V22() real ext-real Element of REAL
diff (((n,f) . x0),t) is V22() real ext-real Element of REAL
(((n,f) . x0) `| ].r,x.[) . t is V22() real ext-real Element of REAL
((n,f) . x0) | ].r,x.[ is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
(((n,f) . x0) | ].r,x.[) `| ].r,x.[ is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
(n,].r,x.[) . x0 is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
((n,].r,x.[) . x0) `| ].r,x.[ is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
(n,f) . 0 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
x0 is V22() real ext-real Element of REAL
].x0,r.[ is open V80() V81() V82() V95() V96() V100() Element of K19(REAL)
((n,f) . 0) | ].x0,r.[ is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
(n,].x0,r.[) is V1() V4( NAT ) V5( PFuncs (REAL,REAL)) Function-like non empty total quasi_total Element of K19(K20(NAT,(PFuncs (REAL,REAL))))
(n,].x0,r.[) . 0 is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
n | f is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
(n | f) | ].x0,r.[ is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
n | ].x0,r.[ 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))
dom n is V80() V81() V82() Element of K19(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))))
(n,f) . 0 is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,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
r is V22() real ext-real Element of REAL
x0 is V22() real ext-real Element of REAL
[.x0,r.] is closed V80() V81() V82() V100() Element of K19(REAL)
((n,f) . 0) | [.x0,r.] is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
].x0,r.[ is open V80() V81() V82() V95() V96() V100() Element of K19(REAL)
n . r is V22() real ext-real Element of REAL
(n,].x0,r.[) is V1() V4( NAT ) V5( PFuncs (REAL,REAL)) Function-like non empty total quasi_total Element of K19(K20(NAT,(PFuncs (REAL,REAL))))
(n,].x0,r.[) . (0 + 1) is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,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)
x . r is V22() real ext-real Element of REAL
x | [.x0,r.] is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
(n,f,r,r) is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
Partial_Sums (n,f,r,r) is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
(Partial_Sums (n,f,r,r)) . 0 is V22() real ext-real Element of REAL
(n . r) - ((Partial_Sums (n,f,r,r)) . 0) is V22() real ext-real Element of REAL
(n,f,r,r) . 0 is V22() real ext-real Element of REAL
(n . r) - ((n,f,r,r) . 0) is V22() real ext-real Element of REAL
((n,f) . 0) . r is V22() real ext-real Element of REAL
r - r is V22() real ext-real Element of REAL
(r - r) |^ 0 is V22() real ext-real Element of REAL
(((n,f) . 0) . r) * ((r - r) |^ 0) is V22() real ext-real Element of REAL
((((n,f) . 0) . r) * ((r - r) |^ 0)) / (0 !) is V22() real ext-real Element of REAL
(n . r) - (((((n,f) . 0) . r) * ((r - r) |^ 0)) / (0 !)) is V22() real ext-real Element of REAL
n | f is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
(n | f) . r is V22() real ext-real Element of REAL
((n | f) . r) * ((r - r) |^ 0) is V22() real ext-real Element of REAL
(((n | f) . r) * ((r - r) |^ 0)) / (0 !) is V22() real ext-real Element of REAL
(n . r) - ((((n | f) . r) * ((r - r) |^ 0)) / (0 !)) is V22() real ext-real Element of REAL
(n . r) * ((r - r) |^ 0) is V22() real ext-real Element of REAL
((n . r) * ((r - r) |^ 0)) / (0 !) is V22() real ext-real Element of REAL
(n . r) - (((n . r) * ((r - r) |^ 0)) / (0 !)) is V22() real ext-real Element of REAL
(n . r) * 1 is V22() real ext-real Element of REAL
(n . r) - ((n . r) * 1) is V22() real ext-real Element of REAL
t is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
dom t is V80() V81() V82() Element of K19(REAL)
rng n is V80() V81() V82() Element of K19(REAL)
t * n is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
dom (t * n) is V80() V81() V82() Element of K19(REAL)
c is V22() real ext-real Element of REAL
t | REAL is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
n .: [.x0,r.] is V80() V81() V82() Element of K19(REAL)
t | (n .: [.x0,r.]) is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
(0 + 1) - 1 is V22() real ext-real integer non irrational Element of REAL
(n,].x0,r.[) . 0 is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
n | ].x0,r.[ is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
c is V22() real ext-real Element of REAL
((n,].x0,r.[) . 0) `| ].x0,r.[ is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
(n | ].x0,r.[) `| ].x0,r.[ is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
n `| ].x0,r.[ is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
c is V22() real ext-real Element of REAL
diff ((t * n),c) is V22() real ext-real Element of REAL
((n,].x0,r.[) . (0 + 1)) . c is V22() real ext-real Element of REAL
r - c is V22() real ext-real Element of REAL
(r - c) |^ 0 is V22() real ext-real Element of REAL
(((n,].x0,r.[) . (0 + 1)) . c) * ((r - c) |^ 0) is V22() real ext-real Element of REAL
((((n,].x0,r.[) . (0 + 1)) . c) * ((r - c) |^ 0)) / (0 !) is V22() real ext-real Element of REAL
- (((((n,].x0,r.[) . (0 + 1)) . c) * ((r - c) |^ 0)) / (0 !)) is V22() real ext-real Element of REAL
n . c is V22() real ext-real Element of REAL
((r - c) |^ 0) / (0 !) is V22() real ext-real Element of REAL
diff (t,(n . c)) is V22() real ext-real Element of REAL
diff (n,c) is V22() real ext-real Element of REAL
(diff (t,(n . c))) * (diff (n,c)) is V22() real ext-real Element of REAL
(n `| ].x0,r.[) . c is V22() real ext-real Element of REAL
(diff (t,(n . c))) * ((n `| ].x0,r.[) . c) is V22() real ext-real Element of REAL
(- 1) * (((n,].x0,r.[) . (0 + 1)) . c) is V22() real ext-real Element of REAL
(((n,].x0,r.[) . (0 + 1)) . c) * (((r - c) |^ 0) / (0 !)) is V22() real ext-real Element of REAL
- ((((n,].x0,r.[) . (0 + 1)) . c) * (((r - c) |^ 0) / (0 !))) is V22() real ext-real Element of REAL
c is V22() real ext-real Element of REAL
(t * n) | [.x0,r.] is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
dom ((t * n) | [.x0,r.]) is V80() V81() V82() Element of K19(REAL)
(dom (t * n)) /\ [.x0,r.] is V80() V81() V82() Element of K19(REAL)
f /\ [.x0,r.] is V80() V81() V82() Element of K19(REAL)
dom (x | [.x0,r.]) is V80() V81() V82() Element of K19(REAL)
c is set
(dom x) /\ [.x0,r.] is V80() V81() V82() Element of K19(REAL)
s is V22() real ext-real Element of REAL
r - s is V22() real ext-real Element of REAL
(r - s) |^ 0 is V22() real ext-real Element of REAL
((r - s) |^ 0) / (0 !) is V22() real ext-real Element of REAL
(x | [.x0,r.]) . c is V22() real ext-real Element of REAL
x . s is V22() real ext-real Element of REAL
(n,f,s,r) is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
Partial_Sums (n,f,s,r) is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
(Partial_Sums (n,f,s,r)) . 0 is V22() real ext-real Element of REAL
(n . r) - ((Partial_Sums (n,f,s,r)) . 0) is V22() real ext-real Element of REAL
(n,f,s,r) . 0 is V22() real ext-real Element of REAL
(n . r) - ((n,f,s,r) . 0) is V22() real ext-real Element of REAL
((n,f) . 0) . s is V22() real ext-real Element of REAL
(((n,f) . 0) . s) * ((r - s) |^ 0) is V22() real ext-real Element of REAL
((((n,f) . 0) . s) * ((r - s) |^ 0)) / (0 !) is V22() real ext-real Element of REAL
(n . r) - (((((n,f) . 0) . s) * ((r - s) |^ 0)) / (0 !)) is V22() real ext-real Element of REAL
(n | f) . s is V22() real ext-real Element of REAL
((n | f) . s) * ((r - s) |^ 0) is V22() real ext-real Element of REAL
(((n | f) . s) * ((r - s) |^ 0)) / (0 !) is V22() real ext-real Element of REAL
(n . r) - ((((n | f) . s) * ((r - s) |^ 0)) / (0 !)) is V22() real ext-real Element of REAL
n . s is V22() real ext-real Element of REAL
(n . s) * ((r - s) |^ 0) is V22() real ext-real Element of REAL
((n . s) * ((r - s) |^ 0)) / (0 !) is V22() real ext-real Element of REAL
(n . r) - (((n . s) * ((r - s) |^ 0)) / (0 !)) is V22() real ext-real Element of REAL
(n . s) * (((r - s) |^ 0) / (0 !)) is V22() real ext-real Element of REAL
(n . r) - ((n . s) * (((r - s) |^ 0) / (0 !))) is V22() real ext-real Element of REAL
t . (n . s) is V22() real ext-real Element of REAL
(t * n) . s is V22() real ext-real Element of REAL
((t * n) | [.x0,r.]) . c is V22() real ext-real Element of REAL
(n | f) | [.x0,r.] is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
((n | f) | [.x0,r.]) | [.x0,r.] is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
n | [.x0,r.] is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
(n | [.x0,r.]) | [.x0,r.] is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
(t * n) | ].x0,r.[ is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
dom ((t * n) | ].x0,r.[) is V80() V81() V82() Element of K19(REAL)
(dom (t * n)) /\ ].x0,r.[ is V80() V81() V82() Element of K19(REAL)
f /\ ].x0,r.[ is V80() V81() V82() Element of K19(REAL)
x | ].x0,r.[ is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
dom (x | ].x0,r.[) is V80() V81() V82() Element of K19(REAL)
c is set
(dom x) /\ ].x0,r.[ is V80() V81() V82() Element of K19(REAL)
s is V22() real ext-real Element of REAL
r - s is V22() real ext-real Element of REAL
(r - s) |^ 0 is V22() real ext-real Element of REAL
((r - s) |^ 0) / (0 !) is V22() real ext-real Element of REAL
(x | ].x0,r.[) . c is V22() real ext-real Element of REAL
x . s is V22() real ext-real Element of REAL
(n,f,s,r) is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
Partial_Sums (n,f,s,r) is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
(Partial_Sums (n,f,s,r)) . 0 is V22() real ext-real Element of REAL
(n . r) - ((Partial_Sums (n,f,s,r)) . 0) is V22() real ext-real Element of REAL
(n,f,s,r) . 0 is V22() real ext-real Element of REAL
(n . r) - ((n,f,s,r) . 0) is V22() real ext-real Element of REAL
((n,f) . 0) . s is V22() real ext-real Element of REAL
(((n,f) . 0) . s) * ((r - s) |^ 0) is V22() real ext-real Element of REAL
((((n,f) . 0) . s) * ((r - s) |^ 0)) / (0 !) is V22() real ext-real Element of REAL
(n . r) - (((((n,f) . 0) . s) * ((r - s) |^ 0)) / (0 !)) is V22() real ext-real Element of REAL
(n | f) . s is V22() real ext-real Element of REAL
((n | f) . s) * ((r - s) |^ 0) is V22() real ext-real Element of REAL
(((n | f) . s) * ((r - s) |^ 0)) / (0 !) is V22() real ext-real Element of REAL
(n . r) - ((((n | f) . s) * ((r - s) |^ 0)) / (0 !)) is V22() real ext-real Element of REAL
n . s is V22() real ext-real Element of REAL
(n . s) * ((r - s) |^ 0) is V22() real ext-real Element of REAL
((n . s) * ((r - s) |^ 0)) / (0 !) is V22() real ext-real Element of REAL
(n . r) - (((n . s) * ((r - s) |^ 0)) / (0 !)) is V22() real ext-real Element of REAL
(n . s) * (((r - s) |^ 0) / (0 !)) is V22() real ext-real Element of REAL
(n . r) - ((n . s) * (((r - s) |^ 0) / (0 !))) is V22() real ext-real Element of REAL
t . (n . s) is V22() real ext-real Element of REAL
(t * n) . s is V22() real ext-real Element of REAL
((t * n) | ].x0,r.[) . c is V22() real ext-real Element of REAL
c is V22() real ext-real Element of REAL
c is V22() real ext-real Element of REAL
diff (x,c) is V22() real ext-real Element of REAL
x `| ].x0,r.[ is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
(x `| ].x0,r.[) . c is V22() real ext-real Element of REAL
(x | ].x0,r.[) `| ].x0,r.[ is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
((x | ].x0,r.[) `| ].x0,r.[) . c is V22() real ext-real Element of REAL
(t * n) `| ].x0,r.[ is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
((t * n) `| ].x0,r.[) . c is V22() real ext-real Element of REAL
diff ((t * n),c) is V22() real ext-real Element of REAL
((n,].x0,r.[) . (0 + 1)) . c is V22() real ext-real Element of REAL
r - c is V22() real ext-real Element of REAL
(r - c) |^ 0 is V22() real ext-real Element of REAL
(((n,].x0,r.[) . (0 + 1)) . c) * ((r - c) |^ 0) is V22() real ext-real Element of REAL
((((n,].x0,r.[) . (0 + 1)) . c) * ((r - c) |^ 0)) / (0 !) is V22() real ext-real Element of REAL
- (((((n,].x0,r.[) . (0 + 1)) . c) * ((r - c) |^ 0)) / (0 !)) is V22() real ext-real Element of REAL
c is V22() real ext-real Element of REAL
diff (x,c) is V22() real ext-real Element of REAL
((n,].x0,r.[) . (0 + 1)) . c is V22() real ext-real Element of REAL
r - c is V22() real ext-real Element of REAL
(r - c) |^ 0 is V22() real ext-real Element of REAL
(((n,].x0,r.[) . (0 + 1)) . c) * ((r - c) |^ 0) is V22() real ext-real Element of REAL
((((n,].x0,r.[) . (0 + 1)) . c) * ((r - c) |^ 0)) / (0 !) is V22() real ext-real Element of REAL
- (((((n,].x0,r.[) . (0 + 1)) . c) * ((r - c) |^ 0)) / (0 !)) 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 V80() V81() V82() V83() V84() V85() V97() Element of NAT
(n,f) . x0 is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,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 ! is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative integer non irrational Element of REAL
(n,f) . (x0 + 1) is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
(x0 + 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
(x0 + 1) ! is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative integer non irrational Element of REAL
x is V22() real ext-real Element of REAL
r is V22() real ext-real Element of REAL
[.r,x.] is closed V80() V81() V82() V100() Element of K19(REAL)
((n,f) . (x0 + 1)) | [.r,x.] is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
].r,x.[ is open V80() V81() V82() V95() V96() V100() Element of K19(REAL)
n . x is V22() real ext-real Element of REAL
(n,].r,x.[) is V1() V4( NAT ) V5( PFuncs (REAL,REAL)) Function-like non empty total quasi_total Element of K19(K20(NAT,(PFuncs (REAL,REAL))))
(n,].r,x.[) . ((x0 + 1) + 1) is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
(x0 + 1) - 1 is V22() real ext-real integer non irrational Element of REAL
((n,f) . x0) | f is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
((n,f) . x0) | [.r,x.] is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
t is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
dom t is V80() V81() V82() Element of K19(REAL)
t | [.r,x.] is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
((x0 + 1) + 1) - 1 is V22() real ext-real integer non irrational Element of REAL
(n,].r,x.[) . x0 is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
((n,f) . x0) `| 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))
dom c is V80() V81() V82() Element of K19(REAL)
c . x is V22() real ext-real Element of REAL
(n,f,x,x) is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
Partial_Sums (n,f,x,x) is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
(Partial_Sums (n,f,x,x)) . (x0 + 1) is V22() real ext-real Element of REAL
(n . x) - ((Partial_Sums (n,f,x,x)) . (x0 + 1)) is V22() real ext-real Element of REAL
(Partial_Sums (n,f,x,x)) . x0 is V22() real ext-real Element of REAL
(n,f,x,x) . (x0 + 1) is V22() real ext-real Element of REAL
((Partial_Sums (n,f,x,x)) . x0) + ((n,f,x,x) . (x0 + 1)) is V22() real ext-real Element of REAL
(n . x) - (((Partial_Sums (n,f,x,x)) . x0) + ((n,f,x,x) . (x0 + 1))) is V22() real ext-real Element of REAL
(n . x) - ((Partial_Sums (n,f,x,x)) . x0) is V22() real ext-real Element of REAL
((n . x) - ((Partial_Sums (n,f,x,x)) . x0)) - ((n,f,x,x) . (x0 + 1)) is V22() real ext-real Element of REAL
t . x is V22() real ext-real Element of REAL
(t . x) - ((n,f,x,x) . (x0 + 1)) is V22() real ext-real Element of REAL
0 - ((n,f,x,x) . (x0 + 1)) is V22() real ext-real Element of REAL
((n,f) . (x0 + 1)) . x is V22() real ext-real Element of REAL
x - x is V22() real ext-real Element of REAL
(x - x) |^ (x0 + 1) is V22() real ext-real Element of REAL
(((n,f) . (x0 + 1)) . x) * ((x - x) |^ (x0 + 1)) is V22() real ext-real Element of REAL
((((n,f) . (x0 + 1)) . x) * ((x - x) |^ (x0 + 1))) / ((x0 + 1) !) is V22() real ext-real Element of REAL
0 - (((((n,f) . (x0 + 1)) . x) * ((x - x) |^ (x0 + 1))) / ((x0 + 1) !)) is V22() real ext-real Element of REAL
0 |^ 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
(0 |^ x0) * 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,f) . (x0 + 1)) . x) * ((0 |^ x0) * 0) is V22() real ext-real Element of REAL
((((n,f) . (x0 + 1)) . x) * ((0 |^ x0) * 0)) / ((x0 + 1) !) is V22() real ext-real Element of REAL
0 - (((((n,f) . (x0 + 1)) . x) * ((0 |^ x0) * 0)) / ((x0 + 1) !)) is V22() real ext-real Element of REAL
s is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
dom s is V80() V81() V82() Element of K19(REAL)
((n,f) . (x0 + 1)) (#) s is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
dom (((n,f) . (x0 + 1)) (#) s) is V80() V81() V82() Element of K19(REAL)
dom ((n,f) . (x0 + 1)) is V80() V81() V82() Element of K19(REAL)
(dom ((n,f) . (x0 + 1))) /\ (dom s) is V80() V81() V82() Element of K19(REAL)
f /\ REAL is V80() V81() V82() Element of K19(REAL)
t - (((n,f) . (x0 + 1)) (#) s) is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
dom (t - (((n,f) . (x0 + 1)) (#) s)) is V80() V81() V82() Element of K19(REAL)
(dom t) /\ (dom (((n,f) . (x0 + 1)) (#) s)) is V80() V81() V82() Element of K19(REAL)
c | [.r,x.] is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
hp is V22() real ext-real Element of REAL
s | REAL is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
s | [.r,x.] is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
hp is V22() real ext-real Element of REAL
c . hp is V22() real ext-real Element of REAL
(n,f,hp,x) is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
Partial_Sums (n,f,hp,x) is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
(Partial_Sums (n,f,hp,x)) . (x0 + 1) is V22() real ext-real Element of REAL
(n . x) - ((Partial_Sums (n,f,hp,x)) . (x0 + 1)) is V22() real ext-real Element of REAL
(Partial_Sums (n,f,hp,x)) . x0 is V22() real ext-real Element of REAL
(n,f,hp,x) . (x0 + 1) is V22() real ext-real Element of REAL
((Partial_Sums (n,f,hp,x)) . x0) + ((n,f,hp,x) . (x0 + 1)) is V22() real ext-real Element of REAL
(n . x) - (((Partial_Sums (n,f,hp,x)) . x0) + ((n,f,hp,x) . (x0 + 1))) is V22() real ext-real Element of REAL
(n . x) - ((Partial_Sums (n,f,hp,x)) . x0) is V22() real ext-real Element of REAL
((n . x) - ((Partial_Sums (n,f,hp,x)) . x0)) - ((n,f,hp,x) . (x0 + 1)) is V22() real ext-real Element of REAL
t . hp is V22() real ext-real Element of REAL
(t . hp) - ((n,f,hp,x) . (x0 + 1)) is V22() real ext-real Element of REAL
((n,f) . (x0 + 1)) . hp is V22() real ext-real Element of REAL
x - hp is V22() real ext-real Element of REAL
(x - hp) |^ (x0 + 1) is V22() real ext-real Element of REAL
(((n,f) . (x0 + 1)) . hp) * ((x - hp) |^ (x0 + 1)) is V22() real ext-real Element of REAL
((((n,f) . (x0 + 1)) . hp) * ((x - hp) |^ (x0 + 1))) / ((x0 + 1) !) is V22() real ext-real Element of REAL
(t . hp) - (((((n,f) . (x0 + 1)) . hp) * ((x - hp) |^ (x0 + 1))) / ((x0 + 1) !)) is V22() real ext-real Element of REAL
1 * ((x - hp) |^ (x0 + 1)) is V22() real ext-real Element of REAL
(1 * ((x - hp) |^ (x0 + 1))) / ((x0 + 1) !) is V22() real ext-real Element of REAL
(((n,f) . (x0 + 1)) . hp) * ((1 * ((x - hp) |^ (x0 + 1))) / ((x0 + 1) !)) is V22() real ext-real Element of REAL
(t . hp) - ((((n,f) . (x0 + 1)) . hp) * ((1 * ((x - hp) |^ (x0 + 1))) / ((x0 + 1) !))) is V22() real ext-real Element of REAL
s . hp is V22() real ext-real Element of REAL
(((n,f) . (x0 + 1)) . hp) * (s . hp) is V22() real ext-real Element of REAL
(t . hp) - ((((n,f) . (x0 + 1)) . hp) * (s . hp)) is V22() real ext-real Element of REAL
(((n,f) . (x0 + 1)) (#) s) . hp is V22() real ext-real Element of REAL
(t . hp) - ((((n,f) . (x0 + 1)) (#) s) . hp) is V22() real ext-real Element of REAL
(t - (((n,f) . (x0 + 1)) (#) s)) . hp is V22() real ext-real Element of REAL
[.r,x.] /\ [.r,x.] is V80() V81() V82() V100() Element of K19(REAL)
(((n,f) . (x0 + 1)) (#) s) | ([.r,x.] /\ [.r,x.]) is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
(n,].r,x.[) . (x0 + 1) is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
((n,].r,x.[) . x0) `| ].r,x.[ is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
((n,].r,x.[) . (x0 + 1)) (#) s is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
t - (((n,].r,x.[) . (x0 + 1)) (#) s) is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
dom (((n,].r,x.[) . (x0 + 1)) (#) s) is V80() V81() V82() Element of K19(REAL)
dom ((n,].r,x.[) . (x0 + 1)) is V80() V81() V82() Element of K19(REAL)
(dom ((n,].r,x.[) . (x0 + 1))) /\ (dom s) is V80() V81() V82() Element of K19(REAL)
].r,x.[ /\ REAL is V80() V81() V82() V100() Element of K19(REAL)
dom (t - (((n,].r,x.[) . (x0 + 1)) (#) s)) is V80() V81() V82() Element of K19(REAL)
f /\ ].r,x.[ is V80() V81() V82() Element of K19(REAL)
hp is V22() real ext-real Element of REAL
(t - (((n,f) . (x0 + 1)) (#) s)) . hp is V22() real ext-real Element of REAL
(t - (((n,].r,x.[) . (x0 + 1)) (#) s)) . hp is V22() real ext-real Element of REAL
t . hp is V22() real ext-real Element of REAL
(((n,].r,x.[) . (x0 + 1)) (#) s) . hp is V22() real ext-real Element of REAL
(t . hp) - ((((n,].r,x.[) . (x0 + 1)) (#) s) . hp) is V22() real ext-real Element of REAL
((n,].r,x.[) . (x0 + 1)) . hp is V22() real ext-real Element of REAL
s . hp is V22() real ext-real Element of REAL
(((n,].r,x.[) . (x0 + 1)) . hp) * (s . hp) is V22() real ext-real Element of REAL
(t . hp) - ((((n,].r,x.[) . (x0 + 1)) . hp) * (s . hp)) is V22() real ext-real Element of REAL
((n,f) . (x0 + 1)) | ].r,x.[ is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
(((n,f) . (x0 + 1)) | ].r,x.[) . hp is V22() real ext-real Element of REAL
((((n,f) . (x0 + 1)) | ].r,x.[) . hp) * (s . hp) is V22() real ext-real Element of REAL
(t . hp) - (((((n,f) . (x0 + 1)) | ].r,x.[) . hp) * (s . hp)) is V22() real ext-real Element of REAL
((n,f) . (x0 + 1)) . hp is V22() real ext-real Element of REAL
(((n,f) . (x0 + 1)) . hp) * (s . hp) is V22() real ext-real Element of REAL
(t . hp) - ((((n,f) . (x0 + 1)) . hp) * (s . hp)) is V22() real ext-real Element of REAL
(((n,f) . (x0 + 1)) (#) s) . hp is V22() real ext-real Element of REAL
(t . hp) - ((((n,f) . (x0 + 1)) (#) s) . hp) is V22() real ext-real Element of REAL
hp is set
c . hp is V22() real ext-real Element of REAL
x is V22() real ext-real Element of REAL
(n,f,x,x) is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
Partial_Sums (n,f,x,x) is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
(Partial_Sums (n,f,x,x)) . (x0 + 1) is V22() real ext-real Element of REAL
(n . x) - ((Partial_Sums (n,f,x,x)) . (x0 + 1)) is V22() real ext-real Element of REAL
(Partial_Sums (n,f,x,x)) . x0 is V22() real ext-real Element of REAL
(n,f,x,x) . (x0 + 1) is V22() real ext-real Element of REAL
((Partial_Sums (n,f,x,x)) . x0) + ((n,f,x,x) . (x0 + 1)) is V22() real ext-real Element of REAL
(n . x) - (((Partial_Sums (n,f,x,x)) . x0) + ((n,f,x,x) . (x0 + 1))) is V22() real ext-real Element of REAL
(n . x) - ((Partial_Sums (n,f,x,x)) . x0) is V22() real ext-real Element of REAL
((n . x) - ((Partial_Sums (n,f,x,x)) . x0)) - ((n,f,x,x) . (x0 + 1)) is V22() real ext-real Element of REAL
t . x is V22() real ext-real Element of REAL
(t . x) - ((n,f,x,x) . (x0 + 1)) is V22() real ext-real Element of REAL
((n,f) . (x0 + 1)) . x is V22() real ext-real Element of REAL
x - x is V22() real ext-real Element of REAL
(x - x) |^ (x0 + 1) is V22() real ext-real Element of REAL
(((n,f) . (x0 + 1)) . x) * ((x - x) |^ (x0 + 1)) is V22() real ext-real Element of REAL
((((n,f) . (x0 + 1)) . x) * ((x - x) |^ (x0 + 1))) / ((x0 + 1) !) is V22() real ext-real Element of REAL
(t . x) - (((((n,f) . (x0 + 1)) . x) * ((x - x) |^ (x0 + 1))) / ((x0 + 1) !)) is V22() real ext-real Element of REAL
1 * ((x - x) |^ (x0 + 1)) is V22() real ext-real Element of REAL
(1 * ((x - x) |^ (x0 + 1))) / ((x0 + 1) !) is V22() real ext-real Element of REAL
(((n,f) . (x0 + 1)) . x) * ((1 * ((x - x) |^ (x0 + 1))) / ((x0 + 1) !)) is V22() real ext-real Element of REAL
(t . x) - ((((n,f) . (x0 + 1)) . x) * ((1 * ((x - x) |^ (x0 + 1))) / ((x0 + 1) !))) is V22() real ext-real Element of REAL
s . x is V22() real ext-real Element of REAL
(((n,f) . (x0 + 1)) . x) * (s . x) is V22() real ext-real Element of REAL
(t . x) - ((((n,f) . (x0 + 1)) . x) * (s . x)) is V22() real ext-real Element of REAL
(((n,f) . (x0 + 1)) (#) s) . x is V22() real ext-real Element of REAL
(t . x) - ((((n,f) . (x0 + 1)) (#) s) . x) is V22() real ext-real Element of REAL
(t - (((n,f) . (x0 + 1)) (#) s)) . x is V22() real ext-real Element of REAL
(t - (((n,].r,x.[) . (x0 + 1)) (#) s)) . hp is V22() real ext-real Element of REAL
hp is V22() real ext-real Element of REAL
(dom c) /\ ].r,x.[ is V80() V81() V82() Element of K19(REAL)
c | ].r,x.[ is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
(c | ].r,x.[) | ].r,x.[ is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
(t - (((n,].r,x.[) . (x0 + 1)) (#) s)) | ].r,x.[ is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
hp is V22() real ext-real Element of REAL
hp is V22() real ext-real Element of REAL
diff (c,hp) is V22() real ext-real Element of REAL
c `| ].r,x.[ is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
(c `| ].r,x.[) . hp is V22() real ext-real Element of REAL
(c | ].r,x.[) `| ].r,x.[ is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
((c | ].r,x.[) `| ].r,x.[) . hp is V22() real ext-real Element of REAL
((t - (((n,].r,x.[) . (x0 + 1)) (#) s)) | ].r,x.[) `| ].r,x.[ is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
(((t - (((n,].r,x.[) . (x0 + 1)) (#) s)) | ].r,x.[) `| ].r,x.[) . hp is V22() real ext-real Element of REAL
(t - (((n,].r,x.[) . (x0 + 1)) (#) s)) `| ].r,x.[ is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
((t - (((n,].r,x.[) . (x0 + 1)) (#) s)) `| ].r,x.[) . hp is V22() real ext-real Element of REAL
diff (t,hp) is V22() real ext-real Element of REAL
diff ((((n,].r,x.[) . (x0 + 1)) (#) s),hp) is V22() real ext-real Element of REAL
(diff (t,hp)) - (diff ((((n,].r,x.[) . (x0 + 1)) (#) s),hp)) is V22() real ext-real Element of REAL
((n,].r,x.[) . (x0 + 1)) . hp is V22() real ext-real Element of REAL
x - hp is V22() real ext-real Element of REAL
(x - hp) |^ x0 is V22() real ext-real Element of REAL
(((n,].r,x.[) . (x0 + 1)) . hp) * ((x - hp) |^ x0) is V22() real ext-real Element of REAL
((((n,].r,x.[) . (x0 + 1)) . hp) * ((x - hp) |^ x0)) / (x0 !) is V22() real ext-real Element of REAL
- (((((n,].r,x.[) . (x0 + 1)) . hp) * ((x - hp) |^ x0)) / (x0 !)) is V22() real ext-real Element of REAL
(- (((((n,].r,x.[) . (x0 + 1)) . hp) * ((x - hp) |^ x0)) / (x0 !))) - (diff ((((n,].r,x.[) . (x0 + 1)) (#) s),hp)) is V22() real ext-real Element of REAL
(((n,].r,x.[) . (x0 + 1)) (#) s) `| ].r,x.[ is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
((((n,].r,x.[) . (x0 + 1)) (#) s) `| ].r,x.[) . hp is V22() real ext-real Element of REAL
(- (((((n,].r,x.[) . (x0 + 1)) . hp) * ((x - hp) |^ x0)) / (x0 !))) - (((((n,].r,x.[) . (x0 + 1)) (#) s) `| ].r,x.[) . hp) is V22() real ext-real Element of REAL
s . hp is V22() real ext-real Element of REAL
diff (((n,].r,x.[) . (x0 + 1)),hp) is V22() real ext-real Element of REAL
(s . hp) * (diff (((n,].r,x.[) . (x0 + 1)),hp)) is V22() real ext-real Element of REAL
diff (s,hp) is V22() real ext-real Element of REAL
(((n,].r,x.[) . (x0 + 1)) . hp) * (diff (s,hp)) is V22() real ext-real Element of REAL
((s . hp) * (diff (((n,].r,x.[) . (x0 + 1)),hp))) + ((((n,].r,x.[) . (x0 + 1)) . hp) * (diff (s,hp))) is V22() real ext-real Element of REAL
(- (((((n,].r,x.[) . (x0 + 1)) . hp) * ((x - hp) |^ x0)) / (x0 !))) - (((s . hp) * (diff (((n,].r,x.[) . (x0 + 1)),hp))) + ((((n,].r,x.[) . (x0 + 1)) . hp) * (diff (s,hp)))) is V22() real ext-real Element of REAL
(- (((((n,].r,x.[) . (x0 + 1)) . hp) * ((x - hp) |^ x0)) / (x0 !))) - ((s . hp) * (diff (((n,].r,x.[) . (x0 + 1)),hp))) is V22() real ext-real Element of REAL
((- (((((n,].r,x.[) . (x0 + 1)) . hp) * ((x - hp) |^ x0)) / (x0 !))) - ((s . hp) * (diff (((n,].r,x.[) . (x0 + 1)),hp)))) - ((((n,].r,x.[) . (x0 + 1)) . hp) * (diff (s,hp))) is V22() real ext-real Element of REAL
(x - hp) |^ (x0 + 1) is V22() real ext-real Element of REAL
1 * ((x - hp) |^ (x0 + 1)) is V22() real ext-real Element of REAL
(1 * ((x - hp) |^ (x0 + 1))) / ((x0 + 1) !) is V22() real ext-real Element of REAL
((1 * ((x - hp) |^ (x0 + 1))) / ((x0 + 1) !)) * (diff (((n,].r,x.[) . (x0 + 1)),hp)) is V22() real ext-real Element of REAL
(- (((((n,].r,x.[) . (x0 + 1)) . hp) * ((x - hp) |^ x0)) / (x0 !))) - (((1 * ((x - hp) |^ (x0 + 1))) / ((x0 + 1) !)) * (diff (((n,].r,x.[) . (x0 + 1)),hp))) is V22() real ext-real Element of REAL
((- (((((n,].r,x.[) . (x0 + 1)) . hp) * ((x - hp) |^ x0)) / (x0 !))) - (((1 * ((x - hp) |^ (x0 + 1))) / ((x0 + 1) !)) * (diff (((n,].r,x.[) . (x0 + 1)),hp)))) - ((((n,].r,x.[) . (x0 + 1)) . hp) * (diff (s,hp))) is V22() real ext-real Element of REAL
((x - hp) |^ (x0 + 1)) / ((x0 + 1) !) is V22() real ext-real Element of REAL
(((x - hp) |^ (x0 + 1)) / ((x0 + 1) !)) * (diff (((n,].r,x.[) . (x0 + 1)),hp)) is V22() real ext-real Element of REAL
(- (((((n,].r,x.[) . (x0 + 1)) . hp) * ((x - hp) |^ x0)) / (x0 !))) - ((((x - hp) |^ (x0 + 1)) / ((x0 + 1) !)) * (diff (((n,].r,x.[) . (x0 + 1)),hp))) is V22() real ext-real Element of REAL
1 * ((x - hp) |^ x0) is V22() real ext-real Element of REAL
(1 * ((x - hp) |^ x0)) / (x0 !) is V22() real ext-real Element of REAL
- ((1 * ((x - hp) |^ x0)) / (x0 !)) is V22() real ext-real Element of REAL
(((n,].r,x.[) . (x0 + 1)) . hp) * (- ((1 * ((x - hp) |^ x0)) / (x0 !))) is V22() real ext-real Element of REAL
((- (((((n,].r,x.[) . (x0 + 1)) . hp) * ((x - hp) |^ x0)) / (x0 !))) - ((((x - hp) |^ (x0 + 1)) / ((x0 + 1) !)) * (diff (((n,].r,x.[) . (x0 + 1)),hp)))) - ((((n,].r,x.[) . (x0 + 1)) . hp) * (- ((1 * ((x - hp) |^ x0)) / (x0 !)))) is V22() real ext-real Element of REAL
(((n,].r,x.[) . (x0 + 1)) . hp) * ((1 * ((x - hp) |^ x0)) / (x0 !)) is V22() real ext-real Element of REAL
(- (((((n,].r,x.[) . (x0 + 1)) . hp) * ((x - hp) |^ x0)) / (x0 !))) + ((((n,].r,x.[) . (x0 + 1)) . hp) * ((1 * ((x - hp) |^ x0)) / (x0 !))) is V22() real ext-real Element of REAL
((- (((((n,].r,x.[) . (x0 + 1)) . hp) * ((x - hp) |^ x0)) / (x0 !))) + ((((n,].r,x.[) . (x0 + 1)) . hp) * ((1 * ((x - hp) |^ x0)) / (x0 !)))) - ((((x - hp) |^ (x0 + 1)) / ((x0 + 1) !)) * (diff (((n,].r,x.[) . (x0 + 1)),hp))) is V22() real ext-real Element of REAL
(- (((((n,].r,x.[) . (x0 + 1)) . hp) * ((x - hp) |^ x0)) / (x0 !))) + (((((n,].r,x.[) . (x0 + 1)) . hp) * ((x - hp) |^ x0)) / (x0 !)) is V22() real ext-real Element of REAL
((- (((((n,].r,x.[) . (x0 + 1)) . hp) * ((x - hp) |^ x0)) / (x0 !))) + (((((n,].r,x.[) . (x0 + 1)) . hp) * ((x - hp) |^ x0)) / (x0 !))) - ((((x - hp) |^ (x0 + 1)) / ((x0 + 1) !)) * (diff (((n,].r,x.[) . (x0 + 1)),hp))) is V22() real ext-real Element of REAL
- ((((x - hp) |^ (x0 + 1)) / ((x0 + 1) !)) * (diff (((n,].r,x.[) . (x0 + 1)),hp))) is V22() real ext-real Element of REAL
((n,].r,x.[) . (x0 + 1)) `| ].r,x.[ is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
(((n,].r,x.[) . (x0 + 1)) `| ].r,x.[) . hp is V22() real ext-real Element of REAL
(((x - hp) |^ (x0 + 1)) / ((x0 + 1) !)) * ((((n,].r,x.[) . (x0 + 1)) `| ].r,x.[) . hp) is V22() real ext-real Element of REAL
- ((((x - hp) |^ (x0 + 1)) / ((x0 + 1) !)) * ((((n,].r,x.[) . (x0 + 1)) `| ].r,x.[) . hp)) is V22() real ext-real Element of REAL
((n,].r,x.[) . ((x0 + 1) + 1)) . hp is V22() real ext-real Element of REAL
(((x - hp) |^ (x0 + 1)) / ((x0 + 1) !)) * (((n,].r,x.[) . ((x0 + 1) + 1)) . hp) is V22() real ext-real Element of REAL
- ((((x - hp) |^ (x0 + 1)) / ((x0 + 1) !)) * (((n,].r,x.[) . ((x0 + 1) + 1)) . hp)) is V22() real ext-real Element of REAL
(((n,].r,x.[) . ((x0 + 1) + 1)) . hp) * ((x - hp) |^ (x0 + 1)) is V22() real ext-real Element of REAL
((((n,].r,x.[) . ((x0 + 1) + 1)) . hp) * ((x - hp) |^ (x0 + 1))) / ((x0 + 1) !) is V22() real ext-real Element of REAL
- (((((n,].r,x.[) . ((x0 + 1) + 1)) . hp) * ((x - hp) |^ (x0 + 1))) / ((x0 + 1) !)) is V22() real ext-real Element of REAL
hp is V22() real ext-real Element of REAL
diff (c,hp) is V22() real ext-real Element of REAL
((n,].r,x.[) . ((x0 + 1) + 1)) . hp is V22() real ext-real Element of REAL
x - hp is V22() real ext-real Element of REAL
(x - hp) |^ (x0 + 1) is V22() real ext-real Element of REAL
(((n,].r,x.[) . ((x0 + 1) + 1)) . hp) * ((x - hp) |^ (x0 + 1)) is V22() real ext-real Element of REAL
((((n,].r,x.[) . ((x0 + 1) + 1)) . hp) * ((x - hp) |^ (x0 + 1))) / ((x0 + 1) !) is V22() real ext-real Element of REAL
- (((((n,].r,x.[) . ((x0 + 1) + 1)) . hp) * ((x - hp) |^ (x0 + 1))) / ((x0 + 1) !)) is V22() real ext-real Element of REAL
c is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
dom c is V80() V81() V82() Element of K19(REAL)
c . x is V22() real ext-real Element of REAL
c | [.r,x.] is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
s is V22() real ext-real Element of REAL
diff (c,s) is V22() real ext-real Element of REAL
((n,].r,x.[) . ((x0 + 1) + 1)) . s is V22() real ext-real Element of REAL
x - s is V22() real ext-real Element of REAL
(x - s) |^ (x0 + 1) is V22() real ext-real Element of REAL
(((n,].r,x.[) . ((x0 + 1) + 1)) . s) * ((x - s) |^ (x0 + 1)) is V22() real ext-real Element of REAL
((((n,].r,x.[) . ((x0 + 1) + 1)) . s) * ((x - s) |^ (x0 + 1))) / ((x0 + 1) !) is V22() real ext-real Element of REAL
- (((((n,].r,x.[) . ((x0 + 1) + 1)) . s) * ((x - s) |^ (x0 + 1))) / ((x0 + 1) !)) 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 V80() V81() V82() V83() V84() V85() V97() Element of NAT
x is V22() real ext-real Element of REAL
r is V22() real ext-real Element of REAL
[.r,x.] is closed V80() V81() V82() V100() Element of K19(REAL)
(n,f) . x0 is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
((n,f) . x0) | [.r,x.] is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,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
].r,x.[ is open V80() V81() V82() V95() V96() V100() Element of K19(REAL)
t is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
dom t is V80() V81() V82() Element of K19(REAL)
n . x is V22() real ext-real Element of REAL
t . x is V22() real ext-real Element of REAL
t | [.r,x.] is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
c is V22() real ext-real Element of REAL
diff (t,c) is V22() real ext-real Element of REAL
(n,].r,x.[) is V1() V4( NAT ) V5( PFuncs (REAL,REAL)) Function-like non empty total quasi_total Element of K19(K20(NAT,(PFuncs (REAL,REAL))))
(n,].r,x.[) . (x0 + 1) is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
((n,].r,x.[) . (x0 + 1)) . c is V22() real ext-real Element of REAL
x - c is V22() real ext-real Element of REAL
(x - c) |^ x0 is V22() real ext-real Element of REAL
(((n,].r,x.[) . (x0 + 1)) . c) * ((x - c) |^ x0) is V22() real ext-real Element of REAL
x0 ! is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative integer non irrational Element of REAL
((((n,].r,x.[) . (x0 + 1)) . c) * ((x - c) |^ x0)) / (x0 !) is V22() real ext-real Element of REAL
- (((((n,].r,x.[) . (x0 + 1)) . c) * ((x - c) |^ x0)) / (x0 !)) 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 ! is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative integer non irrational 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 V80() V81() V82() Element of K19(REAL)
(f,x0) is V1() V4( NAT ) V5( PFuncs (REAL,REAL)) Function-like non empty total quasi_total Element of K19(K20(NAT,(PFuncs (REAL,REAL))))
(f,x0) . n is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
x is V22() real ext-real Element of REAL
r is V22() real ext-real Element of REAL
[.r,x.] is closed V80() V81() V82() V100() Element of K19(REAL)
((f,x0) . n) | [.r,x.] is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
].r,x.[ is open V80() V81() V82() V95() V96() V100() Element of K19(REAL)
f . x is V22() real ext-real Element of REAL
(f,].r,x.[) is V1() V4( NAT ) V5( PFuncs (REAL,REAL)) Function-like non empty total quasi_total Element of K19(K20(NAT,(PFuncs (REAL,REAL))))
(f,].r,x.[) . (n + 1) is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
t is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
dom t is V80() V81() V82() Element of K19(REAL)
t . x is V22() real ext-real Element of REAL
t | [.r,x.] is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
c is V22() real ext-real Element of REAL
t . c is V22() real ext-real Element of REAL
(f,x0,c,x) is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
Partial_Sums (f,x0,c,x) is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
(Partial_Sums (f,x0,c,x)) . n is V22() real ext-real Element of REAL
(f . x) - ((Partial_Sums (f,x0,c,x)) . n) is V22() real ext-real Element of REAL
s is V22() real ext-real Element of REAL
diff (t,s) is V22() real ext-real Element of REAL
((f,].r,x.[) . (n + 1)) . s is V22() real ext-real Element of REAL
x - s is V22() real ext-real Element of REAL
(x - s) |^ n is V22() real ext-real Element of REAL
(((f,].r,x.[) . (n + 1)) . s) * ((x - s) |^ n) is V22() real ext-real Element of REAL
((((f,].r,x.[) . (n + 1)) . s) * ((x - s) |^ n)) / (n !) is V22() real ext-real Element of REAL
- (((((f,].r,x.[) . (n + 1)) . s) * ((x - s) |^ n)) / (n !)) 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 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 V80() V81() V82() Element of K19(REAL)
(f,x0) is V1() V4( NAT ) V5( PFuncs (REAL,REAL)) Function-like non empty total quasi_total Element of K19(K20(NAT,(PFuncs (REAL,REAL))))
(f,x0) . n is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
x is V22() real ext-real Element of REAL
r is V22() real ext-real Element of REAL
[.r,x.] is closed V80() V81() V82() V100() Element of K19(REAL)
((f,x0) . n) | [.r,x.] is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
].r,x.[ is open V80() V81() V82() V95() V96() V100() Element of K19(REAL)
f . x is V22() real ext-real Element of REAL
(f,x0,r,x) is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
Partial_Sums (f,x0,r,x) is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
(Partial_Sums (f,x0,r,x)) . n is V22() real ext-real Element of REAL
(f . x) - ((Partial_Sums (f,x0,r,x)) . n) is V22() real ext-real Element of REAL
x - r is V22() real ext-real Element of REAL
(x - r) |^ (n + 1) is V22() real ext-real Element of REAL
(f,].r,x.[) is V1() V4( NAT ) V5( PFuncs (REAL,REAL)) Function-like non empty total quasi_total Element of K19(K20(NAT,(PFuncs (REAL,REAL))))
(f,].r,x.[) . (n + 1) is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
t is V22() real ext-real Element of REAL
t * ((x - r) |^ (n + 1)) is V22() real ext-real Element of REAL
(t * ((x - r) |^ (n + 1))) / ((n + 1) !) is V22() real ext-real Element of REAL
((f . x) - ((Partial_Sums (f,x0,r,x)) . n)) - ((t * ((x - r) |^ (n + 1))) / ((n + 1) !)) is V22() real ext-real Element of REAL
c is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
dom c is V80() V81() V82() Element of K19(REAL)
s is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
dom s is V80() V81() V82() Element of K19(REAL)
s . x is V22() real ext-real Element of REAL
s | [.r,x.] is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
(dom s) /\ (dom c) is V80() V81() V82() Element of K19(REAL)
g is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
dom g is V80() V81() V82() Element of K19(REAL)
g . r is V22() real ext-real Element of REAL
g . x is V22() real ext-real Element of REAL
g | [.r,x.] is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
s - c is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
dom (s - c) is V80() V81() V82() Element of K19(REAL)
x is set
(s - c) . x is V22() real ext-real Element of REAL
g . x is V22() real ext-real Element of REAL
xx is V22() real ext-real Element of REAL
s . xx is V22() real ext-real Element of REAL
c . xx is V22() real ext-real Element of REAL
(s . xx) - (c . xx) is V22() real ext-real Element of REAL
(f,x0,xx,x) is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
Partial_Sums (f,x0,xx,x) is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
(Partial_Sums (f,x0,xx,x)) . n is V22() real ext-real Element of REAL
(f . x) - ((Partial_Sums (f,x0,xx,x)) . n) is V22() real ext-real Element of REAL
((f . x) - ((Partial_Sums (f,x0,xx,x)) . n)) - (c . xx) is V22() real ext-real Element of REAL
x - xx is V22() real ext-real Element of REAL
(x - xx) |^ (n + 1) is V22() real ext-real Element of REAL
t * ((x - xx) |^ (n + 1)) is V22() real ext-real Element of REAL
(t * ((x - xx) |^ (n + 1))) / ((n + 1) !) is V22() real ext-real Element of REAL
((f . x) - ((Partial_Sums (f,x0,xx,x)) . n)) - ((t * ((x - xx) |^ (n + 1))) / ((n + 1) !)) is V22() real ext-real Element of REAL
x is V22() real ext-real Element of REAL
c | REAL is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
c | [.r,x.] is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
(dom g) /\ x0 is V80() V81() V82() Element of K19(REAL)
(s - c) | ].r,x.[ is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
g | x0 is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
(g | x0) | ].r,x.[ is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
g | ].r,x.[ is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
x is V22() real ext-real Element of REAL
diff ((s - c),x) is V22() real ext-real Element of REAL
((f,].r,x.[) . (n + 1)) . x is V22() real ext-real Element of REAL
x - x is V22() real ext-real Element of REAL
(x - x) |^ n is V22() real ext-real Element of REAL
(((f,].r,x.[) . (n + 1)) . x) * ((x - x) |^ n) is V22() real ext-real Element of REAL
((((f,].r,x.[) . (n + 1)) . x) * ((x - x) |^ n)) / (n !) is V22() real ext-real Element of REAL
- (((((f,].r,x.[) . (n + 1)) . x) * ((x - x) |^ n)) / (n !)) is V22() real ext-real Element of REAL
t * ((x - x) |^ n) is V22() real ext-real Element of REAL
(t * ((x - x) |^ n)) / (n !) is V22() real ext-real Element of REAL
(- (((((f,].r,x.[) . (n + 1)) . x) * ((x - x) |^ n)) / (n !))) + ((t * ((x - x) |^ n)) / (n !)) is V22() real ext-real Element of REAL
diff (s,x) is V22() real ext-real Element of REAL
diff (c,x) is V22() real ext-real Element of REAL
(diff (s,x)) - (diff (c,x)) is V22() real ext-real Element of REAL
(- (((((f,].r,x.[) . (n + 1)) . x) * ((x - x) |^ n)) / (n !))) - (diff (c,x)) is V22() real ext-real Element of REAL
- ((t * ((x - x) |^ n)) / (n !)) is V22() real ext-real Element of REAL
(- (((((f,].r,x.[) . (n + 1)) . x) * ((x - x) |^ n)) / (n !))) - (- ((t * ((x - x) |^ n)) / (n !))) 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
(s - c) . x is V22() real ext-real Element of REAL
c . x is V22() real ext-real Element of REAL
(s . x) - (c . x) is V22() real ext-real Element of REAL
x - x is V22() real ext-real Element of REAL
(x - x) |^ (n + 1) is V22() real ext-real Element of REAL
t * ((x - x) |^ (n + 1)) is V22() real ext-real Element of REAL
(t * ((x - x) |^ (n + 1))) / ((n + 1) !) is V22() real ext-real Element of REAL
0 - ((t * ((x - x) |^ (n + 1))) / ((n + 1) !)) is V22() real ext-real Element of REAL
0 |^ 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
(0 |^ n) * 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
t * ((0 |^ n) * 0) is V22() real ext-real Element of REAL
(t * ((0 |^ n) * 0)) / ((n + 1) !) is V22() real ext-real Element of REAL
0 - ((t * ((0 |^ n) * 0)) / ((n + 1) !)) is V22() real ext-real Element of REAL
(s - c) | [.r,x.] is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
(g | x0) | [.r,x.] is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
x is V22() real ext-real Element of REAL
diff (g,x) is V22() real ext-real Element of REAL
((f,].r,x.[) . (n + 1)) . x is V22() real ext-real Element of REAL
x - x is V22() real ext-real Element of REAL
(x - x) |^ n is V22() real ext-real Element of REAL
(((f,].r,x.[) . (n + 1)) . x) * ((x - x) |^ n) is V22() real ext-real Element of REAL
((((f,].r,x.[) . (n + 1)) . x) * ((x - x) |^ n)) / (n !) is V22() real ext-real Element of REAL
- (((((f,].r,x.[) . (n + 1)) . x) * ((x - x) |^ n)) / (n !)) is V22() real ext-real Element of REAL
t * ((x - x) |^ n) is V22() real ext-real Element of REAL
(t * ((x - x) |^ n)) / (n !) is V22() real ext-real Element of REAL
(- (((((f,].r,x.[) . (n + 1)) . x) * ((x - x) |^ n)) / (n !))) + ((t * ((x - x) |^ n)) / (n !)) is V22() real ext-real Element of REAL
g `| ].r,x.[ is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
(g `| ].r,x.[) . x is V22() real ext-real Element of REAL
(g | ].r,x.[) `| ].r,x.[ is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
((g | ].r,x.[) `| ].r,x.[) . x is V22() real ext-real Element of REAL
(s - c) `| ].r,x.[ is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
((s - c) `| ].r,x.[) . x is V22() real ext-real Element of REAL
diff ((s - c),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
f is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
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
x is V22() real ext-real Element of REAL
t is V1() V4( REAL ) V5( REAL ) Function-like non empty total quasi_total V33() V34() V35() Element of K19(K20(REAL,REAL))
c is V22() real ext-real Element of REAL
t . c is V22() real ext-real Element of REAL
(f,x0,c,r) is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
Partial_Sums (f,x0,c,r) is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
(Partial_Sums (f,x0,c,r)) . n is V22() real ext-real Element of REAL
(f . r) - ((Partial_Sums (f,x0,c,r)) . n) is V22() real ext-real Element of REAL
r - c is V22() real ext-real Element of REAL
(r - c) |^ (n + 1) is V22() real ext-real Element of REAL
x * ((r - c) |^ (n + 1)) is V22() real ext-real Element of REAL
(x * ((r - c) |^ (n + 1))) / ((n + 1) !) is V22() real ext-real Element of REAL
((f . r) - ((Partial_Sums (f,x0,c,r)) . n)) - ((x * ((r - c) |^ (n + 1))) / ((n + 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 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
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 V80() V81() V82() Element of K19(REAL)
(f,x0) is V1() V4( NAT ) V5( PFuncs (REAL,REAL)) Function-like non empty total quasi_total Element of K19(K20(NAT,(PFuncs (REAL,REAL))))
(f,x0) . n is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
x is V22() real ext-real Element of REAL
r is V22() real ext-real Element of REAL
[.r,x.] is closed V80() V81() V82() V100() Element of K19(REAL)
((f,x0) . n) | [.r,x.] is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
].r,x.[ is open V80() V81() V82() V95() V96() V100() Element of K19(REAL)
f . x is V22() real ext-real Element of REAL
(f,x0,r,x) is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
Partial_Sums (f,x0,r,x) is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
(Partial_Sums (f,x0,r,x)) . n is V22() real ext-real Element of REAL
(f,].r,x.[) is V1() V4( NAT ) V5( PFuncs (REAL,REAL)) Function-like non empty total quasi_total Element of K19(K20(NAT,(PFuncs (REAL,REAL))))
(f,].r,x.[) . (n + 1) is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
x - r is V22() real ext-real Element of REAL
(x - r) |^ (n + 1) is V22() real ext-real Element of REAL
(f . x) - ((Partial_Sums (f,x0,r,x)) . n) is V22() real ext-real Element of REAL
((x - r) |^ (n + 1)) / ((n + 1) !) is V22() real ext-real Element of REAL
H₁(r) / (((x - r) |^ (n + 1)) / ((n + 1) !)) is V22() real ext-real Element of REAL
t is V22() real ext-real Element of REAL
c is V1() V4( REAL ) V5( REAL ) Function-like non empty total quasi_total V33() V34() V35() Element of K19(K20(REAL,REAL))
t * ((x - r) |^ (n + 1)) is V22() real ext-real Element of REAL
(t * ((x - r) |^ (n + 1))) / ((n + 1) !) is V22() real ext-real Element of REAL
((f . x) - ((Partial_Sums (f,x0,r,x)) . n)) - ((t * ((x - r) |^ (n + 1))) / ((n + 1) !)) is V22() real ext-real Element of REAL
(H₁(r) / (((x - r) |^ (n + 1)) / ((n + 1) !))) * (((x - r) |^ (n + 1)) / ((n + 1) !)) is V22() real ext-real Element of REAL
H₁(r) - ((H₁(r) / (((x - r) |^ (n + 1)) / ((n + 1) !))) * (((x - r) |^ (n + 1)) / ((n + 1) !))) is V22() real ext-real Element of REAL
H₁(r) - H₁(r) is V22() real ext-real Element of REAL
c . r is V22() real ext-real Element of REAL
dom c is V80() V81() V82() Element of K19(REAL)
c | [.r,x.] is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
c . x is V22() real ext-real Element of REAL
s is V22() real ext-real Element of REAL
diff (c,s) is V22() real ext-real Element of REAL
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( not b₁ <= r & not x <= b₁ ) } is set
x - s is V22() real ext-real Element of REAL
g is V22() real ext-real Element of REAL
(x - s) |^ n is V22() real ext-real Element of REAL
((f,].r,x.[) . (n + 1)) . s is V22() real ext-real Element of REAL
(((f,].r,x.[) . (n + 1)) . s) * ((x - s) |^ n) is V22() real ext-real 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,].r,x.[) . (n + 1)) . s) * ((x - s) |^ n)) / (n !) is V22() real ext-real Element of REAL
- (((((f,].r,x.[) . (n + 1)) . s) * ((x - s) |^ n)) / (n !)) is V22() real ext-real Element of REAL
t * ((x - s) |^ n) is V22() real ext-real Element of REAL
(t * ((x - s) |^ n)) / (n !) is V22() real ext-real Element of REAL
(- (((((f,].r,x.[) . (n + 1)) . s) * ((x - s) |^ n)) / (n !))) + ((t * ((x - s) |^ n)) / (n !)) is V22() real ext-real Element of REAL
(((((f,].r,x.[) . (n + 1)) . s) * ((x - s) |^ n)) / (n !)) * (n !) is V22() real ext-real Element of REAL
((t * ((x - s) |^ n)) / (n !)) * (n !) is V22() real ext-real Element of REAL
((((((f,].r,x.[) . (n + 1)) . s) * ((x - s) |^ n)) / (n !)) * (n !)) - (((t * ((x - s) |^ n)) / (n !)) * (n !)) is V22() real ext-real Element of REAL
((((f,].r,x.[) . (n + 1)) . s) * ((x - s) |^ n)) - (((t * ((x - s) |^ n)) / (n !)) * (n !)) is V22() real ext-real Element of REAL
((((f,].r,x.[) . (n + 1)) . s) * ((x - s) |^ n)) - (t * ((x - s) |^ n)) is V22() real ext-real Element of REAL
(((((f,].r,x.[) . (n + 1)) . s) * ((x - s) |^ n)) - (t * ((x - s) |^ n))) / ((x - s) |^ n) is V22() real ext-real Element of REAL
0 / ((x - s) |^ n) is V22() real ext-real Element of REAL
((((f,].r,x.[) . (n + 1)) . s) * ((x - s) |^ n)) / ((x - s) |^ n) is V22() real ext-real Element of REAL
(t * ((x - s) |^ n)) / ((x - s) |^ n) is V22() real ext-real Element of REAL
(((((f,].r,x.[) . (n + 1)) . s) * ((x - s) |^ n)) / ((x - s) |^ n)) - ((t * ((x - s) |^ n)) / ((x - s) |^ n)) is V22() real ext-real Element of REAL
(((f,].r,x.[) . (n + 1)) . s) - ((t * ((x - s) |^ n)) / ((x - s) |^ n)) is V22() real ext-real Element of REAL
(((f,].r,x.[) . (n + 1)) . s) * ((x - r) |^ (n + 1)) is V22() real ext-real Element of REAL
((((f,].r,x.[) . (n + 1)) . s) * ((x - r) |^ (n + 1))) / ((n + 1) !) is V22() real ext-real Element of REAL
((f . x) - ((Partial_Sums (f,x0,r,x)) . n)) - (((((f,].r,x.[) . (n + 1)) . s) * ((x - r) |^ (n + 1))) / ((n + 1) !)) is V22() real ext-real Element of REAL
(((((f,].r,x.[) . (n + 1)) . s) * ((x - r) |^ (n + 1))) / ((n + 1) !)) + ((Partial_Sums (f,x0,r,x)) . n) is V22() real ext-real Element of REAL
n is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
dom n is V80() V81() V82() Element of K19(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 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) . x0 is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,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 ! is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative integer non irrational Element of REAL
(n,f) . (x0 + 1) is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
(x0 + 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
(x0 + 1) ! is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative integer non irrational Element of REAL
x is V22() real ext-real Element of REAL
r is V22() real ext-real Element of REAL
[.r,x.] is closed V80() V81() V82() V100() Element of K19(REAL)
((n,f) . (x0 + 1)) | [.r,x.] is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
].r,x.[ is open V80() V81() V82() V95() V96() V100() Element of K19(REAL)
n . r is V22() real ext-real Element of REAL
(n,].r,x.[) is V1() V4( NAT ) V5( PFuncs (REAL,REAL)) Function-like non empty total quasi_total Element of K19(K20(NAT,(PFuncs (REAL,REAL))))
(n,].r,x.[) . ((x0 + 1) + 1) is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
(x0 + 1) - 1 is V22() real ext-real integer non irrational Element of REAL
((n,f) . x0) | f is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
((n,f) . x0) | [.r,x.] is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
t is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
dom t is V80() V81() V82() Element of K19(REAL)
t | [.r,x.] is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
((x0 + 1) + 1) - 1 is V22() real ext-real integer non irrational Element of REAL
(n,].r,x.[) . x0 is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
((n,f) . x0) `| 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))
dom c is V80() V81() V82() Element of K19(REAL)
c . r is V22() real ext-real Element of REAL
(n,f,r,r) is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
Partial_Sums (n,f,r,r) is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
(Partial_Sums (n,f,r,r)) . (x0 + 1) is V22() real ext-real Element of REAL
(n . r) - ((Partial_Sums (n,f,r,r)) . (x0 + 1)) is V22() real ext-real Element of REAL
(Partial_Sums (n,f,r,r)) . x0 is V22() real ext-real Element of REAL
(n,f,r,r) . (x0 + 1) is V22() real ext-real Element of REAL
((Partial_Sums (n,f,r,r)) . x0) + ((n,f,r,r) . (x0 + 1)) is V22() real ext-real Element of REAL
(n . r) - (((Partial_Sums (n,f,r,r)) . x0) + ((n,f,r,r) . (x0 + 1))) is V22() real ext-real Element of REAL
(n . r) - ((Partial_Sums (n,f,r,r)) . x0) is V22() real ext-real Element of REAL
((n . r) - ((Partial_Sums (n,f,r,r)) . x0)) - ((n,f,r,r) . (x0 + 1)) is V22() real ext-real Element of REAL
t . r is V22() real ext-real Element of REAL
(t . r) - ((n,f,r,r) . (x0 + 1)) is V22() real ext-real Element of REAL
0 - ((n,f,r,r) . (x0 + 1)) is V22() real ext-real Element of REAL
((n,f) . (x0 + 1)) . r is V22() real ext-real Element of REAL
r - r is V22() real ext-real Element of REAL
(r - r) |^ (x0 + 1) is V22() real ext-real Element of REAL
(((n,f) . (x0 + 1)) . r) * ((r - r) |^ (x0 + 1)) is V22() real ext-real Element of REAL
((((n,f) . (x0 + 1)) . r) * ((r - r) |^ (x0 + 1))) / ((x0 + 1) !) is V22() real ext-real Element of REAL
0 - (((((n,f) . (x0 + 1)) . r) * ((r - r) |^ (x0 + 1))) / ((x0 + 1) !)) is V22() real ext-real Element of REAL
0 |^ 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
(0 |^ x0) * 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,f) . (x0 + 1)) . r) * ((0 |^ x0) * 0) is V22() real ext-real Element of REAL
((((n,f) . (x0 + 1)) . r) * ((0 |^ x0) * 0)) / ((x0 + 1) !) is V22() real ext-real Element of REAL
0 - (((((n,f) . (x0 + 1)) . r) * ((0 |^ x0) * 0)) / ((x0 + 1) !)) is V22() real ext-real Element of REAL
s is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
dom s is V80() V81() V82() Element of K19(REAL)
((n,f) . (x0 + 1)) (#) s is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
dom (((n,f) . (x0 + 1)) (#) s) is V80() V81() V82() Element of K19(REAL)
dom ((n,f) . (x0 + 1)) is V80() V81() V82() Element of K19(REAL)
(dom ((n,f) . (x0 + 1))) /\ (dom s) is V80() V81() V82() Element of K19(REAL)
f /\ REAL is V80() V81() V82() Element of K19(REAL)
t - (((n,f) . (x0 + 1)) (#) s) is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
dom (t - (((n,f) . (x0 + 1)) (#) s)) is V80() V81() V82() Element of K19(REAL)
(dom t) /\ (dom (((n,f) . (x0 + 1)) (#) s)) is V80() V81() V82() Element of K19(REAL)
c | [.r,x.] is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
hp is V22() real ext-real Element of REAL
s | REAL is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
s | [.r,x.] is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
hp is V22() real ext-real Element of REAL
c . hp is V22() real ext-real Element of REAL
(n,f,hp,r) is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
Partial_Sums (n,f,hp,r) is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
(Partial_Sums (n,f,hp,r)) . (x0 + 1) is V22() real ext-real Element of REAL
(n . r) - ((Partial_Sums (n,f,hp,r)) . (x0 + 1)) is V22() real ext-real Element of REAL
(Partial_Sums (n,f,hp,r)) . x0 is V22() real ext-real Element of REAL
(n,f,hp,r) . (x0 + 1) is V22() real ext-real Element of REAL
((Partial_Sums (n,f,hp,r)) . x0) + ((n,f,hp,r) . (x0 + 1)) is V22() real ext-real Element of REAL
(n . r) - (((Partial_Sums (n,f,hp,r)) . x0) + ((n,f,hp,r) . (x0 + 1))) is V22() real ext-real Element of REAL
(n . r) - ((Partial_Sums (n,f,hp,r)) . x0) is V22() real ext-real Element of REAL
((n . r) - ((Partial_Sums (n,f,hp,r)) . x0)) - ((n,f,hp,r) . (x0 + 1)) is V22() real ext-real Element of REAL
t . hp is V22() real ext-real Element of REAL
(t . hp) - ((n,f,hp,r) . (x0 + 1)) is V22() real ext-real Element of REAL
((n,f) . (x0 + 1)) . hp is V22() real ext-real Element of REAL
r - hp is V22() real ext-real Element of REAL
(r - hp) |^ (x0 + 1) is V22() real ext-real Element of REAL
(((n,f) . (x0 + 1)) . hp) * ((r - hp) |^ (x0 + 1)) is V22() real ext-real Element of REAL
((((n,f) . (x0 + 1)) . hp) * ((r - hp) |^ (x0 + 1))) / ((x0 + 1) !) is V22() real ext-real Element of REAL
(t . hp) - (((((n,f) . (x0 + 1)) . hp) * ((r - hp) |^ (x0 + 1))) / ((x0 + 1) !)) is V22() real ext-real Element of REAL
1 * ((r - hp) |^ (x0 + 1)) is V22() real ext-real Element of REAL
(1 * ((r - hp) |^ (x0 + 1))) / ((x0 + 1) !) is V22() real ext-real Element of REAL
(((n,f) . (x0 + 1)) . hp) * ((1 * ((r - hp) |^ (x0 + 1))) / ((x0 + 1) !)) is V22() real ext-real Element of REAL
(t . hp) - ((((n,f) . (x0 + 1)) . hp) * ((1 * ((r - hp) |^ (x0 + 1))) / ((x0 + 1) !))) is V22() real ext-real Element of REAL
s . hp is V22() real ext-real Element of REAL
(((n,f) . (x0 + 1)) . hp) * (s . hp) is V22() real ext-real Element of REAL
(t . hp) - ((((n,f) . (x0 + 1)) . hp) * (s . hp)) is V22() real ext-real Element of REAL
(((n,f) . (x0 + 1)) (#) s) . hp is V22() real ext-real Element of REAL
(t . hp) - ((((n,f) . (x0 + 1)) (#) s) . hp) is V22() real ext-real Element of REAL
(t - (((n,f) . (x0 + 1)) (#) s)) . hp is V22() real ext-real Element of REAL
[.r,x.] /\ [.r,x.] is V80() V81() V82() V100() Element of K19(REAL)
(((n,f) . (x0 + 1)) (#) s) | ([.r,x.] /\ [.r,x.]) is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
(n,].r,x.[) . (x0 + 1) is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
((n,].r,x.[) . x0) `| ].r,x.[ is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
((n,].r,x.[) . (x0 + 1)) (#) s is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
t - (((n,].r,x.[) . (x0 + 1)) (#) s) is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
dom (((n,].r,x.[) . (x0 + 1)) (#) s) is V80() V81() V82() Element of K19(REAL)
dom ((n,].r,x.[) . (x0 + 1)) is V80() V81() V82() Element of K19(REAL)
(dom ((n,].r,x.[) . (x0 + 1))) /\ (dom s) is V80() V81() V82() Element of K19(REAL)
].r,x.[ /\ REAL is V80() V81() V82() V100() Element of K19(REAL)
dom (t - (((n,].r,x.[) . (x0 + 1)) (#) s)) is V80() V81() V82() Element of K19(REAL)
f /\ (dom (((n,].r,x.[) . (x0 + 1)) (#) s)) is V80() V81() V82() Element of K19(REAL)
hp is V22() real ext-real Element of REAL
(t - (((n,f) . (x0 + 1)) (#) s)) . hp is V22() real ext-real Element of REAL
(t - (((n,].r,x.[) . (x0 + 1)) (#) s)) . hp is V22() real ext-real Element of REAL
t . hp is V22() real ext-real Element of REAL
(((n,].r,x.[) . (x0 + 1)) (#) s) . hp is V22() real ext-real Element of REAL
(t . hp) - ((((n,].r,x.[) . (x0 + 1)) (#) s) . hp) is V22() real ext-real Element of REAL
((n,].r,x.[) . (x0 + 1)) . hp is V22() real ext-real Element of REAL
s . hp is V22() real ext-real Element of REAL
(((n,].r,x.[) . (x0 + 1)) . hp) * (s . hp) is V22() real ext-real Element of REAL
(t . hp) - ((((n,].r,x.[) . (x0 + 1)) . hp) * (s . hp)) is V22() real ext-real Element of REAL
((n,f) . (x0 + 1)) | ].r,x.[ is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
(((n,f) . (x0 + 1)) | ].r,x.[) . hp is V22() real ext-real Element of REAL
((((n,f) . (x0 + 1)) | ].r,x.[) . hp) * (s . hp) is V22() real ext-real Element of REAL
(t . hp) - (((((n,f) . (x0 + 1)) | ].r,x.[) . hp) * (s . hp)) is V22() real ext-real Element of REAL
((n,f) . (x0 + 1)) . hp is V22() real ext-real Element of REAL
(((n,f) . (x0 + 1)) . hp) * (s . hp) is V22() real ext-real Element of REAL
(t . hp) - ((((n,f) . (x0 + 1)) . hp) * (s . hp)) is V22() real ext-real Element of REAL
(((n,f) . (x0 + 1)) (#) s) . hp is V22() real ext-real Element of REAL
(t . hp) - ((((n,f) . (x0 + 1)) (#) s) . hp) is V22() real ext-real Element of REAL
hp is set
c . hp is V22() real ext-real Element of REAL
x is V22() real ext-real Element of REAL
(n,f,x,r) is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
Partial_Sums (n,f,x,r) is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
(Partial_Sums (n,f,x,r)) . (x0 + 1) is V22() real ext-real Element of REAL
(n . r) - ((Partial_Sums (n,f,x,r)) . (x0 + 1)) is V22() real ext-real Element of REAL
(Partial_Sums (n,f,x,r)) . x0 is V22() real ext-real Element of REAL
(n,f,x,r) . (x0 + 1) is V22() real ext-real Element of REAL
((Partial_Sums (n,f,x,r)) . x0) + ((n,f,x,r) . (x0 + 1)) is V22() real ext-real Element of REAL
(n . r) - (((Partial_Sums (n,f,x,r)) . x0) + ((n,f,x,r) . (x0 + 1))) is V22() real ext-real Element of REAL
(n . r) - ((Partial_Sums (n,f,x,r)) . x0) is V22() real ext-real Element of REAL
((n . r) - ((Partial_Sums (n,f,x,r)) . x0)) - ((n,f,x,r) . (x0 + 1)) is V22() real ext-real Element of REAL
t . x is V22() real ext-real Element of REAL
(t . x) - ((n,f,x,r) . (x0 + 1)) is V22() real ext-real Element of REAL
((n,f) . (x0 + 1)) . x is V22() real ext-real Element of REAL
r - x is V22() real ext-real Element of REAL
(r - x) |^ (x0 + 1) is V22() real ext-real Element of REAL
(((n,f) . (x0 + 1)) . x) * ((r - x) |^ (x0 + 1)) is V22() real ext-real Element of REAL
((((n,f) . (x0 + 1)) . x) * ((r - x) |^ (x0 + 1))) / ((x0 + 1) !) is V22() real ext-real Element of REAL
(t . x) - (((((n,f) . (x0 + 1)) . x) * ((r - x) |^ (x0 + 1))) / ((x0 + 1) !)) is V22() real ext-real Element of REAL
1 * ((r - x) |^ (x0 + 1)) is V22() real ext-real Element of REAL
(1 * ((r - x) |^ (x0 + 1))) / ((x0 + 1) !) is V22() real ext-real Element of REAL
(((n,f) . (x0 + 1)) . x) * ((1 * ((r - x) |^ (x0 + 1))) / ((x0 + 1) !)) is V22() real ext-real Element of REAL
(t . x) - ((((n,f) . (x0 + 1)) . x) * ((1 * ((r - x) |^ (x0 + 1))) / ((x0 + 1) !))) is V22() real ext-real Element of REAL
s . x is V22() real ext-real Element of REAL
(((n,f) . (x0 + 1)) . x) * (s . x) is V22() real ext-real Element of REAL
(t . x) - ((((n,f) . (x0 + 1)) . x) * (s . x)) is V22() real ext-real Element of REAL
(((n,f) . (x0 + 1)) (#) s) . x is V22() real ext-real Element of REAL
(t . x) - ((((n,f) . (x0 + 1)) (#) s) . x) is V22() real ext-real Element of REAL
(t - (((n,f) . (x0 + 1)) (#) s)) . x is V22() real ext-real Element of REAL
(t - (((n,].r,x.[) . (x0 + 1)) (#) s)) . hp is V22() real ext-real Element of REAL
hp is V22() real ext-real Element of REAL
(dom c) /\ ].r,x.[ is V80() V81() V82() Element of K19(REAL)
c | ].r,x.[ is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
(c | ].r,x.[) | ].r,x.[ is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
(t - (((n,].r,x.[) . (x0 + 1)) (#) s)) | ].r,x.[ is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
hp is V22() real ext-real Element of REAL
hp is V22() real ext-real Element of REAL
diff (c,hp) is V22() real ext-real Element of REAL
c `| ].r,x.[ is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
(c `| ].r,x.[) . hp is V22() real ext-real Element of REAL
(c | ].r,x.[) `| ].r,x.[ is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
((c | ].r,x.[) `| ].r,x.[) . hp is V22() real ext-real Element of REAL
((t - (((n,].r,x.[) . (x0 + 1)) (#) s)) | ].r,x.[) `| ].r,x.[ is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
(((t - (((n,].r,x.[) . (x0 + 1)) (#) s)) | ].r,x.[) `| ].r,x.[) . hp is V22() real ext-real Element of REAL
(t - (((n,].r,x.[) . (x0 + 1)) (#) s)) `| ].r,x.[ is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
((t - (((n,].r,x.[) . (x0 + 1)) (#) s)) `| ].r,x.[) . hp is V22() real ext-real Element of REAL
diff (t,hp) is V22() real ext-real Element of REAL
diff ((((n,].r,x.[) . (x0 + 1)) (#) s),hp) is V22() real ext-real Element of REAL
(diff (t,hp)) - (diff ((((n,].r,x.[) . (x0 + 1)) (#) s),hp)) is V22() real ext-real Element of REAL
((n,].r,x.[) . (x0 + 1)) . hp is V22() real ext-real Element of REAL
r - hp is V22() real ext-real Element of REAL
(r - hp) |^ x0 is V22() real ext-real Element of REAL
(((n,].r,x.[) . (x0 + 1)) . hp) * ((r - hp) |^ x0) is V22() real ext-real Element of REAL
((((n,].r,x.[) . (x0 + 1)) . hp) * ((r - hp) |^ x0)) / (x0 !) is V22() real ext-real Element of REAL
- (((((n,].r,x.[) . (x0 + 1)) . hp) * ((r - hp) |^ x0)) / (x0 !)) is V22() real ext-real Element of REAL
(- (((((n,].r,x.[) . (x0 + 1)) . hp) * ((r - hp) |^ x0)) / (x0 !))) - (diff ((((n,].r,x.[) . (x0 + 1)) (#) s),hp)) is V22() real ext-real Element of REAL
(((n,].r,x.[) . (x0 + 1)) (#) s) `| ].r,x.[ is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
((((n,].r,x.[) . (x0 + 1)) (#) s) `| ].r,x.[) . hp is V22() real ext-real Element of REAL
(- (((((n,].r,x.[) . (x0 + 1)) . hp) * ((r - hp) |^ x0)) / (x0 !))) - (((((n,].r,x.[) . (x0 + 1)) (#) s) `| ].r,x.[) . hp) is V22() real ext-real Element of REAL
s . hp is V22() real ext-real Element of REAL
diff (((n,].r,x.[) . (x0 + 1)),hp) is V22() real ext-real Element of REAL
(s . hp) * (diff (((n,].r,x.[) . (x0 + 1)),hp)) is V22() real ext-real Element of REAL
diff (s,hp) is V22() real ext-real Element of REAL
(((n,].r,x.[) . (x0 + 1)) . hp) * (diff (s,hp)) is V22() real ext-real Element of REAL
((s . hp) * (diff (((n,].r,x.[) . (x0 + 1)),hp))) + ((((n,].r,x.[) . (x0 + 1)) . hp) * (diff (s,hp))) is V22() real ext-real Element of REAL
(- (((((n,].r,x.[) . (x0 + 1)) . hp) * ((r - hp) |^ x0)) / (x0 !))) - (((s . hp) * (diff (((n,].r,x.[) . (x0 + 1)),hp))) + ((((n,].r,x.[) . (x0 + 1)) . hp) * (diff (s,hp)))) is V22() real ext-real Element of REAL
(- (((((n,].r,x.[) . (x0 + 1)) . hp) * ((r - hp) |^ x0)) / (x0 !))) - ((s . hp) * (diff (((n,].r,x.[) . (x0 + 1)),hp))) is V22() real ext-real Element of REAL
((- (((((n,].r,x.[) . (x0 + 1)) . hp) * ((r - hp) |^ x0)) / (x0 !))) - ((s . hp) * (diff (((n,].r,x.[) . (x0 + 1)),hp)))) - ((((n,].r,x.[) . (x0 + 1)) . hp) * (diff (s,hp))) is V22() real ext-real Element of REAL
(r - hp) |^ (x0 + 1) is V22() real ext-real Element of REAL
1 * ((r - hp) |^ (x0 + 1)) is V22() real ext-real Element of REAL
(1 * ((r - hp) |^ (x0 + 1))) / ((x0 + 1) !) is V22() real ext-real Element of REAL
((1 * ((r - hp) |^ (x0 + 1))) / ((x0 + 1) !)) * (diff (((n,].r,x.[) . (x0 + 1)),hp)) is V22() real ext-real Element of REAL
(- (((((n,].r,x.[) . (x0 + 1)) . hp) * ((r - hp) |^ x0)) / (x0 !))) - (((1 * ((r - hp) |^ (x0 + 1))) / ((x0 + 1) !)) * (diff (((n,].r,x.[) . (x0 + 1)),hp))) is V22() real ext-real Element of REAL
((- (((((n,].r,x.[) . (x0 + 1)) . hp) * ((r - hp) |^ x0)) / (x0 !))) - (((1 * ((r - hp) |^ (x0 + 1))) / ((x0 + 1) !)) * (diff (((n,].r,x.[) . (x0 + 1)),hp)))) - ((((n,].r,x.[) . (x0 + 1)) . hp) * (diff (s,hp))) is V22() real ext-real Element of REAL
((r - hp) |^ (x0 + 1)) / ((x0 + 1) !) is V22() real ext-real Element of REAL
(((r - hp) |^ (x0 + 1)) / ((x0 + 1) !)) * (diff (((n,].r,x.[) . (x0 + 1)),hp)) is V22() real ext-real Element of REAL
(- (((((n,].r,x.[) . (x0 + 1)) . hp) * ((r - hp) |^ x0)) / (x0 !))) - ((((r - hp) |^ (x0 + 1)) / ((x0 + 1) !)) * (diff (((n,].r,x.[) . (x0 + 1)),hp))) is V22() real ext-real Element of REAL
1 * ((r - hp) |^ x0) is V22() real ext-real Element of REAL
(1 * ((r - hp) |^ x0)) / (x0 !) is V22() real ext-real Element of REAL
- ((1 * ((r - hp) |^ x0)) / (x0 !)) is V22() real ext-real Element of REAL
(((n,].r,x.[) . (x0 + 1)) . hp) * (- ((1 * ((r - hp) |^ x0)) / (x0 !))) is V22() real ext-real Element of REAL
((- (((((n,].r,x.[) . (x0 + 1)) . hp) * ((r - hp) |^ x0)) / (x0 !))) - ((((r - hp) |^ (x0 + 1)) / ((x0 + 1) !)) * (diff (((n,].r,x.[) . (x0 + 1)),hp)))) - ((((n,].r,x.[) . (x0 + 1)) . hp) * (- ((1 * ((r - hp) |^ x0)) / (x0 !)))) is V22() real ext-real Element of REAL
(((n,].r,x.[) . (x0 + 1)) . hp) * ((1 * ((r - hp) |^ x0)) / (x0 !)) is V22() real ext-real Element of REAL
(- (((((n,].r,x.[) . (x0 + 1)) . hp) * ((r - hp) |^ x0)) / (x0 !))) + ((((n,].r,x.[) . (x0 + 1)) . hp) * ((1 * ((r - hp) |^ x0)) / (x0 !))) is V22() real ext-real Element of REAL
((- (((((n,].r,x.[) . (x0 + 1)) . hp) * ((r - hp) |^ x0)) / (x0 !))) + ((((n,].r,x.[) . (x0 + 1)) . hp) * ((1 * ((r - hp) |^ x0)) / (x0 !)))) - ((((r - hp) |^ (x0 + 1)) / ((x0 + 1) !)) * (diff (((n,].r,x.[) . (x0 + 1)),hp))) is V22() real ext-real Element of REAL
(- (((((n,].r,x.[) . (x0 + 1)) . hp) * ((r - hp) |^ x0)) / (x0 !))) + (((((n,].r,x.[) . (x0 + 1)) . hp) * ((r - hp) |^ x0)) / (x0 !)) is V22() real ext-real Element of REAL
((- (((((n,].r,x.[) . (x0 + 1)) . hp) * ((r - hp) |^ x0)) / (x0 !))) + (((((n,].r,x.[) . (x0 + 1)) . hp) * ((r - hp) |^ x0)) / (x0 !))) - ((((r - hp) |^ (x0 + 1)) / ((x0 + 1) !)) * (diff (((n,].r,x.[) . (x0 + 1)),hp))) is V22() real ext-real Element of REAL
- ((((r - hp) |^ (x0 + 1)) / ((x0 + 1) !)) * (diff (((n,].r,x.[) . (x0 + 1)),hp))) is V22() real ext-real Element of REAL
((n,].r,x.[) . (x0 + 1)) `| ].r,x.[ is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
(((n,].r,x.[) . (x0 + 1)) `| ].r,x.[) . hp is V22() real ext-real Element of REAL
(((r - hp) |^ (x0 + 1)) / ((x0 + 1) !)) * ((((n,].r,x.[) . (x0 + 1)) `| ].r,x.[) . hp) is V22() real ext-real Element of REAL
- ((((r - hp) |^ (x0 + 1)) / ((x0 + 1) !)) * ((((n,].r,x.[) . (x0 + 1)) `| ].r,x.[) . hp)) is V22() real ext-real Element of REAL
((n,].r,x.[) . ((x0 + 1) + 1)) . hp is V22() real ext-real Element of REAL
(((r - hp) |^ (x0 + 1)) / ((x0 + 1) !)) * (((n,].r,x.[) . ((x0 + 1) + 1)) . hp) is V22() real ext-real Element of REAL
- ((((r - hp) |^ (x0 + 1)) / ((x0 + 1) !)) * (((n,].r,x.[) . ((x0 + 1) + 1)) . hp)) is V22() real ext-real Element of REAL
(((n,].r,x.[) . ((x0 + 1) + 1)) . hp) * ((r - hp) |^ (x0 + 1)) is V22() real ext-real Element of REAL
((((n,].r,x.[) . ((x0 + 1) + 1)) . hp) * ((r - hp) |^ (x0 + 1))) / ((x0 + 1) !) is V22() real ext-real Element of REAL
- (((((n,].r,x.[) . ((x0 + 1) + 1)) . hp) * ((r - hp) |^ (x0 + 1))) / ((x0 + 1) !)) is V22() real ext-real Element of REAL
hp is V22() real ext-real Element of REAL
diff (c,hp) is V22() real ext-real Element of REAL
((n,].r,x.[) . ((x0 + 1) + 1)) . hp is V22() real ext-real Element of REAL
r - hp is V22() real ext-real Element of REAL
(r - hp) |^ (x0 + 1) is V22() real ext-real Element of REAL
(((n,].r,x.[) . ((x0 + 1) + 1)) . hp) * ((r - hp) |^ (x0 + 1)) is V22() real ext-real Element of REAL
((((n,].r,x.[) . ((x0 + 1) + 1)) . hp) * ((r - hp) |^ (x0 + 1))) / ((x0 + 1) !) is V22() real ext-real Element of REAL
- (((((n,].r,x.[) . ((x0 + 1) + 1)) . hp) * ((r - hp) |^ (x0 + 1))) / ((x0 + 1) !)) is V22() real ext-real Element of REAL
c is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
dom c is V80() V81() V82() Element of K19(REAL)
c . r is V22() real ext-real Element of REAL
c | [.r,x.] is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
s is V22() real ext-real Element of REAL
diff (c,s) is V22() real ext-real Element of REAL
((n,].r,x.[) . ((x0 + 1) + 1)) . s is V22() real ext-real Element of REAL
r - s is V22() real ext-real Element of REAL
(r - s) |^ (x0 + 1) is V22() real ext-real Element of REAL
(((n,].r,x.[) . ((x0 + 1) + 1)) . s) * ((r - s) |^ (x0 + 1)) is V22() real ext-real Element of REAL
((((n,].r,x.[) . ((x0 + 1) + 1)) . s) * ((r - s) |^ (x0 + 1))) / ((x0 + 1) !) is V22() real ext-real Element of REAL
- (((((n,].r,x.[) . ((x0 + 1) + 1)) . s) * ((r - s) |^ (x0 + 1))) / ((x0 + 1) !)) is V22() real ext-real Element of REAL
(n,f) . 0 is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,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
r is V22() real ext-real Element of REAL
x0 is V22() real ext-real Element of REAL
[.x0,r.] is closed V80() V81() V82() V100() Element of K19(REAL)
((n,f) . 0) | [.x0,r.] is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
].x0,r.[ is open V80() V81() V82() V95() V96() V100() Element of K19(REAL)
n . x0 is V22() real ext-real Element of REAL
(n,].x0,r.[) is V1() V4( NAT ) V5( PFuncs (REAL,REAL)) Function-like non empty total quasi_total Element of K19(K20(NAT,(PFuncs (REAL,REAL))))
(n,].x0,r.[) . (0 + 1) is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,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)
x . x0 is V22() real ext-real Element of REAL
x | [.x0,r.] is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
(n,f,x0,x0) is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
Partial_Sums (n,f,x0,x0) is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
(Partial_Sums (n,f,x0,x0)) . 0 is V22() real ext-real Element of REAL
(n . x0) - ((Partial_Sums (n,f,x0,x0)) . 0) is V22() real ext-real Element of REAL
(n,f,x0,x0) . 0 is V22() real ext-real Element of REAL
(n . x0) - ((n,f,x0,x0) . 0) is V22() real ext-real Element of REAL
((n,f) . 0) . x0 is V22() real ext-real Element of REAL
x0 - x0 is V22() real ext-real Element of REAL
(x0 - x0) |^ 0 is V22() real ext-real Element of REAL
(((n,f) . 0) . x0) * ((x0 - x0) |^ 0) is V22() real ext-real Element of REAL
((((n,f) . 0) . x0) * ((x0 - x0) |^ 0)) / (0 !) is V22() real ext-real Element of REAL
(n . x0) - (((((n,f) . 0) . x0) * ((x0 - x0) |^ 0)) / (0 !)) is V22() real ext-real Element of REAL
n | f is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
(n | f) . x0 is V22() real ext-real Element of REAL
((n | f) . x0) * ((x0 - x0) |^ 0) is V22() real ext-real Element of REAL
(((n | f) . x0) * ((x0 - x0) |^ 0)) / (0 !) is V22() real ext-real Element of REAL
(n . x0) - ((((n | f) . x0) * ((x0 - x0) |^ 0)) / (0 !)) is V22() real ext-real Element of REAL
(n . x0) * ((x0 - x0) |^ 0) is V22() real ext-real Element of REAL
((n . x0) * ((x0 - x0) |^ 0)) / (0 !) is V22() real ext-real Element of REAL
(n . x0) - (((n . x0) * ((x0 - x0) |^ 0)) / (0 !)) is V22() real ext-real Element of REAL
(n . x0) * 1 is V22() real ext-real Element of REAL
(n . x0) - ((n . x0) * 1) is V22() real ext-real Element of REAL
t is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
dom t is V80() V81() V82() Element of K19(REAL)
rng n is V80() V81() V82() Element of K19(REAL)
t * n is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
dom (t * n) is V80() V81() V82() Element of K19(REAL)
c is V22() real ext-real Element of REAL
t | REAL is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
n .: [.x0,r.] is V80() V81() V82() Element of K19(REAL)
t | (n .: [.x0,r.]) is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
(0 + 1) - 1 is V22() real ext-real integer non irrational Element of REAL
(n,].x0,r.[) . 0 is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
n | ].x0,r.[ is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
c is V22() real ext-real Element of REAL
((n,].x0,r.[) . 0) `| ].x0,r.[ is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
(n | ].x0,r.[) `| ].x0,r.[ is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
n `| ].x0,r.[ is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
c is V22() real ext-real Element of REAL
diff ((t * n),c) is V22() real ext-real Element of REAL
((n,].x0,r.[) . (0 + 1)) . c is V22() real ext-real Element of REAL
x0 - c is V22() real ext-real Element of REAL
(x0 - c) |^ 0 is V22() real ext-real Element of REAL
(((n,].x0,r.[) . (0 + 1)) . c) * ((x0 - c) |^ 0) is V22() real ext-real Element of REAL
((((n,].x0,r.[) . (0 + 1)) . c) * ((x0 - c) |^ 0)) / (0 !) is V22() real ext-real Element of REAL
- (((((n,].x0,r.[) . (0 + 1)) . c) * ((x0 - c) |^ 0)) / (0 !)) is V22() real ext-real Element of REAL
n . c is V22() real ext-real Element of REAL
((x0 - c) |^ 0) / (0 !) is V22() real ext-real Element of REAL
diff (t,(n . c)) is V22() real ext-real Element of REAL
diff (n,c) is V22() real ext-real Element of REAL
(diff (t,(n . c))) * (diff (n,c)) is V22() real ext-real Element of REAL
(n `| ].x0,r.[) . c is V22() real ext-real Element of REAL
(diff (t,(n . c))) * ((n `| ].x0,r.[) . c) is V22() real ext-real Element of REAL
(- 1) * (((n,].x0,r.[) . (0 + 1)) . c) is V22() real ext-real Element of REAL
(((n,].x0,r.[) . (0 + 1)) . c) * (((x0 - c) |^ 0) / (0 !)) is V22() real ext-real Element of REAL
- ((((n,].x0,r.[) . (0 + 1)) . c) * (((x0 - c) |^ 0) / (0 !))) is V22() real ext-real Element of REAL
c is V22() real ext-real Element of REAL
(t * n) | [.x0,r.] is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
dom ((t * n) | [.x0,r.]) is V80() V81() V82() Element of K19(REAL)
(dom (t * n)) /\ [.x0,r.] is V80() V81() V82() Element of K19(REAL)
f /\ [.x0,r.] is V80() V81() V82() Element of K19(REAL)
dom (x | [.x0,r.]) is V80() V81() V82() Element of K19(REAL)
c is set
(dom x) /\ [.x0,r.] is V80() V81() V82() Element of K19(REAL)
s is V22() real ext-real Element of REAL
(x | [.x0,r.]) . c is V22() real ext-real Element of REAL
x . s is V22() real ext-real Element of REAL
(n,f,s,x0) is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
Partial_Sums (n,f,s,x0) is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
(Partial_Sums (n,f,s,x0)) . 0 is V22() real ext-real Element of REAL
(n . x0) - ((Partial_Sums (n,f,s,x0)) . 0) is V22() real ext-real Element of REAL
(n,f,s,x0) . 0 is V22() real ext-real Element of REAL
(n . x0) - ((n,f,s,x0) . 0) is V22() real ext-real Element of REAL
((n,f) . 0) . s is V22() real ext-real Element of REAL
x0 - s is V22() real ext-real Element of REAL
(x0 - s) |^ 0 is V22() real ext-real Element of REAL
(((n,f) . 0) . s) * ((x0 - s) |^ 0) is V22() real ext-real Element of REAL
((((n,f) . 0) . s) * ((x0 - s) |^ 0)) / (0 !) is V22() real ext-real Element of REAL
(n . x0) - (((((n,f) . 0) . s) * ((x0 - s) |^ 0)) / (0 !)) is V22() real ext-real Element of REAL
(n | f) . s is V22() real ext-real Element of REAL
((n | f) . s) * ((x0 - s) |^ 0) is V22() real ext-real Element of REAL
(((n | f) . s) * ((x0 - s) |^ 0)) / (0 !) is V22() real ext-real Element of REAL
(n . x0) - ((((n | f) . s) * ((x0 - s) |^ 0)) / (0 !)) is V22() real ext-real Element of REAL
n . s is V22() real ext-real Element of REAL
(n . s) * ((x0 - s) |^ 0) is V22() real ext-real Element of REAL
((n . s) * ((x0 - s) |^ 0)) / (0 !) is V22() real ext-real Element of REAL
(n . x0) - (((n . s) * ((x0 - s) |^ 0)) / (0 !)) is V22() real ext-real Element of REAL
(n . s) * 1 is V22() real ext-real Element of REAL
(n . x0) - ((n . s) * 1) is V22() real ext-real Element of REAL
t . (n . s) is V22() real ext-real Element of REAL
(t * n) . s is V22() real ext-real Element of REAL
((t * n) | [.x0,r.]) . c is V22() real ext-real Element of REAL
(n | f) | [.x0,r.] is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
((n | f) | [.x0,r.]) | [.x0,r.] is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
n | [.x0,r.] is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
(n | [.x0,r.]) | [.x0,r.] is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
(t * n) | ].x0,r.[ is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
dom ((t * n) | ].x0,r.[) is V80() V81() V82() Element of K19(REAL)
(dom (t * n)) /\ ].x0,r.[ is V80() V81() V82() Element of K19(REAL)
f /\ ].x0,r.[ is V80() V81() V82() Element of K19(REAL)
x | ].x0,r.[ is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
dom (x | ].x0,r.[) is V80() V81() V82() Element of K19(REAL)
c is set
(dom x) /\ ].x0,r.[ is V80() V81() V82() Element of K19(REAL)
s is V22() real ext-real Element of REAL
x0 - s is V22() real ext-real Element of REAL
(x0 - s) |^ 0 is V22() real ext-real Element of REAL
((x0 - s) |^ 0) / (0 !) is V22() real ext-real Element of REAL
(x | ].x0,r.[) . c is V22() real ext-real Element of REAL
x . s is V22() real ext-real Element of REAL
(n,f,s,x0) is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
Partial_Sums (n,f,s,x0) is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
(Partial_Sums (n,f,s,x0)) . 0 is V22() real ext-real Element of REAL
(n . x0) - ((Partial_Sums (n,f,s,x0)) . 0) is V22() real ext-real Element of REAL
(n,f,s,x0) . 0 is V22() real ext-real Element of REAL
(n . x0) - ((n,f,s,x0) . 0) is V22() real ext-real Element of REAL
((n,f) . 0) . s is V22() real ext-real Element of REAL
(((n,f) . 0) . s) * ((x0 - s) |^ 0) is V22() real ext-real Element of REAL
((((n,f) . 0) . s) * ((x0 - s) |^ 0)) / (0 !) is V22() real ext-real Element of REAL
(n . x0) - (((((n,f) . 0) . s) * ((x0 - s) |^ 0)) / (0 !)) is V22() real ext-real Element of REAL
(n | f) . s is V22() real ext-real Element of REAL
((n | f) . s) * ((x0 - s) |^ 0) is V22() real ext-real Element of REAL
(((n | f) . s) * ((x0 - s) |^ 0)) / (0 !) is V22() real ext-real Element of REAL
(n . x0) - ((((n | f) . s) * ((x0 - s) |^ 0)) / (0 !)) is V22() real ext-real Element of REAL
n . s is V22() real ext-real Element of REAL
(n . s) * ((x0 - s) |^ 0) is V22() real ext-real Element of REAL
((n . s) * ((x0 - s) |^ 0)) / (0 !) is V22() real ext-real Element of REAL
(n . x0) - (((n . s) * ((x0 - s) |^ 0)) / (0 !)) is V22() real ext-real Element of REAL
(n . s) * (((x0 - s) |^ 0) / (0 !)) is V22() real ext-real Element of REAL
(n . x0) - ((n . s) * (((x0 - s) |^ 0) / (0 !))) is V22() real ext-real Element of REAL
t . (n . s) is V22() real ext-real Element of REAL
(t * n) . s is V22() real ext-real Element of REAL
((t * n) | ].x0,r.[) . c is V22() real ext-real Element of REAL
c is V22() real ext-real Element of REAL
c is V22() real ext-real Element of REAL
diff (x,c) is V22() real ext-real Element of REAL
x `| ].x0,r.[ is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
(x `| ].x0,r.[) . c is V22() real ext-real Element of REAL
(x | ].x0,r.[) `| ].x0,r.[ is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
((x | ].x0,r.[) `| ].x0,r.[) . c is V22() real ext-real Element of REAL
(t * n) `| ].x0,r.[ is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
((t * n) `| ].x0,r.[) . c is V22() real ext-real Element of REAL
diff ((t * n),c) is V22() real ext-real Element of REAL
((n,].x0,r.[) . (0 + 1)) . c is V22() real ext-real Element of REAL
x0 - c is V22() real ext-real Element of REAL
(x0 - c) |^ 0 is V22() real ext-real Element of REAL
(((n,].x0,r.[) . (0 + 1)) . c) * ((x0 - c) |^ 0) is V22() real ext-real Element of REAL
((((n,].x0,r.[) . (0 + 1)) . c) * ((x0 - c) |^ 0)) / (0 !) is V22() real ext-real Element of REAL
- (((((n,].x0,r.[) . (0 + 1)) . c) * ((x0 - c) |^ 0)) / (0 !)) is V22() real ext-real Element of REAL
c is V22() real ext-real Element of REAL
diff (x,c) is V22() real ext-real Element of REAL
((n,].x0,r.[) . (0 + 1)) . c is V22() real ext-real Element of REAL
x0 - c is V22() real ext-real Element of REAL
(x0 - c) |^ 0 is V22() real ext-real Element of REAL
(((n,].x0,r.[) . (0 + 1)) . c) * ((x0 - c) |^ 0) is V22() real ext-real Element of REAL
((((n,].x0,r.[) . (0 + 1)) . c) * ((x0 - c) |^ 0)) / (0 !) is V22() real ext-real Element of REAL
- (((((n,].x0,r.[) . (0 + 1)) . c) * ((x0 - c) |^ 0)) / (0 !)) 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 V80() V81() V82() V83() V84() V85() V97() Element of NAT
x is V22() real ext-real Element of REAL
r is V22() real ext-real Element of REAL
[.r,x.] is closed V80() V81() V82() V100() Element of K19(REAL)
(n,f) . x0 is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
((n,f) . x0) | [.r,x.] is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,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
].r,x.[ is open V80() V81() V82() V95() V96() V100() Element of K19(REAL)
t is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
dom t is V80() V81() V82() Element of K19(REAL)
n . r is V22() real ext-real Element of REAL
t . r is V22() real ext-real Element of REAL
t | [.r,x.] is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
c is V22() real ext-real Element of REAL
diff (t,c) is V22() real ext-real Element of REAL
(n,].r,x.[) is V1() V4( NAT ) V5( PFuncs (REAL,REAL)) Function-like non empty total quasi_total Element of K19(K20(NAT,(PFuncs (REAL,REAL))))
(n,].r,x.[) . (x0 + 1) is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
((n,].r,x.[) . (x0 + 1)) . c is V22() real ext-real Element of REAL
r - c is V22() real ext-real Element of REAL
(r - c) |^ x0 is V22() real ext-real Element of REAL
(((n,].r,x.[) . (x0 + 1)) . c) * ((r - c) |^ x0) is V22() real ext-real Element of REAL
x0 ! is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative integer non irrational Element of REAL
((((n,].r,x.[) . (x0 + 1)) . c) * ((r - c) |^ x0)) / (x0 !) is V22() real ext-real Element of REAL
- (((((n,].r,x.[) . (x0 + 1)) . c) * ((r - c) |^ x0)) / (x0 !)) 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 ! is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative integer non irrational 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 V80() V81() V82() Element of K19(REAL)
(f,x0) is V1() V4( NAT ) V5( PFuncs (REAL,REAL)) Function-like non empty total quasi_total Element of K19(K20(NAT,(PFuncs (REAL,REAL))))
(f,x0) . n is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
x is V22() real ext-real Element of REAL
r is V22() real ext-real Element of REAL
[.r,x.] is closed V80() V81() V82() V100() Element of K19(REAL)
((f,x0) . n) | [.r,x.] is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
].r,x.[ is open V80() V81() V82() V95() V96() V100() Element of K19(REAL)
f . r is V22() real ext-real Element of REAL
(f,].r,x.[) is V1() V4( NAT ) V5( PFuncs (REAL,REAL)) Function-like non empty total quasi_total Element of K19(K20(NAT,(PFuncs (REAL,REAL))))
(f,].r,x.[) . (n + 1) is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
t is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
dom t is V80() V81() V82() Element of K19(REAL)
t . r is V22() real ext-real Element of REAL
t | [.r,x.] is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
c is V22() real ext-real Element of REAL
t . c is V22() real ext-real Element of REAL
(f,x0,c,r) is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
Partial_Sums (f,x0,c,r) is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
(Partial_Sums (f,x0,c,r)) . n is V22() real ext-real Element of REAL
(f . r) - ((Partial_Sums (f,x0,c,r)) . n) is V22() real ext-real Element of REAL
s is V22() real ext-real Element of REAL
diff (t,s) is V22() real ext-real Element of REAL
((f,].r,x.[) . (n + 1)) . s is V22() real ext-real Element of REAL
r - s is V22() real ext-real Element of REAL
(r - s) |^ n is V22() real ext-real Element of REAL
(((f,].r,x.[) . (n + 1)) . s) * ((r - s) |^ n) is V22() real ext-real Element of REAL
((((f,].r,x.[) . (n + 1)) . s) * ((r - s) |^ n)) / (n !) is V22() real ext-real Element of REAL
- (((((f,].r,x.[) . (n + 1)) . s) * ((r - s) |^ n)) / (n !)) 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 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 V80() V81() V82() Element of K19(REAL)
(f,x0) is V1() V4( NAT ) V5( PFuncs (REAL,REAL)) Function-like non empty total quasi_total Element of K19(K20(NAT,(PFuncs (REAL,REAL))))
(f,x0) . n is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
x is V22() real ext-real Element of REAL
r is V22() real ext-real Element of REAL
[.r,x.] is closed V80() V81() V82() V100() Element of K19(REAL)
((f,x0) . n) | [.r,x.] is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
].r,x.[ is open V80() V81() V82() V95() V96() V100() Element of K19(REAL)
f . r is V22() real ext-real Element of REAL
(f,x0,x,r) is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
Partial_Sums (f,x0,x,r) is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
(Partial_Sums (f,x0,x,r)) . n is V22() real ext-real Element of REAL
(f . r) - ((Partial_Sums (f,x0,x,r)) . n) is V22() real ext-real Element of REAL
r - x is V22() real ext-real Element of REAL
(r - x) |^ (n + 1) is V22() real ext-real Element of REAL
(f,].r,x.[) is V1() V4( NAT ) V5( PFuncs (REAL,REAL)) Function-like non empty total quasi_total Element of K19(K20(NAT,(PFuncs (REAL,REAL))))
(f,].r,x.[) . (n + 1) is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
t is V22() real ext-real Element of REAL
t * ((r - x) |^ (n + 1)) is V22() real ext-real Element of REAL
(t * ((r - x) |^ (n + 1))) / ((n + 1) !) is V22() real ext-real Element of REAL
((f . r) - ((Partial_Sums (f,x0,x,r)) . n)) - ((t * ((r - x) |^ (n + 1))) / ((n + 1) !)) is V22() real ext-real Element of REAL
c is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
dom c is V80() V81() V82() Element of K19(REAL)
s is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
dom s is V80() V81() V82() Element of K19(REAL)
s . r is V22() real ext-real Element of REAL
s | [.r,x.] is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
(dom s) /\ (dom c) is V80() V81() V82() Element of K19(REAL)
g is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
dom g is V80() V81() V82() Element of K19(REAL)
g . x is V22() real ext-real Element of REAL
g . r is V22() real ext-real Element of REAL
g | [.r,x.] is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
s - c is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
dom (s - c) is V80() V81() V82() Element of K19(REAL)
x is set
(s - c) . x is V22() real ext-real Element of REAL
g . x is V22() real ext-real Element of REAL
xx is V22() real ext-real Element of REAL
s . xx is V22() real ext-real Element of REAL
c . xx is V22() real ext-real Element of REAL
(s . xx) - (c . xx) is V22() real ext-real Element of REAL
(f,x0,xx,r) is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
Partial_Sums (f,x0,xx,r) is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
(Partial_Sums (f,x0,xx,r)) . n is V22() real ext-real Element of REAL
(f . r) - ((Partial_Sums (f,x0,xx,r)) . n) is V22() real ext-real Element of REAL
((f . r) - ((Partial_Sums (f,x0,xx,r)) . n)) - (c . xx) is V22() real ext-real Element of REAL
r - xx is V22() real ext-real Element of REAL
(r - xx) |^ (n + 1) is V22() real ext-real Element of REAL
t * ((r - xx) |^ (n + 1)) is V22() real ext-real Element of REAL
(t * ((r - xx) |^ (n + 1))) / ((n + 1) !) is V22() real ext-real Element of REAL
((f . r) - ((Partial_Sums (f,x0,xx,r)) . n)) - ((t * ((r - xx) |^ (n + 1))) / ((n + 1) !)) is V22() real ext-real Element of REAL
x is V22() real ext-real Element of REAL
c | REAL is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
c | [.r,x.] is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
(dom g) /\ x0 is V80() V81() V82() Element of K19(REAL)
(s - c) | ].r,x.[ is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
g | x0 is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
(g | x0) | ].r,x.[ is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
g | ].r,x.[ is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
x is V22() real ext-real Element of REAL
diff ((s - c),x) is V22() real ext-real Element of REAL
((f,].r,x.[) . (n + 1)) . x is V22() real ext-real Element of REAL
r - x is V22() real ext-real Element of REAL
(r - x) |^ n is V22() real ext-real Element of REAL
(((f,].r,x.[) . (n + 1)) . x) * ((r - x) |^ n) is V22() real ext-real Element of REAL
((((f,].r,x.[) . (n + 1)) . x) * ((r - x) |^ n)) / (n !) is V22() real ext-real Element of REAL
- (((((f,].r,x.[) . (n + 1)) . x) * ((r - x) |^ n)) / (n !)) is V22() real ext-real Element of REAL
t * ((r - x) |^ n) is V22() real ext-real Element of REAL
(t * ((r - x) |^ n)) / (n !) is V22() real ext-real Element of REAL
(- (((((f,].r,x.[) . (n + 1)) . x) * ((r - x) |^ n)) / (n !))) + ((t * ((r - x) |^ n)) / (n !)) is V22() real ext-real Element of REAL
diff (s,x) is V22() real ext-real Element of REAL
diff (c,x) is V22() real ext-real Element of REAL
(diff (s,x)) - (diff (c,x)) is V22() real ext-real Element of REAL
(- (((((f,].r,x.[) . (n + 1)) . x) * ((r - x) |^ n)) / (n !))) - (diff (c,x)) is V22() real ext-real Element of REAL
- ((t * ((r - x) |^ n)) / (n !)) is V22() real ext-real Element of REAL
(- (((((f,].r,x.[) . (n + 1)) . x) * ((r - x) |^ n)) / (n !))) - (- ((t * ((r - x) |^ n)) / (n !))) 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
(s - c) . r is V22() real ext-real Element of REAL
c . r is V22() real ext-real Element of REAL
(s . r) - (c . r) is V22() real ext-real Element of REAL
r - r is V22() real ext-real Element of REAL
(r - r) |^ (n + 1) is V22() real ext-real Element of REAL
t * ((r - r) |^ (n + 1)) is V22() real ext-real Element of REAL
(t * ((r - r) |^ (n + 1))) / ((n + 1) !) is V22() real ext-real Element of REAL
0 - ((t * ((r - r) |^ (n + 1))) / ((n + 1) !)) is V22() real ext-real Element of REAL
0 |^ 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
(0 |^ n) * 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
t * ((0 |^ n) * 0) is V22() real ext-real Element of REAL
(t * ((0 |^ n) * 0)) / ((n + 1) !) is V22() real ext-real Element of REAL
0 - ((t * ((0 |^ n) * 0)) / ((n + 1) !)) is V22() real ext-real Element of REAL
(s - c) | [.r,x.] is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
(g | x0) | [.r,x.] is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
x is V22() real ext-real Element of REAL
diff (g,x) is V22() real ext-real Element of REAL
((f,].r,x.[) . (n + 1)) . x is V22() real ext-real Element of REAL
r - x is V22() real ext-real Element of REAL
(r - x) |^ n is V22() real ext-real Element of REAL
(((f,].r,x.[) . (n + 1)) . x) * ((r - x) |^ n) is V22() real ext-real Element of REAL
((((f,].r,x.[) . (n + 1)) . x) * ((r - x) |^ n)) / (n !) is V22() real ext-real Element of REAL
- (((((f,].r,x.[) . (n + 1)) . x) * ((r - x) |^ n)) / (n !)) is V22() real ext-real Element of REAL
t * ((r - x) |^ n) is V22() real ext-real Element of REAL
(t * ((r - x) |^ n)) / (n !) is V22() real ext-real Element of REAL
(- (((((f,].r,x.[) . (n + 1)) . x) * ((r - x) |^ n)) / (n !))) + ((t * ((r - x) |^ n)) / (n !)) is V22() real ext-real Element of REAL
g `| ].r,x.[ is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
(g `| ].r,x.[) . x is V22() real ext-real Element of REAL
(g | ].r,x.[) `| ].r,x.[ is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
((g | ].r,x.[) `| ].r,x.[) . x is V22() real ext-real Element of REAL
(s - c) `| ].r,x.[ is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
((s - c) `| ].r,x.[) . x is V22() real ext-real Element of REAL
diff ((s - c),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
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 V80() V81() V82() Element of K19(REAL)
(f,x0) is V1() V4( NAT ) V5( PFuncs (REAL,REAL)) Function-like non empty total quasi_total Element of K19(K20(NAT,(PFuncs (REAL,REAL))))
(f,x0) . n is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
x is V22() real ext-real Element of REAL
r is V22() real ext-real Element of REAL
[.r,x.] is closed V80() V81() V82() V100() Element of K19(REAL)
((f,x0) . n) | [.r,x.] is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
].r,x.[ is open V80() V81() V82() V95() V96() V100() Element of K19(REAL)
f . r is V22() real ext-real Element of REAL
(f,x0,x,r) is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
Partial_Sums (f,x0,x,r) is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
(Partial_Sums (f,x0,x,r)) . n is V22() real ext-real Element of REAL
(f,].r,x.[) is V1() V4( NAT ) V5( PFuncs (REAL,REAL)) Function-like non empty total quasi_total Element of K19(K20(NAT,(PFuncs (REAL,REAL))))
(f,].r,x.[) . (n + 1) is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
r - x is V22() real ext-real Element of REAL
(r - x) |^ (n + 1) is V22() real ext-real Element of REAL
(f . r) - ((Partial_Sums (f,x0,x,r)) . n) is V22() real ext-real Element of REAL
((r - x) |^ (n + 1)) / ((n + 1) !) is V22() real ext-real Element of REAL
H₁(x) / (((r - x) |^ (n + 1)) / ((n + 1) !)) is V22() real ext-real Element of REAL
t is V22() real ext-real Element of REAL
c is V1() V4( REAL ) V5( REAL ) Function-like non empty total quasi_total V33() V34() V35() Element of K19(K20(REAL,REAL))
t * ((r - x) |^ (n + 1)) is V22() real ext-real Element of REAL
(t * ((r - x) |^ (n + 1))) / ((n + 1) !) is V22() real ext-real Element of REAL
((f . r) - ((Partial_Sums (f,x0,x,r)) . n)) - ((t * ((r - x) |^ (n + 1))) / ((n + 1) !)) is V22() real ext-real Element of REAL
(H₁(x) / (((r - x) |^ (n + 1)) / ((n + 1) !))) * (((r - x) |^ (n + 1)) / ((n + 1) !)) is V22() real ext-real Element of REAL
H₁(x) - ((H₁(x) / (((r - x) |^ (n + 1)) / ((n + 1) !))) * (((r - x) |^ (n + 1)) / ((n + 1) !))) is V22() real ext-real Element of REAL
H₁(x) - H₁(x) is V22() real ext-real Element of REAL
c . x is V22() real ext-real Element of REAL
dom c is V80() V81() V82() Element of K19(REAL)
c | [.r,x.] is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
c . r is V22() real ext-real Element of REAL
s is V22() real ext-real Element of REAL
diff (c,s) is V22() real ext-real Element of REAL
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( not b₁ <= r & not x <= b₁ ) } is set
r - s is V22() real ext-real Element of REAL
g is V22() real ext-real Element of REAL
(r - s) |^ n is V22() real ext-real Element of REAL
((f,].r,x.[) . (n + 1)) . s is V22() real ext-real Element of REAL
(((f,].r,x.[) . (n + 1)) . s) * ((r - s) |^ n) is V22() real ext-real 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,].r,x.[) . (n + 1)) . s) * ((r - s) |^ n)) / (n !) is V22() real ext-real Element of REAL
- (((((f,].r,x.[) . (n + 1)) . s) * ((r - s) |^ n)) / (n !)) is V22() real ext-real Element of REAL
t * ((r - s) |^ n) is V22() real ext-real Element of REAL
(t * ((r - s) |^ n)) / (n !) is V22() real ext-real Element of REAL
(- (((((f,].r,x.[) . (n + 1)) . s) * ((r - s) |^ n)) / (n !))) + ((t * ((r - s) |^ n)) / (n !)) is V22() real ext-real Element of REAL
(((((f,].r,x.[) . (n + 1)) . s) * ((r - s) |^ n)) / (n !)) * (n !) is V22() real ext-real Element of REAL
((t * ((r - s) |^ n)) / (n !)) * (n !) is V22() real ext-real Element of REAL
((((((f,].r,x.[) . (n + 1)) . s) * ((r - s) |^ n)) / (n !)) * (n !)) - (((t * ((r - s) |^ n)) / (n !)) * (n !)) is V22() real ext-real Element of REAL
((((f,].r,x.[) . (n + 1)) . s) * ((r - s) |^ n)) - (((t * ((r - s) |^ n)) / (n !)) * (n !)) is V22() real ext-real Element of REAL
((((f,].r,x.[) . (n + 1)) . s) * ((r - s) |^ n)) - (t * ((r - s) |^ n)) is V22() real ext-real Element of REAL
(((((f,].r,x.[) . (n + 1)) . s) * ((r - s) |^ n)) - (t * ((r - s) |^ n))) / ((r - s) |^ n) is V22() real ext-real Element of REAL
0 / ((r - s) |^ n) is V22() real ext-real Element of REAL
((((f,].r,x.[) . (n + 1)) . s) * ((r - s) |^ n)) / ((r - s) |^ n) is V22() real ext-real Element of REAL
(t * ((r - s) |^ n)) / ((r - s) |^ n) is V22() real ext-real Element of REAL
(((((f,].r,x.[) . (n + 1)) . s) * ((r - s) |^ n)) / ((r - s) |^ n)) - ((t * ((r - s) |^ n)) / ((r - s) |^ n)) is V22() real ext-real Element of REAL
(((f,].r,x.[) . (n + 1)) . s) - ((t * ((r - s) |^ n)) / ((r - s) |^ n)) is V22() real ext-real Element of REAL
(((f,].r,x.[) . (n + 1)) . s) * ((r - x) |^ (n + 1)) is V22() real ext-real Element of REAL
((((f,].r,x.[) . (n + 1)) . s) * ((r - x) |^ (n + 1))) / ((n + 1) !) is V22() real ext-real Element of REAL
(((((f,].r,x.[) . (n + 1)) . s) * ((r - x) |^ (n + 1))) / ((n + 1) !)) + ((Partial_Sums (f,x0,x,r)) . n) is V22() real ext-real Element of 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 open V80() V81() V82() Element of K19(REAL)
(n,x0) is V1() V4( NAT ) V5( PFuncs (REAL,REAL)) Function-like non empty total quasi_total Element of K19(K20(NAT,(PFuncs (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
(n,f) . r is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
((n,f) . r) | x0 is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
(n,x0) . r is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,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
(n,f) . (r + 1) is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
((n,f) . (r + 1)) | x0 is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
(n,x0) . (r + 1) is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
(r + 1) - 1 is V22() real ext-real integer non irrational Element of REAL
((n,f) . r) `| x0 is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
dom (((n,f) . r) `| x0) is V80() V81() V82() Element of K19(REAL)
((n,f) . r) `| f is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
(((n,f) . r) `| f) | x0 is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
dom ((((n,f) . r) `| f) | x0) is V80() V81() V82() Element of K19(REAL)
dom (((n,f) . r) `| f) is V80() V81() V82() Element of K19(REAL)
(dom (((n,f) . r) `| f)) /\ x0 is V80() V81() V82() Element of K19(REAL)
f /\ x0 is V80() V81() V82() Element of K19(REAL)
x is V22() real ext-real Element of REAL
((((n,f) . r) `| f) | x0) . x is V22() real ext-real Element of REAL
(((n,f) . r) `| f) . x is V22() real ext-real Element of REAL
diff (((n,f) . r),x) is V22() real ext-real Element of REAL
(((n,f) . r) `| x0) . x is V22() real ext-real Element of REAL
((n,x0) . r) `| x0 is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
(n,f) . 0 is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
((n,f) . 0) | x0 is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
(n,x0) . 0 is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
n | f is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
(n | f) | 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))
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 open V80() V81() V82() Element of K19(REAL)
r is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative integer non irrational 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 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
(r + 1) - 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,(PFuncs (REAL,REAL))))
(n,f) . x is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
((n,f) . x) | x0 is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
(n,x0) is V1() V4( NAT ) V5( PFuncs (REAL,REAL)) Function-like non empty total quasi_total Element of K19(K20(NAT,(PFuncs (REAL,REAL))))
(n,x0) . 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)
x0 is V22() real ext-real Element of REAL
n . x0 is V22() real ext-real Element of REAL
(n,f,x0,x0) is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
Partial_Sums (n,f,x0,x0) is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total V33() V34() V35() Element of K19(K20(NAT,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
(Partial_Sums (n,f,x0,x0)) . r 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
(Partial_Sums (n,f,x0,x0)) . (r + 1) is V22() real ext-real Element of REAL
(n,f,x0,x0) . (r + 1) is V22() real ext-real Element of REAL
((Partial_Sums (n,f,x0,x0)) . r) + ((n,f,x0,x0) . (r + 1)) is V22() real ext-real 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,(PFuncs (REAL,REAL))))
(n,f) . (r + 1) is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
((n,f) . (r + 1)) . x0 is V22() real ext-real Element of REAL
x0 - x0 is V22() real ext-real Element of REAL
(x0 - x0) |^ (r + 1) is V22() real ext-real Element of REAL
(((n,f) . (r + 1)) . x0) * ((x0 - x0) |^ (r + 1)) 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 Element of REAL
((((n,f) . (r + 1)) . x0) * ((x0 - x0) |^ (r + 1))) / ((r + 1) !) is V22() real ext-real Element of REAL
(n . x0) + (((((n,f) . (r + 1)) . x0) * ((x0 - x0) |^ (r + 1))) / ((r + 1) !)) is V22() real ext-real Element of REAL
0 |^ 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
(0 |^ r) * 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,f) . (r + 1)) . x0) * ((0 |^ r) * 0) is V22() real ext-real Element of REAL
((((n,f) . (r + 1)) . x0) * ((0 |^ r) * 0)) / ((r + 1) !) is V22() real ext-real Element of REAL
(n . x0) + (((((n,f) . (r + 1)) . x0) * ((0 |^ r) * 0)) / ((r + 1) !)) is V22() real ext-real Element of REAL
(Partial_Sums (n,f,x0,x0)) . 0 is V22() real ext-real Element of REAL
(n,f,x0,x0) . 0 is V22() real ext-real 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,(PFuncs (REAL,REAL))))
(n,f) . 0 is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
((n,f) . 0) . x0 is V22() real ext-real Element of REAL
x0 - x0 is V22() real ext-real Element of REAL
(x0 - x0) |^ 0 is V22() real ext-real Element of REAL
(((n,f) . 0) . x0) * ((x0 - x0) |^ 0) is V22() real ext-real Element of REAL
((((n,f) . 0) . x0) * ((x0 - x0) |^ 0)) / (0 !) is V22() real ext-real Element of REAL
n | f is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
(n | f) . x0 is V22() real ext-real Element of REAL
((n | f) . x0) * ((x0 - x0) |^ 0) is V22() real ext-real Element of REAL
(((n | f) . x0) * ((x0 - x0) |^ 0)) / (0 !) is V22() real ext-real Element of REAL
((n | f) . x0) * 1 is V22() real ext-real Element of REAL
(((n | f) . x0) * 1) / 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
(Partial_Sums (n,f,x0,x0)) . r 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
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 V22() real ext-real Element of REAL
r is V22() real ext-real Element of REAL
x0 - r is V22() real ext-real Element of REAL
x0 + r is V22() real ext-real Element of REAL
].(x0 - r),(x0 + r).[ is open V80() V81() V82() V95() V96() V100() Element of K19(REAL)
(f,].(x0 - r),(x0 + r).[) is V1() V4( NAT ) V5( PFuncs (REAL,REAL)) Function-like non empty total quasi_total Element of K19(K20(NAT,(PFuncs (REAL,REAL))))
(f,].(x0 - r),(x0 + r).[) . (n + 1) is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
x is V22() real ext-real Element of REAL
f . x is V22() real ext-real Element of REAL
(f,].(x0 - r),(x0 + r).[,x0,x) is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
Partial_Sums (f,].(x0 - r),(x0 + r).[,x0,x) is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
(Partial_Sums (f,].(x0 - r),(x0 + r).[,x0,x)) . n is V22() real ext-real Element of REAL
x - x0 is V22() real ext-real Element of REAL
(x - x0) |^ (n + 1) is V22() real ext-real Element of REAL
x0 - x0 is V22() real ext-real Element of REAL
abs (x0 - x0) is V22() real ext-real Element of REAL
[.x,x0.] is closed V80() V81() V82() V100() Element of K19(REAL)
(n + 1) - 1 is V22() real ext-real integer non irrational Element of REAL
(f,].(x0 - r),(x0 + r).[) . n is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
((f,].(x0 - r),(x0 + r).[) . n) | ].(x0 - r),(x0 + r).[ is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
((f,].(x0 - r),(x0 + r).[) . n) | [.x,x0.] is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
x0 - x is V22() real ext-real Element of REAL
].x,x0.[ is open V80() V81() V82() V95() V96() V100() Element of K19(REAL)
(f,].x,x0.[) is V1() V4( NAT ) V5( PFuncs (REAL,REAL)) Function-like non empty total quasi_total Element of K19(K20(NAT,(PFuncs (REAL,REAL))))
(f,].x,x0.[) . (n + 1) is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
c is V22() real ext-real Element of REAL
((f,].x,x0.[) . (n + 1)) . c is V22() real ext-real Element of REAL
(((f,].x,x0.[) . (n + 1)) . c) * ((x - x0) |^ (n + 1)) is V22() real ext-real Element of REAL
((((f,].x,x0.[) . (n + 1)) . c) * ((x - x0) |^ (n + 1))) / ((n + 1) !) is V22() real ext-real Element of REAL
((Partial_Sums (f,].(x0 - r),(x0 + r).[,x0,x)) . n) + (((((f,].x,x0.[) . (n + 1)) . c) * ((x - x0) |^ (n + 1))) / ((n + 1) !)) is V22() real ext-real Element of REAL
x0 - c is V22() real ext-real Element of REAL
(x0 - c) / (x0 - x) is V22() real ext-real Element of REAL
s is V22() real ext-real Element of REAL
s * (x - x0) is V22() real ext-real Element of REAL
x0 + (s * (x - x0)) is V22() real ext-real Element of REAL
((x0 - c) / (x0 - x)) * (x0 - x) is V22() real ext-real Element of REAL
x0 - (((x0 - c) / (x0 - x)) * (x0 - x)) is V22() real ext-real Element of REAL
x0 - (x0 - c) is V22() real ext-real Element of REAL
x0 - (x0 - x) is V22() real ext-real Element of REAL
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( not b₁ <= x0 - (x0 - x) & not x0 <= b₁ ) } is set
g is V22() real ext-real Element of REAL
0 / (x0 - x) is V22() real ext-real Element of REAL
c + (x0 - x) is V22() real ext-real Element of REAL
(x0 - (x0 - x)) + (x0 - x) is V22() real ext-real Element of REAL
g is V22() real ext-real Element of REAL
(x0 - x) / (x0 - x) is V22() real ext-real Element of REAL
((f,].(x0 - r),(x0 + r).[) . (n + 1)) | ].x,x0.[ is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
(((f,].(x0 - r),(x0 + r).[) . (n + 1)) | ].x,x0.[) . c is V22() real ext-real Element of REAL
((f,].(x0 - r),(x0 + r).[) . (n + 1)) . c is V22() real ext-real Element of REAL
((f,].(x0 - r),(x0 + r).[) . (n + 1)) . (x0 + (s * (x - x0))) is V22() real ext-real Element of REAL
(((f,].(x0 - r),(x0 + r).[) . (n + 1)) . (x0 + (s * (x - x0)))) * ((x - x0) |^ (n + 1)) is V22() real ext-real Element of REAL
((((f,].(x0 - r),(x0 + r).[) . (n + 1)) . (x0 + (s * (x - x0)))) * ((x - x0) |^ (n + 1))) / ((n + 1) !) is V22() real ext-real Element of REAL
((Partial_Sums (f,].(x0 - r),(x0 + r).[,x0,x)) . n) + (((((f,].(x0 - r),(x0 + r).[) . (n + 1)) . (x0 + (s * (x - x0)))) * ((x - x0) |^ (n + 1))) / ((n + 1) !)) is V22() real ext-real Element of REAL
1 / 2 is V22() real ext-real non negative non irrational Element of REAL
c is V22() real ext-real non negative non irrational Element of REAL
c * (x - x0) is V22() real ext-real Element of REAL
x0 + (c * (x - x0)) is V22() real ext-real Element of REAL
((f,].(x0 - r),(x0 + r).[) . (n + 1)) . (x0 + (c * (x - x0))) is V22() real ext-real Element of REAL
(((f,].(x0 - r),(x0 + r).[) . (n + 1)) . (x0 + (c * (x - x0)))) * ((x - x0) |^ (n + 1)) is V22() real ext-real Element of REAL
((((f,].(x0 - r),(x0 + r).[) . (n + 1)) . (x0 + (c * (x - x0)))) * ((x - x0) |^ (n + 1))) / ((n + 1) !) is V22() real ext-real Element of REAL
((Partial_Sums (f,].(x0 - r),(x0 + r).[,x0,x)) . n) + (((((f,].(x0 - r),(x0 + r).[) . (n + 1)) . (x0 + (c * (x - x0)))) * ((x - x0) |^ (n + 1))) / ((n + 1) !)) is V22() real ext-real Element of REAL
x - x is V22() real ext-real Element of REAL
(x - x) |^ (n + 1) is V22() real ext-real Element of REAL
(((f,].(x0 - r),(x0 + r).[) . (n + 1)) . (x0 + (c * (x - x0)))) * ((x - x) |^ (n + 1)) is V22() real ext-real Element of REAL
((((f,].(x0 - r),(x0 + r).[) . (n + 1)) . (x0 + (c * (x - x0)))) * ((x - x) |^ (n + 1))) / ((n + 1) !) is V22() real ext-real Element of REAL
(f . x) + (((((f,].(x0 - r),(x0 + r).[) . (n + 1)) . (x0 + (c * (x - x0)))) * ((x - x) |^ (n + 1))) / ((n + 1) !)) is V22() real ext-real Element of REAL
0 |^ 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
(0 |^ n) * 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
(((f,].(x0 - r),(x0 + r).[) . (n + 1)) . (x0 + (c * (x - x0)))) * ((0 |^ n) * 0) is V22() real ext-real Element of REAL
((((f,].(x0 - r),(x0 + r).[) . (n + 1)) . (x0 + (c * (x - x0)))) * ((0 |^ n) * 0)) / ((n + 1) !) is V22() real ext-real Element of REAL
(f . x) + (((((f,].(x0 - r),(x0 + r).[) . (n + 1)) . (x0 + (c * (x - x0)))) * ((0 |^ n) * 0)) / ((n + 1) !)) is V22() real ext-real Element of REAL
x0 - x0 is V22() real ext-real Element of REAL
abs (x0 - x0) is V22() real ext-real Element of REAL
[.x0,x.] is closed V80() V81() V82() V100() Element of K19(REAL)
(n + 1) - 1 is V22() real ext-real integer non irrational Element of REAL
(f,].(x0 - r),(x0 + r).[) . n is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
((f,].(x0 - r),(x0 + r).[) . n) | ].(x0 - r),(x0 + r).[ is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
((f,].(x0 - r),(x0 + r).[) . n) | [.x0,x.] is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
].x0,x.[ is open V80() V81() V82() V95() V96() V100() Element of K19(REAL)
(f,].x0,x.[) is V1() V4( NAT ) V5( PFuncs (REAL,REAL)) Function-like non empty total quasi_total Element of K19(K20(NAT,(PFuncs (REAL,REAL))))
(f,].x0,x.[) . (n + 1) is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
c is V22() real ext-real Element of REAL
((f,].x0,x.[) . (n + 1)) . c is V22() real ext-real Element of REAL
(((f,].x0,x.[) . (n + 1)) . c) * ((x - x0) |^ (n + 1)) is V22() real ext-real Element of REAL
((((f,].x0,x.[) . (n + 1)) . c) * ((x - x0) |^ (n + 1))) / ((n + 1) !) is V22() real ext-real Element of REAL
((Partial_Sums (f,].(x0 - r),(x0 + r).[,x0,x)) . n) + (((((f,].x0,x.[) . (n + 1)) . c) * ((x - x0) |^ (n + 1))) / ((n + 1) !)) is V22() real ext-real Element of REAL
c - x0 is V22() real ext-real Element of REAL
(c - x0) / (x - x0) is V22() real ext-real Element of REAL
s is V22() real ext-real Element of REAL
s * (x - x0) is V22() real ext-real Element of REAL
x0 + (s * (x - x0)) is V22() real ext-real Element of REAL
x0 + (c - x0) is V22() real ext-real Element of REAL
x0 + (x - x0) is V22() real ext-real Element of REAL
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( not b₁ <= x0 & not x0 + (x - x0) <= b₁ ) } is set
g is V22() real ext-real Element of REAL
0 / (x - x0) is V22() real ext-real Element of REAL
g is V22() real ext-real Element of REAL
(x - x0) / (x - x0) is V22() real ext-real Element of REAL
((f,].(x0 - r),(x0 + r).[) . (n + 1)) | ].x0,x.[ is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
(((f,].(x0 - r),(x0 + r).[) . (n + 1)) | ].x0,x.[) . c is V22() real ext-real Element of REAL
((f,].(x0 - r),(x0 + r).[) . (n + 1)) . c is V22() real ext-real Element of REAL
((f,].(x0 - r),(x0 + r).[) . (n + 1)) . (x0 + (s * (x - x0))) is V22() real ext-real Element of REAL
(((f,].(x0 - r),(x0 + r).[) . (n + 1)) . (x0 + (s * (x - x0)))) * ((x - x0) |^ (n + 1)) is V22() real ext-real Element of REAL
((((f,].(x0 - r),(x0 + r).[) . (n + 1)) . (x0 + (s * (x - x0)))) * ((x - x0) |^ (n + 1))) / ((n + 1) !) is V22() real ext-real Element of REAL
((Partial_Sums (f,].(x0 - r),(x0 + r).[,x0,x)) . n) + (((((f,].(x0 - r),(x0 + r).[) . (n + 1)) . (x0 + (s * (x - x0)))) * ((x - x0) |^ (n + 1))) / ((n + 1) !)) is V22() real ext-real Element of REAL
t is V22() real ext-real Element of REAL
t * (x - x0) is V22() real ext-real Element of REAL
x0 + (t * (x - x0)) is V22() real ext-real Element of REAL
((f,].(x0 - r),(x0 + r).[) . (n + 1)) . (x0 + (t * (x - x0))) is V22() real ext-real Element of REAL
(((f,].(x0 - r),(x0 + r).[) . (n + 1)) . (x0 + (t * (x - x0)))) * ((x - x0) |^ (n + 1)) is V22() real ext-real Element of REAL
((((f,].(x0 - r),(x0 + r).[) . (n + 1)) . (x0 + (t * (x - x0)))) * ((x - x0) |^ (n + 1))) / ((n + 1) !) is V22() real ext-real Element of REAL
((Partial_Sums (f,].(x0 - r),(x0 + r).[,x0,x)) . n) + (((((f,].(x0 - r),(x0 + r).[) . (n + 1)) . (x0 + (t * (x - x0)))) * ((x - x0) |^ (n + 1))) / ((n + 1) !)) is V22() real ext-real Element of REAL
c is V22() real ext-real non negative non irrational Element of REAL
c * (x - x0) is V22() real ext-real Element of REAL
x0 + (c * (x - x0)) is V22() real ext-real Element of REAL
((f,].(x0 - r),(x0 + r).[) . (n + 1)) . (x0 + (c * (x - x0))) is V22() real ext-real Element of REAL
(((f,].(x0 - r),(x0 + r).[) . (n + 1)) . (x0 + (c * (x - x0)))) * ((x - x0) |^ (n + 1)) is V22() real ext-real Element of REAL
((((f,].(x0 - r),(x0 + r).[) . (n + 1)) . (x0 + (c * (x - x0)))) * ((x - x0) |^ (n + 1))) / ((n + 1) !) is V22() real ext-real Element of REAL
((Partial_Sums (f,].(x0 - r),(x0 + r).[,x0,x)) . n) + (((((f,].(x0 - r),(x0 + r).[) . (n + 1)) . (x0 + (c * (x - x0)))) * ((x - x0) |^ (n + 1))) / ((n + 1) !)) is V22() real ext-real Element of REAL
s is V22() real ext-real Element of REAL
s * (x - x0) is V22() real ext-real Element of REAL
x0 + (s * (x - x0)) is V22() real ext-real Element of REAL
((f,].(x0 - r),(x0 + r).[) . (n + 1)) . (x0 + (s * (x - x0))) is V22() real ext-real Element of REAL
(((f,].(x0 - r),(x0 + r).[) . (n + 1)) . (x0 + (s * (x - x0)))) * ((x - x0) |^ (n + 1)) is V22() real ext-real Element of REAL
((((f,].(x0 - r),(x0 + r).[) . (n + 1)) . (x0 + (s * (x - x0)))) * ((x - x0) |^ (n + 1))) / ((n + 1) !) is V22() real ext-real Element of REAL
((Partial_Sums (f,].(x0 - r),(x0 + r).[,x0,x)) . n) + (((((f,].(x0 - r),(x0 + r).[) . (n + 1)) . (x0 + (s * (x - x0)))) * ((x - x0) |^ (n + 1))) / ((n + 1) !)) is V22() real ext-real Element of REAL