:: FDIFF_2 semantic presentation

REAL is non empty V49() V72() V73() V74() V78() set
NAT is non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() Element of K19(REAL)
K19(REAL) is set
COMPLEX is non empty V49() V72() V78() set
omega is non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() set
K19(omega) is set
K20(NAT,REAL) is complex-valued ext-real-valued real-valued set
K19(K20(NAT,REAL)) is set
K19(K19(REAL)) is set
{} is set
the empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() real ext-real non positive non negative V72() V73() V74() V75() V76() V77() V78() set is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() real ext-real non positive non negative V72() V73() V74() V75() V76() V77() V78() set
1 is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V72() V73() V74() V75() V76() V77() V94() V95() Element of NAT
{{},1} is set
K20(REAL,REAL) is complex-valued ext-real-valued real-valued set
K19(K20(REAL,REAL)) is set
RAT is non empty V49() V72() V73() V74() V75() V78() set
INT is non empty V49() V72() V73() V74() V75() V76() V78() set
K20(COMPLEX,COMPLEX) is complex-valued set
K19(K20(COMPLEX,COMPLEX)) is set
K20(K20(COMPLEX,COMPLEX),COMPLEX) is complex-valued set
K19(K20(K20(COMPLEX,COMPLEX),COMPLEX)) is set
K20(K20(REAL,REAL),REAL) is complex-valued ext-real-valued real-valued set
K19(K20(K20(REAL,REAL),REAL)) is set
K20(RAT,RAT) is V5( RAT ) complex-valued ext-real-valued real-valued set
K19(K20(RAT,RAT)) is set
K20(K20(RAT,RAT),RAT) is V5( RAT ) complex-valued ext-real-valued real-valued set
K19(K20(K20(RAT,RAT),RAT)) is set
K20(INT,INT) is V5( RAT ) V5( INT ) complex-valued ext-real-valued real-valued set
K19(K20(INT,INT)) is set
K20(K20(INT,INT),INT) is V5( RAT ) V5( INT ) complex-valued ext-real-valued real-valued set
K19(K20(K20(INT,INT),INT)) is set
K20(NAT,NAT) is V5( RAT ) V5( INT ) complex-valued ext-real-valued real-valued natural-valued set
K20(K20(NAT,NAT),NAT) is V5( RAT ) V5( INT ) complex-valued ext-real-valued real-valued natural-valued set
K19(K20(K20(NAT,NAT),NAT)) is set
K19(NAT) is set
0 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V72() V73() V74() V75() V76() V77() V94() V95() Element of NAT
- 1 is non empty V22() real ext-real non positive negative Element of REAL
{0} is V72() V73() V74() V75() V76() V77() set
K19(K20(NAT,NAT)) is set
2 is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V72() V73() V74() V75() V76() V77() V94() V95() Element of NAT
[#] REAL is closed open V72() V73() V74() Element of K19(REAL)
-infty is non empty non real ext-real non positive negative set
+infty is non empty non real ext-real positive non negative set
x0 is V1() non-empty V4( NAT ) V5( REAL ) Function-like non empty total quasi_total complex-valued ext-real-valued real-valued 0 -convergent convergent Element of K19(K20(NAT,REAL))
- x0 is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
- 1 is non empty V22() real ext-real non positive negative set
(- 1) (#) x0 is V1() V4( NAT ) Function-like total complex-valued ext-real-valued real-valued set
x0 is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim x0 is V22() real ext-real Element of REAL
f is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim f is V22() real ext-real Element of REAL
h is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim h is V22() real ext-real Element of REAL
c is V22() real ext-real set
fm is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V72() V73() V74() V75() V76() V77() V94() V95() Element of NAT
fp is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V72() V73() V74() V75() V76() V77() V94() V95() Element of NAT
2 * fm is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V72() V73() V74() V75() V76() V77() V94() V95() Element of NAT
2 * fp is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V72() V73() V74() V75() V76() V77() V94() V95() Element of NAT
(2 * fp) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V72() V73() V74() V75() V76() V77() V94() V95() Element of NAT
max ((2 * fm),((2 * fp) + 1)) is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V72() V73() V74() V75() V76() V77() V94() V95() Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V72() V73() V74() V75() V76() V77() V94() V95() Element of NAT
a is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V72() V73() V74() V75() V76() V77() V94() V95() Element of NAT
h is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V72() V73() V74() V75() V76() V77() V94() V95() Element of NAT
2 * h is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V72() V73() V74() V75() V76() V77() V94() V95() Element of NAT
(2 * h) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V72() V73() V74() V75() V76() V77() V94() V95() Element of NAT
h . a is V22() real ext-real Element of REAL
(h . a) - (lim x0) is V22() real ext-real Element of REAL
abs ((h . a) - (lim x0)) is V22() real ext-real Element of REAL
x0 . h is V22() real ext-real Element of REAL
(x0 . h) - (lim x0) is V22() real ext-real Element of REAL
abs ((x0 . h) - (lim x0)) is V22() real ext-real Element of REAL
h . a is V22() real ext-real Element of REAL
(h . a) - (lim x0) is V22() real ext-real Element of REAL
abs ((h . a) - (lim x0)) is V22() real ext-real Element of REAL
f . h is V22() real ext-real Element of REAL
(f . h) - (lim x0) is V22() real ext-real Element of REAL
abs ((f . h) - (lim x0)) is V22() real ext-real Element of REAL
h . a is V22() real ext-real Element of REAL
(h . a) - (lim x0) is V22() real ext-real Element of REAL
abs ((h . a) - (lim x0)) is V22() real ext-real Element of REAL
h . a is V22() real ext-real Element of REAL
(h . a) - (lim x0) is V22() real ext-real Element of REAL
abs ((h . a) - (lim x0)) is V22() real ext-real Element of REAL
x0 is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
f is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V72() V73() V74() V75() V76() V77() V94() V95() Element of NAT
f + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V72() V73() V74() V75() V76() V77() V94() V95() Element of NAT
x0 . (f + 1) is V22() real ext-real Element of REAL
x0 . f is V22() real ext-real Element of REAL
2 * f is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V72() V73() V74() V75() V76() V77() V94() V95() Element of NAT
(2 * f) + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V72() V73() V74() V75() V76() V77() V94() V95() Element of NAT
(2 * f) + 0 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V72() V73() V74() V75() V76() V77() V94() V95() Element of NAT
2 * (f + 1) is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V72() V73() V74() V75() V76() V77() V94() V95() Element of NAT
x0 . (f + 1) is V22() real ext-real Element of REAL
x0 . f is V22() real ext-real Element of REAL
f is set
h is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V72() V73() V74() V75() V76() V77() V94() V95() Element of NAT
x0 . h is V22() real ext-real Element of REAL
2 * h is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V72() V73() V74() V75() V76() V77() V94() V95() Element of NAT
x0 . f is V22() real ext-real Element of REAL
dom x0 is V72() V73() V74() V75() V76() V77() Element of K19(NAT)
x0 is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
f is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V72() V73() V74() V75() V76() V77() V94() V95() Element of NAT
f + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V72() V73() V74() V75() V76() V77() V94() V95() Element of NAT
x0 . (f + 1) is V22() real ext-real Element of REAL
x0 . f is V22() real ext-real Element of REAL
2 * f is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V72() V73() V74() V75() V76() V77() V94() V95() Element of NAT
(2 * f) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V72() V73() V74() V75() V76() V77() V94() V95() Element of NAT
((2 * f) + 1) + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V72() V73() V74() V75() V76() V77() V94() V95() Element of NAT
((2 * f) + 1) + 0 is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V72() V73() V74() V75() V76() V77() V94() V95() Element of NAT
2 * (f + 1) is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V72() V73() V74() V75() V76() V77() V94() V95() Element of NAT
(2 * (f + 1)) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V72() V73() V74() V75() V76() V77() V94() V95() Element of NAT
x0 . (f + 1) is V22() real ext-real Element of REAL
x0 . f is V22() real ext-real Element of REAL
f is set
dom x0 is V72() V73() V74() V75() V76() V77() Element of K19(NAT)
h is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V72() V73() V74() V75() V76() V77() V94() V95() Element of NAT
x0 . h is V22() real ext-real Element of REAL
2 * h is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V72() V73() V74() V75() V76() V77() V94() V95() Element of NAT
(2 * h) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V72() V73() V74() V75() V76() V77() V94() V95() Element of NAT
x0 . f is V22() real ext-real Element of REAL
x0 is V22() real ext-real Element of REAL
{x0} is V72() V73() V74() set
f is V1() non-empty V4( NAT ) V5( REAL ) Function-like non empty total quasi_total complex-valued ext-real-valued real-valued 0 -convergent convergent Element of K19(K20(NAT,REAL))
h is V1() V4( NAT ) V5( REAL ) Function-like constant non empty total quasi_total complex-valued ext-real-valued real-valued non-decreasing non-increasing convergent Element of K19(K20(NAT,REAL))
rng h is V72() V73() V74() Element of K19(REAL)
lim h is V22() real ext-real Element of REAL
f + h is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim (f + h) is V22() real ext-real Element of REAL
lim f is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() real ext-real non positive non negative V72() V73() V74() V75() V76() V77() V78() Element of REAL
0 + x0 is V22() real ext-real Element of REAL
x0 is V22() real ext-real Element of REAL
{x0} is V72() V73() V74() set
f is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
rng f is V72() V73() V74() Element of K19(REAL)
h is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
rng h is V72() V73() V74() Element of K19(REAL)
c is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V72() V73() V74() V75() V76() V77() V94() V95() Element of NAT
f . c is V22() real ext-real Element of REAL
h . c is V22() real ext-real Element of REAL
x0 is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
f is V1() non-empty V4( NAT ) V5( REAL ) Function-like non empty total quasi_total complex-valued ext-real-valued real-valued 0 -convergent convergent Element of K19(K20(NAT,REAL))
h is V1() V4( NAT ) V5( NAT ) Function-like non empty total quasi_total complex-valued ext-real-valued real-valued natural-valued increasing non-decreasing Element of K19(K20(NAT,NAT))
f * h is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
c is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V72() V73() V74() V75() V76() V77() V94() V95() Element of NAT
x0 . c is V22() real ext-real Element of REAL
h . c is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V72() V73() V74() V75() V76() V77() V94() V95() Element of NAT
f . (h . c) is V22() real ext-real Element of REAL
lim f is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() real ext-real non positive non negative V72() V73() V74() V75() V76() V77() V78() Element of REAL
lim x0 is V22() real ext-real Element of REAL
x0 is V22() real ext-real Element of REAL
{x0} is V72() V73() V74() set
f is V1() V4( REAL ) V5( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom f is V72() V73() V74() Element of K19(REAL)
h is V1() non-empty V4( NAT ) V5( REAL ) Function-like non empty total quasi_total complex-valued ext-real-valued real-valued 0 -convergent convergent Element of K19(K20(NAT,REAL))
h " is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
c is V1() non-empty V4( NAT ) V5( REAL ) Function-like non empty total quasi_total complex-valued ext-real-valued real-valued 0 -convergent convergent Element of K19(K20(NAT,REAL))
c " is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
fm is V1() V4( NAT ) V5( REAL ) Function-like constant non empty total quasi_total complex-valued ext-real-valued real-valued non-decreasing non-increasing convergent Element of K19(K20(NAT,REAL))
rng fm is V72() V73() V74() Element of K19(REAL)
h + fm is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
rng (h + fm) is V72() V73() V74() Element of K19(REAL)
c + fm is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
rng (c + fm) is V72() V73() V74() Element of K19(REAL)
f /* (h + fm) is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
f /* fm is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f /* (h + fm)) - (f /* fm) is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
- (f /* fm) is V1() V4( NAT ) Function-like total complex-valued ext-real-valued real-valued set
(- 1) (#) (f /* fm) is V1() V4( NAT ) Function-like total complex-valued ext-real-valued real-valued set
(f /* (h + fm)) + (- (f /* fm)) is V1() V4( NAT ) Function-like total complex-valued ext-real-valued real-valued set
(h ") (#) ((f /* (h + fm)) - (f /* fm)) is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim ((h ") (#) ((f /* (h + fm)) - (f /* fm))) is V22() real ext-real Element of REAL
f /* (c + fm) is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f /* (c + fm)) - (f /* fm) is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f /* (c + fm)) + (- (f /* fm)) is V1() V4( NAT ) Function-like total complex-valued ext-real-valued real-valued set
(c ") (#) ((f /* (c + fm)) - (f /* fm)) is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim ((c ") (#) ((f /* (c + fm)) - (f /* fm))) is V22() real ext-real Element of REAL
fp is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
n is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V72() V73() V74() V75() V76() V77() V94() V95() Element of NAT
a is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V72() V73() V74() V75() V76() V77() V94() V95() Element of NAT
2 * a is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V72() V73() V74() V75() V76() V77() V94() V95() Element of NAT
(2 * a) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V72() V73() V74() V75() V76() V77() V94() V95() Element of NAT
fp . n is V22() real ext-real Element of REAL
h . a is V22() real ext-real Element of REAL
fp . n is V22() real ext-real Element of REAL
c . a is V22() real ext-real Element of REAL
fp . n is V22() real ext-real Element of REAL
fp . n is V22() real ext-real Element of REAL
lim h is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() real ext-real non positive non negative V72() V73() V74() V75() V76() V77() V78() Element of REAL
lim c is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() real ext-real non positive non negative V72() V73() V74() V75() V76() V77() V78() Element of REAL
lim fp is V22() real ext-real Element of REAL
n is V1() non-empty V4( NAT ) V5( REAL ) Function-like non empty total quasi_total complex-valued ext-real-valued real-valued 0 -convergent convergent Element of K19(K20(NAT,REAL))
n + fm is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
rng (n + fm) is V72() V73() V74() Element of K19(REAL)
a is set
h is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V72() V73() V74() V75() V76() V77() V94() V95() Element of NAT
(n + fm) . h is V22() real ext-real Element of REAL
c is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V72() V73() V74() V75() V76() V77() V94() V95() Element of NAT
2 * c is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V72() V73() V74() V75() V76() V77() V94() V95() Element of NAT
(2 * c) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V72() V73() V74() V75() V76() V77() V94() V95() Element of NAT
(h + fm) . c is V22() real ext-real Element of REAL
n . h is V22() real ext-real Element of REAL
fm . h is V22() real ext-real Element of REAL
(n . h) + (fm . h) is V22() real ext-real Element of REAL
h . c is V22() real ext-real Element of REAL
(h . c) + (fm . h) is V22() real ext-real Element of REAL
fm . c is V22() real ext-real Element of REAL
(h . c) + (fm . c) is V22() real ext-real Element of REAL
(c + fm) . c is V22() real ext-real Element of REAL
n . h is V22() real ext-real Element of REAL
fm . h is V22() real ext-real Element of REAL
(n . h) + (fm . h) is V22() real ext-real Element of REAL
c . c is V22() real ext-real Element of REAL
(c . c) + (fm . h) is V22() real ext-real Element of REAL
fm . c is V22() real ext-real Element of REAL
(c . c) + (fm . c) is V22() real ext-real Element of REAL
n " is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
f /* (n + fm) is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f /* (n + fm)) - (f /* fm) is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f /* (n + fm)) + (- (f /* fm)) is V1() V4( NAT ) Function-like total complex-valued ext-real-valued real-valued set
(n ") (#) ((f /* (n + fm)) - (f /* fm)) is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
a is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
h is V1() V4( NAT ) V5( NAT ) Function-like non empty total quasi_total complex-valued ext-real-valued real-valued natural-valued increasing non-decreasing Element of K19(K20(NAT,NAT))
((n ") (#) ((f /* (n + fm)) - (f /* fm))) * h is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
c is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V72() V73() V74() V75() V76() V77() V94() V95() Element of NAT
(((n ") (#) ((f /* (n + fm)) - (f /* fm))) * h) . c is V22() real ext-real Element of REAL
h . c is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V72() V73() V74() V75() V76() V77() V94() V95() Element of NAT
((n ") (#) ((f /* (n + fm)) - (f /* fm))) . (h . c) is V22() real ext-real Element of REAL
2 * c is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V72() V73() V74() V75() V76() V77() V94() V95() Element of NAT
(2 * c) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V72() V73() V74() V75() V76() V77() V94() V95() Element of NAT
((n ") (#) ((f /* (n + fm)) - (f /* fm))) . ((2 * c) + 1) is V22() real ext-real Element of REAL
(n ") . ((2 * c) + 1) is V22() real ext-real Element of REAL
((f /* (n + fm)) - (f /* fm)) . ((2 * c) + 1) is V22() real ext-real Element of REAL
((n ") . ((2 * c) + 1)) * (((f /* (n + fm)) - (f /* fm)) . ((2 * c) + 1)) is V22() real ext-real Element of REAL
(f /* (n + fm)) . ((2 * c) + 1) is V22() real ext-real Element of REAL
(f /* fm) . ((2 * c) + 1) is V22() real ext-real Element of REAL
((f /* (n + fm)) . ((2 * c) + 1)) - ((f /* fm) . ((2 * c) + 1)) is V22() real ext-real Element of REAL
((n ") . ((2 * c) + 1)) * (((f /* (n + fm)) . ((2 * c) + 1)) - ((f /* fm) . ((2 * c) + 1))) is V22() real ext-real Element of REAL
(n + fm) . ((2 * c) + 1) is V22() real ext-real Element of REAL
f . ((n + fm) . ((2 * c) + 1)) is V22() real ext-real Element of REAL
(f . ((n + fm) . ((2 * c) + 1))) - ((f /* fm) . ((2 * c) + 1)) is V22() real ext-real Element of REAL
((n ") . ((2 * c) + 1)) * ((f . ((n + fm) . ((2 * c) + 1))) - ((f /* fm) . ((2 * c) + 1))) is V22() real ext-real Element of REAL
n . ((2 * c) + 1) is V22() real ext-real Element of REAL
fm . ((2 * c) + 1) is V22() real ext-real Element of REAL
(n . ((2 * c) + 1)) + (fm . ((2 * c) + 1)) is V22() real ext-real Element of REAL
f . ((n . ((2 * c) + 1)) + (fm . ((2 * c) + 1))) is V22() real ext-real Element of REAL
(f . ((n . ((2 * c) + 1)) + (fm . ((2 * c) + 1)))) - ((f /* fm) . ((2 * c) + 1)) is V22() real ext-real Element of REAL
((n ") . ((2 * c) + 1)) * ((f . ((n . ((2 * c) + 1)) + (fm . ((2 * c) + 1)))) - ((f /* fm) . ((2 * c) + 1))) is V22() real ext-real Element of REAL
c . c is V22() real ext-real Element of REAL
(c . c) + (fm . ((2 * c) + 1)) is V22() real ext-real Element of REAL
f . ((c . c) + (fm . ((2 * c) + 1))) is V22() real ext-real Element of REAL
(f . ((c . c) + (fm . ((2 * c) + 1)))) - ((f /* fm) . ((2 * c) + 1)) is V22() real ext-real Element of REAL
((n ") . ((2 * c) + 1)) * ((f . ((c . c) + (fm . ((2 * c) + 1)))) - ((f /* fm) . ((2 * c) + 1))) is V22() real ext-real Element of REAL
fm . c is V22() real ext-real Element of REAL
(c . c) + (fm . c) is V22() real ext-real Element of REAL
f . ((c . c) + (fm . c)) is V22() real ext-real Element of REAL
(f . ((c . c) + (fm . c))) - ((f /* fm) . ((2 * c) + 1)) is V22() real ext-real Element of REAL
((n ") . ((2 * c) + 1)) * ((f . ((c . c) + (fm . c))) - ((f /* fm) . ((2 * c) + 1))) is V22() real ext-real Element of REAL
(c + fm) . c is V22() real ext-real Element of REAL
f . ((c + fm) . c) is V22() real ext-real Element of REAL
(f . ((c + fm) . c)) - ((f /* fm) . ((2 * c) + 1)) is V22() real ext-real Element of REAL
((n ") . ((2 * c) + 1)) * ((f . ((c + fm) . c)) - ((f /* fm) . ((2 * c) + 1))) is V22() real ext-real Element of REAL
(f /* (c + fm)) . c is V22() real ext-real Element of REAL
((f /* (c + fm)) . c) - ((f /* fm) . ((2 * c) + 1)) is V22() real ext-real Element of REAL
((n ") . ((2 * c) + 1)) * (((f /* (c + fm)) . c) - ((f /* fm) . ((2 * c) + 1))) is V22() real ext-real Element of REAL
(n . ((2 * c) + 1)) " is V22() real ext-real Element of REAL
((n . ((2 * c) + 1)) ") * (((f /* (c + fm)) . c) - ((f /* fm) . ((2 * c) + 1))) is V22() real ext-real Element of REAL
(c . c) " is V22() real ext-real Element of REAL
((c . c) ") * (((f /* (c + fm)) . c) - ((f /* fm) . ((2 * c) + 1))) is V22() real ext-real Element of REAL
(c ") . c is V22() real ext-real Element of REAL
((c ") . c) * (((f /* (c + fm)) . c) - ((f /* fm) . ((2 * c) + 1))) is V22() real ext-real Element of REAL
f . (fm . ((2 * c) + 1)) is V22() real ext-real Element of REAL
((f /* (c + fm)) . c) - (f . (fm . ((2 * c) + 1))) is V22() real ext-real Element of REAL
((c ") . c) * (((f /* (c + fm)) . c) - (f . (fm . ((2 * c) + 1)))) is V22() real ext-real Element of REAL
f . (fm . c) is V22() real ext-real Element of REAL
((f /* (c + fm)) . c) - (f . (fm . c)) is V22() real ext-real Element of REAL
((c ") . c) * (((f /* (c + fm)) . c) - (f . (fm . c))) is V22() real ext-real Element of REAL
(f /* fm) . c is V22() real ext-real Element of REAL
((f /* (c + fm)) . c) - ((f /* fm) . c) is V22() real ext-real Element of REAL
((c ") . c) * (((f /* (c + fm)) . c) - ((f /* fm) . c)) is V22() real ext-real Element of REAL
((f /* (c + fm)) - (f /* fm)) . c is V22() real ext-real Element of REAL
((c ") . c) * (((f /* (c + fm)) - (f /* fm)) . c) is V22() real ext-real Element of REAL
((c ") (#) ((f /* (c + fm)) - (f /* fm))) . c is V22() real ext-real Element of REAL
lim (((n ") (#) ((f /* (n + fm)) - (f /* fm))) * h) is V22() real ext-real Element of REAL
lim ((n ") (#) ((f /* (n + fm)) - (f /* fm))) is V22() real ext-real Element of REAL
c is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
a is V1() V4( NAT ) V5( NAT ) Function-like non empty total quasi_total complex-valued ext-real-valued real-valued natural-valued increasing non-decreasing Element of K19(K20(NAT,NAT))
((n ") (#) ((f /* (n + fm)) - (f /* fm))) * a is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
b is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V72() V73() V74() V75() V76() V77() V94() V95() Element of NAT
(((n ") (#) ((f /* (n + fm)) - (f /* fm))) * a) . b is V22() real ext-real Element of REAL
a . b is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V72() V73() V74() V75() V76() V77() V94() V95() Element of NAT
((n ") (#) ((f /* (n + fm)) - (f /* fm))) . (a . b) is V22() real ext-real Element of REAL
2 * b is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V72() V73() V74() V75() V76() V77() V94() V95() Element of NAT
((n ") (#) ((f /* (n + fm)) - (f /* fm))) . (2 * b) is V22() real ext-real Element of REAL
(n ") . (2 * b) is V22() real ext-real Element of REAL
((f /* (n + fm)) - (f /* fm)) . (2 * b) is V22() real ext-real Element of REAL
((n ") . (2 * b)) * (((f /* (n + fm)) - (f /* fm)) . (2 * b)) is V22() real ext-real Element of REAL
(f /* (n + fm)) . (2 * b) is V22() real ext-real Element of REAL
(f /* fm) . (2 * b) is V22() real ext-real Element of REAL
((f /* (n + fm)) . (2 * b)) - ((f /* fm) . (2 * b)) is V22() real ext-real Element of REAL
((n ") . (2 * b)) * (((f /* (n + fm)) . (2 * b)) - ((f /* fm) . (2 * b))) is V22() real ext-real Element of REAL
(n + fm) . (2 * b) is V22() real ext-real Element of REAL
f . ((n + fm) . (2 * b)) is V22() real ext-real Element of REAL
(f . ((n + fm) . (2 * b))) - ((f /* fm) . (2 * b)) is V22() real ext-real Element of REAL
((n ") . (2 * b)) * ((f . ((n + fm) . (2 * b))) - ((f /* fm) . (2 * b))) is V22() real ext-real Element of REAL
n . (2 * b) is V22() real ext-real Element of REAL
fm . (2 * b) is V22() real ext-real Element of REAL
(n . (2 * b)) + (fm . (2 * b)) is V22() real ext-real Element of REAL
f . ((n . (2 * b)) + (fm . (2 * b))) is V22() real ext-real Element of REAL
(f . ((n . (2 * b)) + (fm . (2 * b)))) - ((f /* fm) . (2 * b)) is V22() real ext-real Element of REAL
((n ") . (2 * b)) * ((f . ((n . (2 * b)) + (fm . (2 * b)))) - ((f /* fm) . (2 * b))) is V22() real ext-real Element of REAL
h . b is V22() real ext-real Element of REAL
(h . b) + (fm . (2 * b)) is V22() real ext-real Element of REAL
f . ((h . b) + (fm . (2 * b))) is V22() real ext-real Element of REAL
(f . ((h . b) + (fm . (2 * b)))) - ((f /* fm) . (2 * b)) is V22() real ext-real Element of REAL
((n ") . (2 * b)) * ((f . ((h . b) + (fm . (2 * b)))) - ((f /* fm) . (2 * b))) is V22() real ext-real Element of REAL
fm . b is V22() real ext-real Element of REAL
(h . b) + (fm . b) is V22() real ext-real Element of REAL
f . ((h . b) + (fm . b)) is V22() real ext-real Element of REAL
(f . ((h . b) + (fm . b))) - ((f /* fm) . (2 * b)) is V22() real ext-real Element of REAL
((n ") . (2 * b)) * ((f . ((h . b) + (fm . b))) - ((f /* fm) . (2 * b))) is V22() real ext-real Element of REAL
(h + fm) . b is V22() real ext-real Element of REAL
f . ((h + fm) . b) is V22() real ext-real Element of REAL
(f . ((h + fm) . b)) - ((f /* fm) . (2 * b)) is V22() real ext-real Element of REAL
((n ") . (2 * b)) * ((f . ((h + fm) . b)) - ((f /* fm) . (2 * b))) is V22() real ext-real Element of REAL
(f /* (h + fm)) . b is V22() real ext-real Element of REAL
((f /* (h + fm)) . b) - ((f /* fm) . (2 * b)) is V22() real ext-real Element of REAL
((n ") . (2 * b)) * (((f /* (h + fm)) . b) - ((f /* fm) . (2 * b))) is V22() real ext-real Element of REAL
(n . (2 * b)) " is V22() real ext-real Element of REAL
((n . (2 * b)) ") * (((f /* (h + fm)) . b) - ((f /* fm) . (2 * b))) is V22() real ext-real Element of REAL
(h . b) " is V22() real ext-real Element of REAL
((h . b) ") * (((f /* (h + fm)) . b) - ((f /* fm) . (2 * b))) is V22() real ext-real Element of REAL
(h ") . b is V22() real ext-real Element of REAL
((h ") . b) * (((f /* (h + fm)) . b) - ((f /* fm) . (2 * b))) is V22() real ext-real Element of REAL
f . (fm . (2 * b)) is V22() real ext-real Element of REAL
((f /* (h + fm)) . b) - (f . (fm . (2 * b))) is V22() real ext-real Element of REAL
((h ") . b) * (((f /* (h + fm)) . b) - (f . (fm . (2 * b)))) is V22() real ext-real Element of REAL
f . (fm . b) is V22() real ext-real Element of REAL
((f /* (h + fm)) . b) - (f . (fm . b)) is V22() real ext-real Element of REAL
((h ") . b) * (((f /* (h + fm)) . b) - (f . (fm . b))) is V22() real ext-real Element of REAL
(f /* fm) . b is V22() real ext-real Element of REAL
((f /* (h + fm)) . b) - ((f /* fm) . b) is V22() real ext-real Element of REAL
((h ") . b) * (((f /* (h + fm)) . b) - ((f /* fm) . b)) is V22() real ext-real Element of REAL
((f /* (h + fm)) - (f /* fm)) . b is V22() real ext-real Element of REAL
((h ") . b) * (((f /* (h + fm)) - (f /* fm)) . b) is V22() real ext-real Element of REAL
((h ") (#) ((f /* (h + fm)) - (f /* fm))) . b is V22() real ext-real Element of REAL
x0 is V22() real ext-real Element of REAL
{x0} is V72() V73() V74() set
f is V1() V4( REAL ) V5( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom f is V72() V73() V74() Element of K19(REAL)
h is open V72() V73() V74() Neighbourhood of x0
NAT --> x0 is V1() V4( REAL ) V4( NAT ) V5( REAL ) Function-like constant non empty total T-Sequence-like complex-valued ext-real-valued real-valued non-decreasing non-increasing V79() Element of K19(K20(REAL,REAL))
fm is V22() real ext-real set
x0 - fm is V22() real ext-real Element of REAL
x0 + fm is V22() real ext-real Element of REAL
].(x0 - fm),(x0 + fm).[ is open V72() V73() V74() Element of K19(REAL)
c is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
n is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim n is V22() real ext-real Element of REAL
a is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V72() V73() V74() V75() V76() V77() V94() V95() Element of NAT
a + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V72() V73() V74() V75() V76() V77() V94() V95() Element of NAT
fm / (a + 2) is V22() real ext-real Element of REAL
n . a is V22() real ext-real Element of REAL
a is V1() non-empty V4( NAT ) V5( REAL ) Function-like non empty total quasi_total complex-valued ext-real-valued real-valued 0 -convergent convergent Element of K19(K20(NAT,REAL))
fp is V1() V4( NAT ) V5( REAL ) Function-like constant non empty total quasi_total complex-valued ext-real-valued real-valued non-decreasing non-increasing convergent Element of K19(K20(NAT,REAL))
rng fp is V72() V73() V74() Element of K19(REAL)
a + fp is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
rng (a + fp) is V72() V73() V74() Element of K19(REAL)
h is set
c is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V72() V73() V74() V75() V76() V77() V94() V95() Element of NAT
fp . c is V22() real ext-real Element of REAL
h is set
fp . 0 is V22() real ext-real Element of REAL
h is set
c is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V72() V73() V74() V75() V76() V77() V94() V95() Element of NAT
(a + fp) . c is V22() real ext-real Element of REAL
c + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V72() V73() V74() V75() V76() V77() V94() V95() Element of NAT
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V72() V73() V74() V75() V76() V77() V94() V95() Element of NAT
fm * (c + 2) is V22() real ext-real Element of REAL
fm * 1 is V22() real ext-real Element of REAL
(c + 2) " is non empty V22() real ext-real positive non negative Element of REAL
(fm * (c + 2)) * ((c + 2) ") is V22() real ext-real Element of REAL
fm * ((c + 2) ") is V22() real ext-real Element of REAL
(c + 2) * ((c + 2) ") is non empty V22() real ext-real positive non negative Element of REAL
fm * ((c + 2) * ((c + 2) ")) is V22() real ext-real Element of REAL
fm / (c + 2) is V22() real ext-real Element of REAL
x0 + (fm / (c + 2)) is V22() real ext-real Element of REAL
x0 - 0 is V22() real ext-real Element of REAL
x0 + 0 is V22() real ext-real Element of REAL
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( not b₁ <= x0 - fm & not x0 + fm <= b₁ ) } is set
a . c is V22() real ext-real Element of REAL
fp . c is V22() real ext-real Element of REAL
(a . c) + (fp . c) is V22() real ext-real Element of REAL
(fm / (c + 2)) + (fp . c) is V22() real ext-real Element of REAL
(fm / (c + 2)) + x0 is V22() real ext-real Element of REAL
h is set
x0 is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
rng x0 is V72() V73() V74() Element of K19(REAL)
f is V1() V4( REAL ) V5( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom f is V72() V73() V74() Element of K19(REAL)
h is V1() V4( REAL ) V5( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
f * h is V1() V4( REAL ) V5( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom (f * h) is V72() V73() V74() Element of K19(REAL)
dom h is V72() V73() V74() Element of K19(REAL)
h /* x0 is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
rng (h /* x0) is V72() V73() V74() Element of K19(REAL)
h .: (rng x0) is V72() V73() V74() Element of K19(REAL)
F₁() is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
x0 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V72() V73() V74() V75() V76() V77() V94() V95() Element of NAT
F₁() . x0 is V22() real ext-real Element of REAL
x0 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative set
F₁() . x0 is V22() real ext-real Element of REAL
h is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V72() V73() V74() V75() V76() V77() V94() V95() Element of NAT
h + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V72() V73() V74() V75() V76() V77() V94() V95() Element of NAT
c is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V72() V73() V74() V75() V76() V77() V94() V95() Element of NAT
F₁() . c is V22() real ext-real Element of REAL
fm is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V72() V73() V74() V75() V76() V77() V94() V95() Element of NAT
F₁() . fm is V22() real ext-real Element of REAL
h is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V72() V73() V74() V75() V76() V77() V94() V95() Element of NAT
c is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V72() V73() V74() V75() V76() V77() V94() V95() Element of NAT
fm is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V72() V73() V74() V75() V76() V77() V94() V95() Element of NAT
F₁() . fm is V22() real ext-real Element of REAL
fm is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative set
F₁() . fm is V22() real ext-real Element of REAL
fp is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V72() V73() V74() V75() V76() V77() V94() V95() Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V72() V73() V74() V75() V76() V77() V94() V95() Element of NAT
F₁() . n is V22() real ext-real Element of REAL
a is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V72() V73() V74() V75() V76() V77() V94() V95() Element of NAT
F₁() . a is V22() real ext-real Element of REAL
f is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V72() V73() V74() V75() V76() V77() V94() V95() Element of NAT
h is V1() V4( NAT ) V5( NAT ) Function-like non empty total quasi_total complex-valued ext-real-valued real-valued natural-valued Element of K19(K20(NAT,NAT))
h . 0 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V72() V73() V74() V75() V76() V77() V94() V95() Element of NAT
rng h is V72() V73() V74() V75() V76() V77() Element of K19(NAT)
dom h is V72() V73() V74() V75() V76() V77() Element of K19(NAT)
c is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
fm is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V72() V73() V74() V75() V76() V77() V94() V95() Element of NAT
c . fm is V22() real ext-real Element of REAL
rng c is V72() V73() V74() Element of K19(REAL)
fm is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V72() V73() V74() V75() V76() V77() V94() V95() Element of NAT
fm + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V72() V73() V74() V75() V76() V77() V94() V95() Element of NAT
c . (fm + 1) is V22() real ext-real Element of REAL
c . fm is V22() real ext-real Element of REAL
fm is V1() V4( NAT ) V5( NAT ) Function-like non empty total quasi_total complex-valued ext-real-valued real-valued natural-valued increasing non-decreasing Element of K19(K20(NAT,NAT))
fp is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V72() V73() V74() V75() V76() V77() V94() V95() Element of NAT
F₁() . fp is V22() real ext-real Element of REAL
fp is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative set
F₁() . fp is V22() real ext-real Element of REAL
fm . 0 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V72() V73() V74() V75() V76() V77() V94() V95() Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative set
F₁() . n is V22() real ext-real Element of REAL
a is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V72() V73() V74() V75() V76() V77() V94() V95() Element of NAT
fm . a is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V72() V73() V74() V75() V76() V77() V94() V95() Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative set
F₁() . n is V22() real ext-real Element of REAL
a is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V72() V73() V74() V75() V76() V77() V94() V95() Element of NAT
F₁() . a is V22() real ext-real Element of REAL
h is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V72() V73() V74() V75() V76() V77() V94() V95() Element of NAT
fm . h is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V72() V73() V74() V75() V76() V77() V94() V95() Element of NAT
c is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V72() V73() V74() V75() V76() V77() V94() V95() Element of NAT
fm . c is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V72() V73() V74() V75() V76() V77() V94() V95() Element of NAT
h is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V72() V73() V74() V75() V76() V77() V94() V95() Element of NAT
fm . h is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V72() V73() V74() V75() V76() V77() V94() V95() Element of NAT
a is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V72() V73() V74() V75() V76() V77() V94() V95() Element of NAT
fm . a is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V72() V73() V74() V75() V76() V77() V94() V95() Element of NAT
a is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V72() V73() V74() V75() V76() V77() V94() V95() Element of NAT
fm . a is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V72() V73() V74() V75() V76() V77() V94() V95() Element of NAT
a + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V72() V73() V74() V75() V76() V77() V94() V95() Element of NAT
fm . (a + 1) is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V72() V73() V74() V75() V76() V77() V94() V95() Element of NAT
h is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V72() V73() V74() V75() V76() V77() V94() V95() Element of NAT
fm . h is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V72() V73() V74() V75() V76() V77() V94() V95() Element of NAT
F₁() . (fm . (a + 1)) is V22() real ext-real Element of REAL
F₁() * fm is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
n is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V72() V73() V74() V75() V76() V77() V94() V95() Element of NAT
(F₁() * fm) . 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 V72() V73() V74() V75() V76() V77() V94() V95() Element of NAT
(F₁() * fm) . (n + 1) is V22() real ext-real Element of REAL
fm . n is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V72() V73() V74() V75() V76() V77() V94() V95() Element of NAT
fm . (n + 1) is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V72() V73() V74() V75() V76() V77() V94() V95() Element of NAT
a is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V72() V73() V74() V75() V76() V77() V94() V95() Element of NAT
h is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V72() V73() V74() V75() V76() V77() V94() V95() Element of NAT
F₁() . h is V22() real ext-real Element of REAL
c is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V72() V73() V74() V75() V76() V77() V94() V95() Element of NAT
F₁() . c is V22() real ext-real Element of REAL
F₁() . (fm . (n + 1)) is V22() real ext-real Element of REAL
(F₁() * fm) . 0 is V22() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V72() V73() V74() V75() V76() V77() V94() V95() Element of NAT
F₁() . n is V22() real ext-real Element of REAL
a is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V72() V73() V74() V75() V76() V77() V94() V95() Element of NAT
fm . a is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V72() V73() V74() V75() V76() V77() V94() V95() Element of NAT
x0 is V22() real ext-real Element of REAL
f is V22() real ext-real Element of REAL
h is V1() V4( REAL ) V5( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
h . x0 is V22() real ext-real Element of REAL
dom h is V72() V73() V74() Element of K19(REAL)
c is open V72() V73() V74() Neighbourhood of x0
fm is V1() V4( REAL ) V5( REAL ) Function-like complex-valued ext-real-valued real-valued linear Element of K19(K20(REAL,REAL))
fp is V1() V4( REAL ) V5( REAL ) Function-like complex-valued ext-real-valued real-valued RestFunc-like Element of K19(K20(REAL,REAL))
x0 is V22() real ext-real Element of REAL
{x0} is V72() V73() V74() set
f is V1() V4( REAL ) V5( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom f is V72() V73() V74() Element of K19(REAL)
diff (f,x0) is V22() real ext-real Element of REAL
h is open V72() V73() V74() Neighbourhood of x0
fm is V1() V4( NAT ) V5( REAL ) Function-like constant non empty total quasi_total complex-valued ext-real-valued real-valued non-decreasing non-increasing convergent Element of K19(K20(NAT,REAL))
rng fm is V72() V73() V74() Element of K19(REAL)
c is V1() non-empty V4( NAT ) V5( REAL ) Function-like non empty total quasi_total complex-valued ext-real-valued real-valued 0 -convergent convergent Element of K19(K20(NAT,REAL))
c + fm is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
rng (c + fm) is V72() V73() V74() Element of K19(REAL)
c " is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
f /* (c + fm) is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
f /* fm is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f /* (c + fm)) - (f /* fm) is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
- (f /* fm) is V1() V4( NAT ) Function-like total complex-valued ext-real-valued real-valued set
(- 1) (#) (f /* fm) is V1() V4( NAT ) Function-like total complex-valued ext-real-valued real-valued set
(f /* (c + fm)) + (- (f /* fm)) is V1() V4( NAT ) Function-like total complex-valued ext-real-valued real-valued set
(c ") (#) ((f /* (c + fm)) - (f /* fm)) is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
c is V22() real ext-real set
x0 - c is V22() real ext-real Element of REAL
x0 + c is V22() real ext-real Element of REAL
].(x0 - c),(x0 + c).[ is open V72() V73() V74() Element of K19(REAL)
fp is V1() V4( NAT ) V5( REAL ) Function-like constant non empty total quasi_total complex-valued ext-real-valued real-valued non-decreasing non-increasing convergent Element of K19(K20(NAT,REAL))
rng fp is V72() V73() V74() Element of K19(REAL)
fm is V1() non-empty V4( NAT ) V5( REAL ) Function-like non empty total quasi_total complex-valued ext-real-valued real-valued 0 -convergent convergent Element of K19(K20(NAT,REAL))
fm + fp is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
rng (fm + fp) is V72() V73() V74() Element of K19(REAL)
fm " is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
f /* (fm + fp) is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
f /* fp is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f /* (fm + fp)) - (f /* fp) is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
- (f /* fp) is V1() V4( NAT ) Function-like total complex-valued ext-real-valued real-valued set
(- 1) (#) (f /* fp) is V1() V4( NAT ) Function-like total complex-valued ext-real-valued real-valued set
(f /* (fm + fp)) + (- (f /* fp)) is V1() V4( NAT ) Function-like total complex-valued ext-real-valued real-valued set
(fm ") (#) ((f /* (fm + fp)) - (f /* fp)) is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim ((fm ") (#) ((f /* (fm + fp)) - (f /* fp))) is V22() real ext-real Element of REAL
a is V1() V4( REAL ) V5( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom a is V72() V73() V74() Element of K19(REAL)
h is V22() real ext-real Element of REAL
a . h is V22() real ext-real Element of REAL
(lim ((fm ") (#) ((f /* (fm + fp)) - (f /* fp)))) * h is V22() real ext-real Element of REAL
h is V1() V4( REAL ) V5( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom h is V72() V73() V74() Element of K19(REAL)
f * h is V1() V4( REAL ) V5( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
f . x0 is V22() real ext-real Element of REAL
c is V1() V4( REAL ) V5( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom c is V72() V73() V74() Element of K19(REAL)
c - a is V1() V4( REAL ) V5( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
- a is V1() V4( REAL ) Function-like complex-valued ext-real-valued real-valued set
(- 1) (#) a is V1() V4( REAL ) Function-like complex-valued ext-real-valued real-valued set
c + (- a) is V1() V4( REAL ) Function-like complex-valued ext-real-valued real-valued set
- c is V22() real ext-real set
].(- c),c.[ is open V72() V73() V74() Element of K19(REAL)
b is V1() V4( REAL ) V5( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom b is V72() V73() V74() Element of K19(REAL)
b is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V72() V73() V74() V75() V76() V77() V94() V95() Element of NAT
fp . b is V22() real ext-real Element of REAL
b is V1() non-empty V4( NAT ) V5( REAL ) Function-like non empty total quasi_total complex-valued ext-real-valued real-valued 0 -convergent convergent Element of K19(K20(NAT,REAL))
lim b is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() real ext-real non positive non negative V72() V73() V74() V75() V76() V77() V78() Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V72() V73() V74() V75() V76() V77() V94() V95() Element of NAT
b ^\ n is V1() non-empty V4( NAT ) V5( REAL ) Function-like non empty total quasi_total complex-valued ext-real-valued real-valued 0 -convergent convergent subsequence of b
r2 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V72() V73() V74() V75() V76() V77() V94() V95() Element of NAT
r2 + n is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V72() V73() V74() V75() V76() V77() V94() V95() Element of NAT
b . (r2 + n) is V22() real ext-real Element of REAL
(b . (r2 + n)) - 0 is V22() real ext-real Element of REAL
abs ((b . (r2 + n)) - 0) is V22() real ext-real Element of REAL
0 - c is V22() real ext-real Element of REAL
0 + c is V22() real ext-real Element of REAL
].(0 - c),(0 + c).[ is open V72() V73() V74() Element of K19(REAL)
(b ^\ n) . r2 is V22() real ext-real Element of REAL
(b ^\ n) + fp is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
rng ((b ^\ n) + fp) is V72() V73() V74() Element of K19(REAL)
r2 is set
c2 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V72() V73() V74() V75() V76() V77() V94() V95() Element of NAT
((b ^\ n) + fp) . c2 is V22() real ext-real Element of REAL
(b ^\ n) . c2 is V22() real ext-real Element of REAL
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( not b₁ <= - c & not c <= b₁ ) } is set
((b ^\ n) . c2) + x0 is V22() real ext-real Element of REAL
c2 is V22() real ext-real Element of REAL
x0 + (- c) is V22() real ext-real Element of REAL
c2 is V22() real ext-real Element of REAL
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( not b₁ <= x0 - c & not x0 + c <= b₁ ) } is set
fp . c2 is V22() real ext-real Element of REAL
((b ^\ n) . c2) + (fp . c2) is V22() real ext-real Element of REAL
(b ^\ n) " is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
a is V1() V4( REAL ) V5( REAL ) Function-like complex-valued ext-real-valued real-valued linear Element of K19(K20(REAL,REAL))
a /* (b ^\ n) is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
((b ^\ n) ") (#) (a /* (b ^\ n)) is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
c /* (b ^\ n) is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
((b ^\ n) ") (#) (c /* (b ^\ n)) is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
b " is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
b /* b is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(b ") (#) (b /* b) is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
((b ") (#) (b /* b)) ^\ n is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of (b ") (#) (b /* b)
(b ") ^\ n is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of b "
(b /* b) ^\ n is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of b /* b
((b ") ^\ n) (#) ((b /* b) ^\ n) is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
((b ^\ n) ") (#) ((b /* b) ^\ n) is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
b /* (b ^\ n) is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
((b ^\ n) ") (#) (b /* (b ^\ n)) is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(((b ^\ n) ") (#) (c /* (b ^\ n))) - (((b ^\ n) ") (#) (a /* (b ^\ n))) is V1() V4( NAT ) V5(