:: LIMFUNC2 semantic presentation

REAL is non empty V51() V71() V72() V73() V77() set
NAT is non empty epsilon-transitive epsilon-connected ordinal V71() V72() V73() V74() V75() V76() V77() Element of K19(REAL)
K19(REAL) is set
COMPLEX is non empty V51() V71() V77() set
omega is non empty epsilon-transitive epsilon-connected ordinal V71() V72() V73() V74() V75() V76() V77() 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 empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() real ext-real non positive non negative V71() V72() V73() V74() V75() V76() V77() set
1 is non empty epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
{{},1} is non empty V71() V72() V73() V74() V75() V76() set
INT is non empty V51() V71() V72() V73() V74() V75() V77() set
RAT is non empty V51() V71() V72() V73() V74() V77() 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(REAL,REAL) is complex-valued ext-real-valued real-valued set
K19(K20(REAL,REAL)) 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 empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() real ext-real non positive non negative V71() V72() V73() V74() V75() V76() V77() V87() V88() Element of NAT
{0} is non empty V71() V72() V73() V74() V75() V76() set
-infty is non empty non real ext-real non positive negative set
+infty is non empty non real ext-real positive non negative set
f is V30() real ext-real set
x0 is V30() real ext-real set
r is V30() real ext-real set
x0 - f is V30() real ext-real set
r + f is V30() real ext-real set
r - 0 is V30() real ext-real Element of REAL
x0 + 0 is V30() real ext-real Element of REAL
x0 is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
rng x0 is V71() V72() V73() Element of K19(REAL)
f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom f is V71() V72() V73() Element of K19(REAL)
r is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
f (#) r is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom (f (#) r) is V71() V72() V73() Element of K19(REAL)
dom r is V71() V72() V73() Element of K19(REAL)
(dom f) /\ (dom r) is V71() V72() V73() Element of K19(REAL)
s is V71() V72() V73() Element of K19(REAL)
(dom (f (#) r)) /\ s is V71() V72() V73() Element of K19(REAL)
(dom f) /\ s is V71() V72() V73() Element of K19(REAL)
(dom r) /\ s is V71() V72() V73() Element of K19(REAL)
x0 is V30() real ext-real Element of REAL
f is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
f + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
1 / (f + 1) is V30() real ext-real non negative Element of REAL
x0 - (1 / (f + 1)) is V30() real ext-real Element of REAL
x0 + (1 / (f + 1)) is V30() real ext-real Element of REAL
x0 is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
rng x0 is V71() V72() V73() Element of K19(REAL)
f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom f is V71() V72() V73() Element of K19(REAL)
r is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
f + r is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom (f + r) is V71() V72() V73() Element of K19(REAL)
dom r is V71() V72() V73() Element of K19(REAL)
(dom f) /\ (dom r) is V71() V72() V73() Element of K19(REAL)
s is V71() V72() V73() Element of K19(REAL)
(dom (f + r)) /\ s is V71() V72() V73() Element of K19(REAL)
(dom f) /\ s is V71() V72() V73() Element of K19(REAL)
(dom r) /\ s is V71() V72() V73() Element of K19(REAL)
x0 is V30() real ext-real Element of REAL
f is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim f is V30() real ext-real Element of REAL
NAT --> x0 is V1() V4( NAT ) V5( REAL ) V6() constant non empty total quasi_total T-Sequence-like complex-valued ext-real-valued real-valued convergent Element of K19(K20(NAT,REAL))
r is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
f - r is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
- r is V1() V4( NAT ) V6() total complex-valued ext-real-valued real-valued set
- 1 is V30() real ext-real non positive set
(- 1) (#) r is V1() V4( NAT ) V6() total complex-valued ext-real-valued real-valued set
f + (- r) is V1() V4( NAT ) V6() total complex-valued ext-real-valued real-valued set
r . 0 is V30() real ext-real Element of REAL
lim r is V30() real ext-real Element of REAL
lim (f - r) is V30() real ext-real Element of REAL
(lim f) - x0 is V30() real ext-real Element of REAL
s is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
k is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
f . k is V30() real ext-real Element of REAL
(f - r) . k is V30() real ext-real Element of REAL
r . k is V30() real ext-real Element of REAL
(f . k) - (r . k) is V30() real ext-real Element of REAL
(f . k) - x0 is V30() real ext-real Element of REAL
0 + x0 is V30() real ext-real Element of REAL
x0 is V30() real ext-real Element of REAL
f is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim f is V30() real ext-real Element of REAL
NAT --> x0 is V1() V4( NAT ) V5( REAL ) V6() constant non empty total quasi_total T-Sequence-like complex-valued ext-real-valued real-valued convergent Element of K19(K20(NAT,REAL))
r is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
r - f is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
- f is V1() V4( NAT ) V6() total complex-valued ext-real-valued real-valued set
- 1 is V30() real ext-real non positive set
(- 1) (#) f is V1() V4( NAT ) V6() total complex-valued ext-real-valued real-valued set
r + (- f) is V1() V4( NAT ) V6() total complex-valued ext-real-valued real-valued set
r . 0 is V30() real ext-real Element of REAL
lim r is V30() real ext-real Element of REAL
lim (r - f) is V30() real ext-real Element of REAL
x0 - (lim f) is V30() real ext-real Element of REAL
s is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
k is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
f . k is V30() real ext-real Element of REAL
(r - f) . k is V30() real ext-real Element of REAL
r . k is V30() real ext-real Element of REAL
(r . k) - (f . k) is V30() real ext-real Element of REAL
x0 - (f . k) is V30() real ext-real Element of REAL
0 + (f . k) is V30() real ext-real Element of REAL
x0 is V30() real ext-real Element of REAL
right_open_halfline x0 is V71() V72() V73() Element of K19(REAL)
K213(x0,+infty) is set
f is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim f is V30() real ext-real Element of REAL
rng f is V71() V72() V73() Element of K19(REAL)
r is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom r is V71() V72() V73() Element of K19(REAL)
(dom r) /\ (right_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
r /* f is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
s is V30() real ext-real Element of REAL
k is V30() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
g2 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
f . n is V30() real ext-real Element of REAL
{ b₁ where b₁ is V30() real ext-real Element of REAL : not b₁ <= x0 } is set
r . (f . n) is V30() real ext-real Element of REAL
g is V30() real ext-real Element of REAL
(r /* f) . n is V30() real ext-real Element of REAL
x0 is V30() real ext-real Element of REAL
f is V30() real ext-real Element of REAL
f - x0 is V30() real ext-real Element of REAL
].(f - x0),f.[ is V71() V72() V73() Element of K19(REAL)
r is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom r is V71() V72() V73() Element of K19(REAL)
s is V30() real ext-real Element of REAL
k is V30() real ext-real set
n is V30() real ext-real Element of REAL
g2 is V30() real ext-real Element of REAL
{ b₁ where b₁ is V30() real ext-real Element of REAL : ( not b₁ <= f - x0 & not f <= b₁ ) } is set
k is V30() real ext-real set
n is V30() real ext-real Element of REAL
g2 is V30() real ext-real Element of REAL
{ b₁ where b₁ is V30() real ext-real Element of REAL : ( not b₁ <= f - x0 & not f <= b₁ ) } is set
k is V30() real ext-real Element of REAL
x0 is V30() real ext-real Element of REAL
f is V30() real ext-real Element of REAL
f + x0 is V30() real ext-real Element of REAL
].f,(f + x0).[ is V71() V72() V73() Element of K19(REAL)
r is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom r is V71() V72() V73() Element of K19(REAL)
s is V30() real ext-real Element of REAL
k is V30() real ext-real set
n is V30() real ext-real Element of REAL
g2 is V30() real ext-real Element of REAL
{ b₁ where b₁ is V30() real ext-real Element of REAL : ( not b₁ <= f & not f + x0 <= b₁ ) } is set
k is V30() real ext-real set
n is V30() real ext-real Element of REAL
g2 is V30() real ext-real Element of REAL
{ b₁ where b₁ is V30() real ext-real Element of REAL : ( not b₁ <= f & not f + x0 <= b₁ ) } is set
k is V30() real ext-real Element of REAL
x0 is V30() real ext-real Element of REAL
left_open_halfline x0 is V71() V72() V73() Element of K19(REAL)
K213(-infty,x0) is set
f is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim f is V30() real ext-real Element of REAL
rng f is V71() V72() V73() Element of K19(REAL)
r is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom r is V71() V72() V73() Element of K19(REAL)
(dom r) /\ (left_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
NAT --> x0 is V1() V4( NAT ) V5( REAL ) V6() constant non empty total quasi_total T-Sequence-like complex-valued ext-real-valued real-valued convergent Element of K19(K20(NAT,REAL))
k is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
k - s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
- s is V1() V4( NAT ) V6() total complex-valued ext-real-valued real-valued set
- 1 is V30() real ext-real non positive set
(- 1) (#) s is V1() V4( NAT ) V6() total complex-valued ext-real-valued real-valued set
k + (- s) is V1() V4( NAT ) V6() total complex-valued ext-real-valued real-valued set
n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
(k - s) . n is V30() real ext-real Element of REAL
k . n is V30() real ext-real Element of REAL
s . n is V30() real ext-real Element of REAL
(k . n) - (s . n) is V30() real ext-real Element of REAL
x0 - (s . n) is V30() real ext-real Element of REAL
n + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
1 / (n + 1) is V30() real ext-real non negative Element of REAL
x0 - (1 / (n + 1)) is V30() real ext-real Element of REAL
f . n is V30() real ext-real Element of REAL
k . 0 is V30() real ext-real Element of REAL
lim k is V30() real ext-real Element of REAL
lim s is V30() real ext-real Element of REAL
lim (k - s) is V30() real ext-real Element of REAL
x0 - 0 is V30() real ext-real Element of REAL
n is set
g2 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
f . g2 is V30() real ext-real Element of REAL
n is set
g2 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
f . g2 is V30() real ext-real Element of REAL
{ b₁ where b₁ is V30() real ext-real Element of REAL : not x0 <= b₁ } is set
x0 is V30() real ext-real Element of REAL
right_open_halfline x0 is V71() V72() V73() Element of K19(REAL)
K213(x0,+infty) is set
f is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim f is V30() real ext-real Element of REAL
rng f is V71() V72() V73() Element of K19(REAL)
r is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom r is V71() V72() V73() Element of K19(REAL)
(dom r) /\ (right_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
NAT --> x0 is V1() V4( NAT ) V5( REAL ) V6() constant non empty total quasi_total T-Sequence-like complex-valued ext-real-valued real-valued convergent Element of K19(K20(NAT,REAL))
k is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
k + s is V1() V4( NAT ) V5( REAL ) V6() 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 V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
(k + s) . n is V30() real ext-real Element of REAL
k . n is V30() real ext-real Element of REAL
s . n is V30() real ext-real Element of REAL
(k . n) + (s . n) is V30() real ext-real Element of REAL
x0 + (s . n) is V30() real ext-real Element of REAL
n + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
1 / (n + 1) is V30() real ext-real non negative Element of REAL
x0 + (1 / (n + 1)) is V30() real ext-real Element of REAL
f . n is V30() real ext-real Element of REAL
k . 0 is V30() real ext-real Element of REAL
lim k is V30() real ext-real Element of REAL
lim s is V30() real ext-real Element of REAL
lim (k + s) is V30() real ext-real Element of REAL
x0 + 0 is V30() real ext-real Element of REAL
n is set
g2 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
f . g2 is V30() real ext-real Element of REAL
n is set
g2 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
f . g2 is V30() real ext-real Element of REAL
{ b₁ where b₁ is V30() real ext-real Element of REAL : not b₁ <= x0 } is set
x0 is V30() real ext-real Element of REAL
f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom f is V71() V72() V73() Element of K19(REAL)
left_open_halfline x0 is V71() V72() V73() Element of K19(REAL)
K213(-infty,x0) is set
(dom f) /\ (left_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
r is V30() real ext-real Element of REAL
s is V30() real ext-real Element of REAL
s is V30() real ext-real Element of REAL
k is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
k + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
1 / (k + 1) is V30() real ext-real non negative Element of REAL
x0 - (1 / (k + 1)) is V30() real ext-real Element of REAL
n is V30() real ext-real Element of REAL
f . n is V30() real ext-real Element of REAL
(f . n) - r is V30() real ext-real Element of REAL
abs ((f . n) - r) is V30() real ext-real Element of REAL
g2 is V30() real ext-real Element of REAL
f . g2 is V30() real ext-real Element of REAL
(f . g2) - r is V30() real ext-real Element of REAL
abs ((f . g2) - r) is V30() real ext-real Element of REAL
k is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
rng k is V71() V72() V73() Element of K19(REAL)
lim k is V30() real ext-real Element of REAL
f /* k is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim (f /* k) is V30() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
(f /* k) . n is V30() real ext-real Element of REAL
((f /* k) . n) - r is V30() real ext-real Element of REAL
abs (((f /* k) . n) - r) is V30() real ext-real Element of REAL
k . n is V30() real ext-real Element of REAL
f . (k . n) is V30() real ext-real Element of REAL
(f . (k . n)) - r is V30() real ext-real Element of REAL
abs ((f . (k . n)) - r) is V30() real ext-real Element of REAL
r is V30() real ext-real Element of REAL
s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim s is V30() real ext-real Element of REAL
rng s is V71() V72() V73() Element of K19(REAL)
left_open_halfline x0 is V71() V72() V73() Element of K19(REAL)
K213(-infty,x0) is set
(dom f) /\ (left_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
k is V30() real ext-real set
n is V30() real ext-real Element of REAL
g2 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
g is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
s . g is V30() real ext-real Element of REAL
{ b₁ where b₁ is V30() real ext-real Element of REAL : not x0 <= b₁ } is set
f . (s . g) is V30() real ext-real Element of REAL
(f . (s . g)) - r is V30() real ext-real Element of REAL
abs ((f . (s . g)) - r) is V30() real ext-real Element of REAL
n is V30() real ext-real Element of REAL
f /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f /* s) . g is V30() real ext-real Element of REAL
((f /* s) . g) - r is V30() real ext-real Element of REAL
abs (((f /* s) . g) - r) is V30() real ext-real Element of REAL
lim (f /* s) is V30() real ext-real Element of REAL
x0 is V30() real ext-real Element of REAL
f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom f is V71() V72() V73() Element of K19(REAL)
r is V30() real ext-real Element of REAL
s is V30() real ext-real Element of REAL
r is V30() real ext-real Element of REAL
s is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
s + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
1 / (s + 1) is V30() real ext-real non negative Element of REAL
x0 - (1 / (s + 1)) is V30() real ext-real Element of REAL
k is V30() real ext-real Element of REAL
f . k is V30() real ext-real Element of REAL
n is V30() real ext-real Element of REAL
f . n is V30() real ext-real Element of REAL
s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
rng s is V71() V72() V73() Element of K19(REAL)
left_open_halfline x0 is V71() V72() V73() Element of K19(REAL)
K213(-infty,x0) is set
(dom f) /\ (left_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
lim s is V30() real ext-real Element of REAL
f /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
k is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
(f /* s) . k is V30() real ext-real Element of REAL
s . k is V30() real ext-real Element of REAL
f . (s . k) is V30() real ext-real Element of REAL
r is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim r is V30() real ext-real Element of REAL
rng r is V71() V72() V73() Element of K19(REAL)
left_open_halfline x0 is V71() V72() V73() Element of K19(REAL)
K213(-infty,x0) is set
(dom f) /\ (left_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
s is V30() real ext-real Element of REAL
k is V30() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
g2 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
r . n is V30() real ext-real Element of REAL
{ b₁ where b₁ is V30() real ext-real Element of REAL : not x0 <= b₁ } is set
f . (r . n) is V30() real ext-real Element of REAL
g is V30() real ext-real Element of REAL
f /* r is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f /* r) . n is V30() real ext-real Element of REAL
x0 is V30() real ext-real Element of REAL
f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom f is V71() V72() V73() Element of K19(REAL)
r is V30() real ext-real Element of REAL
s is V30() real ext-real Element of REAL
r is V30() real ext-real Element of REAL
s is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
s + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
1 / (s + 1) is V30() real ext-real non negative Element of REAL
x0 - (1 / (s + 1)) is V30() real ext-real Element of REAL
k is V30() real ext-real Element of REAL
f . k is V30() real ext-real Element of REAL
n is V30() real ext-real Element of REAL
f . n is V30() real ext-real Element of REAL
s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
rng s is V71() V72() V73() Element of K19(REAL)
left_open_halfline x0 is V71() V72() V73() Element of K19(REAL)
K213(-infty,x0) is set
(dom f) /\ (left_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
lim s is V30() real ext-real Element of REAL
f /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
k is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
(f /* s) . k is V30() real ext-real Element of REAL
s . k is V30() real ext-real Element of REAL
f . (s . k) is V30() real ext-real Element of REAL
r is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim r is V30() real ext-real Element of REAL
rng r is V71() V72() V73() Element of K19(REAL)
left_open_halfline x0 is V71() V72() V73() Element of K19(REAL)
K213(-infty,x0) is set
(dom f) /\ (left_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
s is V30() real ext-real Element of REAL
k is V30() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
g2 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
r . n is V30() real ext-real Element of REAL
{ b₁ where b₁ is V30() real ext-real Element of REAL : not x0 <= b₁ } is set
f . (r . n) is V30() real ext-real Element of REAL
g is V30() real ext-real Element of REAL
f /* r is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f /* r) . n is V30() real ext-real Element of REAL
x0 is V30() real ext-real Element of REAL
f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom f is V71() V72() V73() Element of K19(REAL)
right_open_halfline x0 is V71() V72() V73() Element of K19(REAL)
K213(x0,+infty) is set
(dom f) /\ (right_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
r is V30() real ext-real Element of REAL
s is V30() real ext-real Element of REAL
s is V30() real ext-real Element of REAL
k is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
k + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
1 / (k + 1) is V30() real ext-real non negative Element of REAL
x0 + (1 / (k + 1)) is V30() real ext-real Element of REAL
n is V30() real ext-real Element of REAL
f . n is V30() real ext-real Element of REAL
(f . n) - r is V30() real ext-real Element of REAL
abs ((f . n) - r) is V30() real ext-real Element of REAL
g2 is V30() real ext-real Element of REAL
f . g2 is V30() real ext-real Element of REAL
(f . g2) - r is V30() real ext-real Element of REAL
abs ((f . g2) - r) is V30() real ext-real Element of REAL
k is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
rng k is V71() V72() V73() Element of K19(REAL)
lim k is V30() real ext-real Element of REAL
f /* k is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim (f /* k) is V30() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
(f /* k) . n is V30() real ext-real Element of REAL
((f /* k) . n) - r is V30() real ext-real Element of REAL
abs (((f /* k) . n) - r) is V30() real ext-real Element of REAL
k . n is V30() real ext-real Element of REAL
f . (k . n) is V30() real ext-real Element of REAL
(f . (k . n)) - r is V30() real ext-real Element of REAL
abs ((f . (k . n)) - r) is V30() real ext-real Element of REAL
r is V30() real ext-real Element of REAL
s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim s is V30() real ext-real Element of REAL
rng s is V71() V72() V73() Element of K19(REAL)
right_open_halfline x0 is V71() V72() V73() Element of K19(REAL)
K213(x0,+infty) is set
(dom f) /\ (right_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
k is V30() real ext-real set
n is V30() real ext-real Element of REAL
g2 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
g is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
s . g is V30() real ext-real Element of REAL
{ b₁ where b₁ is V30() real ext-real Element of REAL : not b₁ <= x0 } is set
f . (s . g) is V30() real ext-real Element of REAL
(f . (s . g)) - r is V30() real ext-real Element of REAL
abs ((f . (s . g)) - r) is V30() real ext-real Element of REAL
n is V30() real ext-real Element of REAL
f /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f /* s) . g is V30() real ext-real Element of REAL
((f /* s) . g) - r is V30() real ext-real Element of REAL
abs (((f /* s) . g) - r) is V30() real ext-real Element of REAL
lim (f /* s) is V30() real ext-real Element of REAL
x0 is V30() real ext-real Element of REAL
f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom f is V71() V72() V73() Element of K19(REAL)
r is V30() real ext-real Element of REAL
s is V30() real ext-real Element of REAL
r is V30() real ext-real Element of REAL
s is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
s + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
1 / (s + 1) is V30() real ext-real non negative Element of REAL
x0 + (1 / (s + 1)) is V30() real ext-real Element of REAL
k is V30() real ext-real Element of REAL
f . k is V30() real ext-real Element of REAL
n is V30() real ext-real Element of REAL
f . n is V30() real ext-real Element of REAL
s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
rng s is V71() V72() V73() Element of K19(REAL)
right_open_halfline x0 is V71() V72() V73() Element of K19(REAL)
K213(x0,+infty) is set
(dom f) /\ (right_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
lim s is V30() real ext-real Element of REAL
f /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
k is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
(f /* s) . k is V30() real ext-real Element of REAL
s . k is V30() real ext-real Element of REAL
f . (s . k) is V30() real ext-real Element of REAL
r is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim r is V30() real ext-real Element of REAL
rng r is V71() V72() V73() Element of K19(REAL)
right_open_halfline x0 is V71() V72() V73() Element of K19(REAL)
K213(x0,+infty) is set
(dom f) /\ (right_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
s is V30() real ext-real Element of REAL
k is V30() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
g2 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
r . n is V30() real ext-real Element of REAL
{ b₁ where b₁ is V30() real ext-real Element of REAL : not b₁ <= x0 } is set
f . (r . n) is V30() real ext-real Element of REAL
g is V30() real ext-real Element of REAL
f /* r is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f /* r) . n is V30() real ext-real Element of REAL
x0 is V30() real ext-real Element of REAL
f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom f is V71() V72() V73() Element of K19(REAL)
r is V30() real ext-real Element of REAL
s is V30() real ext-real Element of REAL
r is V30() real ext-real Element of REAL
s is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
s + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
1 / (s + 1) is V30() real ext-real non negative Element of REAL
x0 + (1 / (s + 1)) is V30() real ext-real Element of REAL
k is V30() real ext-real Element of REAL
f . k is V30() real ext-real Element of REAL
n is V30() real ext-real Element of REAL
f . n is V30() real ext-real Element of REAL
s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
rng s is V71() V72() V73() Element of K19(REAL)
right_open_halfline x0 is V71() V72() V73() Element of K19(REAL)
K213(x0,+infty) is set
(dom f) /\ (right_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
lim s is V30() real ext-real Element of REAL
f /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
k is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
(f /* s) . k is V30() real ext-real Element of REAL
s . k is V30() real ext-real Element of REAL
f . (s . k) is V30() real ext-real Element of REAL
right_open_halfline x0 is V71() V72() V73() Element of K19(REAL)
K213(x0,+infty) is set
(dom f) /\ (right_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
r is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim r is V30() real ext-real Element of REAL
rng r is V71() V72() V73() Element of K19(REAL)
f /* r is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
x0 is V30() real ext-real Element of REAL
f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom f is V71() V72() V73() Element of K19(REAL)
r is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom r is V71() V72() V73() Element of K19(REAL)
(dom f) /\ (dom r) is V71() V72() V73() Element of K19(REAL)
f + r is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
f (#) r is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim s is V30() real ext-real Element of REAL
rng s is V71() V72() V73() Element of K19(REAL)
dom (f + r) is V71() V72() V73() Element of K19(REAL)
left_open_halfline x0 is V71() V72() V73() Element of K19(REAL)
K213(-infty,x0) is set
(dom (f + r)) /\ (left_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
(dom r) /\ (left_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
r /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(dom f) /\ (left_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
f /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f /* s) + (r /* s) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f + r) /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim s is V30() real ext-real Element of REAL
rng s is V71() V72() V73() Element of K19(REAL)
dom (f (#) r) is V71() V72() V73() Element of K19(REAL)
(dom (f (#) r)) /\ (left_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
r /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
f /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f /* s) (#) (r /* s) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f (#) r) /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
s is V30() real ext-real Element of REAL
k is V30() real ext-real Element of REAL
n is V30() real ext-real Element of REAL
s is V30() real ext-real Element of REAL
k is V30() real ext-real Element of REAL
n is V30() real ext-real Element of REAL
x0 is V30() real ext-real Element of REAL
f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom f is V71() V72() V73() Element of K19(REAL)
r is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom r is V71() V72() V73() Element of K19(REAL)
(dom f) /\ (dom r) is V71() V72() V73() Element of K19(REAL)
f + r is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
f (#) r is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim s is V30() real ext-real Element of REAL
rng s is V71() V72() V73() Element of K19(REAL)
dom (f + r) is V71() V72() V73() Element of K19(REAL)
left_open_halfline x0 is V71() V72() V73() Element of K19(REAL)
K213(-infty,x0) is set
(dom (f + r)) /\ (left_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
(dom r) /\ (left_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
r /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(dom f) /\ (left_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
f /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f /* s) + (r /* s) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f + r) /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim s is V30() real ext-real Element of REAL
rng s is V71() V72() V73() Element of K19(REAL)
dom (f (#) r) is V71() V72() V73() Element of K19(REAL)
(dom (f (#) r)) /\ (left_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
r /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
f /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f /* s) (#) (r /* s) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f (#) r) /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
s is V30() real ext-real Element of REAL
k is V30() real ext-real Element of REAL
n is V30() real ext-real Element of REAL
s is V30() real ext-real Element of REAL
k is V30() real ext-real Element of REAL
n is V30() real ext-real Element of REAL
x0 is V30() real ext-real Element of REAL
f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom f is V71() V72() V73() Element of K19(REAL)
r is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom r is V71() V72() V73() Element of K19(REAL)
(dom f) /\ (dom r) is V71() V72() V73() Element of K19(REAL)
f + r is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
f (#) r is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim s is V30() real ext-real Element of REAL
rng s is V71() V72() V73() Element of K19(REAL)
dom (f + r) is V71() V72() V73() Element of K19(REAL)
right_open_halfline x0 is V71() V72() V73() Element of K19(REAL)
K213(x0,+infty) is set
(dom (f + r)) /\ (right_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
(dom r) /\ (right_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
r /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(dom f) /\ (right_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
f /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f /* s) + (r /* s) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f + r) /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim s is V30() real ext-real Element of REAL
rng s is V71() V72() V73() Element of K19(REAL)
dom (f (#) r) is V71() V72() V73() Element of K19(REAL)
(dom (f (#) r)) /\ (right_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
r /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
f /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f /* s) (#) (r /* s) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f (#) r) /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
s is V30() real ext-real Element of REAL
k is V30() real ext-real Element of REAL
n is V30() real ext-real Element of REAL
s is V30() real ext-real Element of REAL
k is V30() real ext-real Element of REAL
n is V30() real ext-real Element of REAL
x0 is V30() real ext-real Element of REAL
f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom f is V71() V72() V73() Element of K19(REAL)
r is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom r is V71() V72() V73() Element of K19(REAL)
(dom f) /\ (dom r) is V71() V72() V73() Element of K19(REAL)
f + r is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
f (#) r is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim s is V30() real ext-real Element of REAL
rng s is V71() V72() V73() Element of K19(REAL)
dom (f + r) is V71() V72() V73() Element of K19(REAL)
right_open_halfline x0 is V71() V72() V73() Element of K19(REAL)
K213(x0,+infty) is set
(dom (f + r)) /\ (right_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
(dom r) /\ (right_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
r /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(dom f) /\ (right_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
f /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f /* s) + (r /* s) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f + r) /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim s is V30() real ext-real Element of REAL
rng s is V71() V72() V73() Element of K19(REAL)
dom (f (#) r) is V71() V72() V73() Element of K19(REAL)
(dom (f (#) r)) /\ (right_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
r /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
f /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f /* s) (#) (r /* s) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f (#) r) /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
s is V30() real ext-real Element of REAL
k is V30() real ext-real Element of REAL
n is V30() real ext-real Element of REAL
s is V30() real ext-real Element of REAL
k is V30() real ext-real Element of REAL
n is V30() real ext-real Element of REAL
x0 is V30() real ext-real Element of REAL
f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
r is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
f + r is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom (f + r) is V71() V72() V73() Element of K19(REAL)
s is V30() real ext-real Element of REAL
x0 - s is V30() real ext-real Element of REAL
].(x0 - s),x0.[ is V71() V72() V73() Element of K19(REAL)
r | ].(x0 - s),x0.[ is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
k is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim k is V30() real ext-real Element of REAL
rng k is V71() V72() V73() Element of K19(REAL)
left_open_halfline x0 is V71() V72() V73() Element of K19(REAL)
K213(-infty,x0) is set
(dom (f + r)) /\ (left_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
k ^\ n is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of k
rng (k ^\ n) is V71() V72() V73() Element of K19(REAL)
dom f is V71() V72() V73() Element of K19(REAL)
dom r is V71() V72() V73() Element of K19(REAL)
(dom f) /\ (dom r) is V71() V72() V73() Element of K19(REAL)
f /* (k ^\ n) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
r /* (k ^\ n) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f /* (k ^\ n)) + (r /* (k ^\ n)) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f + r) /* (k ^\ n) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f + r) /* k is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
((f + r) /* k) ^\ n is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of (f + r) /* k
(dom f) /\ (left_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
].(x0 - s),x0.[ /\ (dom r) is V71() V72() V73() Element of K19(REAL)
g2 is V30() real ext-real set
g2 - 1 is V30() real ext-real Element of REAL
g is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
g + n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
k . (g + n) is V30() real ext-real Element of REAL
(k ^\ n) . g is V30() real ext-real Element of REAL
{ b₁ where b₁ is V30() real ext-real Element of REAL : not x0 <= b₁ } is set
{ b₁ where b₁ is V30() real ext-real Element of REAL : ( not b₁ <= x0 - s & not x0 <= b₁ ) } is set
n is V30() real ext-real Element of REAL
r . ((k ^\ n) . g) is V30() real ext-real Element of REAL
(r . ((k ^\ n) . g)) - 0 is V30() real ext-real Element of REAL
(r /* (k ^\ n)) . g is V30() real ext-real Element of REAL
n is V30() real ext-real Element of REAL
g2 is V30() real ext-real Element of REAL
lim (k ^\ n) is V30() real ext-real Element of REAL
x0 is V30() real ext-real Element of REAL
f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
r is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
f (#) r is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom (f (#) r) is V71() V72() V73() Element of K19(REAL)
dom r is V71() V72() V73() Element of K19(REAL)
s is V30() real ext-real Element of REAL
k is V30() real ext-real Element of REAL
x0 - s is V30() real ext-real Element of REAL
].(x0 - s),x0.[ is V71() V72() V73() Element of K19(REAL)
(dom r) /\ ].(x0 - s),x0.[ is V71() V72() V73() Element of K19(REAL)
n is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim n is V30() real ext-real Element of REAL
rng n is V71() V72() V73() Element of K19(REAL)
left_open_halfline x0 is V71() V72() V73() Element of K19(REAL)
K213(-infty,x0) is set
(dom (f (#) r)) /\ (left_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
g2 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
dom f is V71() V72() V73() Element of K19(REAL)
(dom f) /\ (dom r) is V71() V72() V73() Element of K19(REAL)
n ^\ g2 is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of n
rng (n ^\ g2) is V71() V72() V73() Element of K19(REAL)
n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
n + g2 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
n . (n + g2) is V30() real ext-real Element of REAL
(n ^\ g2) . n is V30() real ext-real Element of REAL
{ b₁ where b₁ is V30() real ext-real Element of REAL : not x0 <= b₁ } is set
{ b₁ where b₁ is V30() real ext-real Element of REAL : ( not b₁ <= x0 - s & not x0 <= b₁ ) } is set
g is V30() real ext-real Element of REAL
r . ((n ^\ g2) . n) is V30() real ext-real Element of REAL
r /* (n ^\ g2) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(r /* (n ^\ g2)) . n is V30() real ext-real Element of REAL
(dom f) /\ (left_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
lim (n ^\ g2) is V30() real ext-real Element of REAL
f /* (n ^\ g2) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f /* (n ^\ g2)) (#) (r /* (n ^\ g2)) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f (#) r) /* (n ^\ g2) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f (#) r) /* n is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
((f (#) r) /* n) ^\ g2 is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of (f (#) r) /* n
x0 is V30() real ext-real Element of REAL
f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
r is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
f + r is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom (f + r) is V71() V72() V73() Element of K19(REAL)
s is V30() real ext-real Element of REAL
x0 + s is V30() real ext-real Element of REAL
].x0,(x0 + s).[ is V71() V72() V73() Element of K19(REAL)
r | ].x0,(x0 + s).[ is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
k is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim k is V30() real ext-real Element of REAL
rng k is V71() V72() V73() Element of K19(REAL)
right_open_halfline x0 is V71() V72() V73() Element of K19(REAL)
K213(x0,+infty) is set
(dom (f + r)) /\ (right_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
k ^\ n is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of k
rng (k ^\ n) is V71() V72() V73() Element of K19(REAL)
dom f is V71() V72() V73() Element of K19(REAL)
dom r is V71() V72() V73() Element of K19(REAL)
(dom f) /\ (dom r) is V71() V72() V73() Element of K19(REAL)
f /* (k ^\ n) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
r /* (k ^\ n) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f /* (k ^\ n)) + (r /* (k ^\ n)) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f + r) /* (k ^\ n) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f + r) /* k is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
((f + r) /* k) ^\ n is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of (f + r) /* k
(dom f) /\ (right_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
].x0,(x0 + s).[ /\ (dom r) is V71() V72() V73() Element of K19(REAL)
g2 is V30() real ext-real set
g2 - 1 is V30() real ext-real Element of REAL
g is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
g + n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
k . (g + n) is V30() real ext-real Element of REAL
(k ^\ n) . g is V30() real ext-real Element of REAL
{ b₁ where b₁ is V30() real ext-real Element of REAL : not b₁ <= x0 } is set
{ b₁ where b₁ is V30() real ext-real Element of REAL : ( not b₁ <= x0 & not x0 + s <= b₁ ) } is set
n is V30() real ext-real Element of REAL
r . ((k ^\ n) . g) is V30() real ext-real Element of REAL
(r . ((k ^\ n) . g)) - 0 is V30() real ext-real Element of REAL
(r /* (k ^\ n)) . g is V30() real ext-real Element of REAL
n is V30() real ext-real Element of REAL
g2 is V30() real ext-real Element of REAL
lim (k ^\ n) is V30() real ext-real Element of REAL
x0 is V30() real ext-real Element of REAL
f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
r is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
f (#) r is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom (f (#) r) is V71() V72() V73() Element of K19(REAL)
dom r is V71() V72() V73() Element of K19(REAL)
s is V30() real ext-real Element of REAL
k is V30() real ext-real Element of REAL
x0 + s is V30() real ext-real Element of REAL
].x0,(x0 + s).[ is V71() V72() V73() Element of K19(REAL)
(dom r) /\ ].x0,(x0 + s).[ is V71() V72() V73() Element of K19(REAL)
n is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim n is V30() real ext-real Element of REAL
rng n is V71() V72() V73() Element of K19(REAL)
right_open_halfline x0 is V71() V72() V73() Element of K19(REAL)
K213(x0,+infty) is set
(dom (f (#) r)) /\ (right_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
g2 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
dom f is V71() V72() V73() Element of K19(REAL)
(dom f) /\ (dom r) is V71() V72() V73() Element of K19(REAL)
n ^\ g2 is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of n
rng (n ^\ g2) is V71() V72() V73() Element of K19(REAL)
n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
n + g2 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
n . (n + g2) is V30() real ext-real Element of REAL
(n ^\ g2) . n is V30() real ext-real Element of REAL
{ b₁ where b₁ is V30() real ext-real Element of REAL : not b₁ <= x0 } is set
{ b₁ where b₁ is V30() real ext-real Element of REAL : ( not b₁ <= x0 & not x0 + s <= b₁ ) } is set
g is V30() real ext-real Element of REAL
r . ((n ^\ g2) . n) is V30() real ext-real Element of REAL
r /* (n ^\ g2) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(r /* (n ^\ g2)) . n is V30() real ext-real Element of REAL
(dom f) /\ (right_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
lim (n ^\ g2) is V30() real ext-real Element of REAL
f /* (n ^\ g2) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f /* (n ^\ g2)) (#) (r /* (n ^\ g2)) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f (#) r) /* (n ^\ g2) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f (#) r) /* n is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
((f (#) r) /* n) ^\ g2 is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of (f (#) r) /* n
x0 is V30() real ext-real Element of REAL
f is V30() real ext-real Element of REAL
r is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
f (#) r is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom r is V71() V72() V73() Element of K19(REAL)
left_open_halfline x0 is V71() V72() V73() Element of K19(REAL)
K213(-infty,x0) is set
(dom r) /\ (left_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
dom (f (#) r) is V71() V72() V73() Element of K19(REAL)
s is V30() real ext-real Element of REAL
k is V30() real ext-real Element of REAL
(dom (f (#) r)) /\ (left_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim s is V30() real ext-real Element of REAL
rng s is V71() V72() V73() Element of K19(REAL)
(f (#) r) /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
r /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
f (#) (r /* s) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
dom (f (#) r) is V71() V72() V73() Element of K19(REAL)
s is V30() real ext-real Element of REAL
k is V30() real ext-real Element of REAL
(dom (f (#) r)) /\ (left_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim s is V30() real ext-real Element of REAL
rng s is V71() V72() V73() Element of K19(REAL)
(f (#) r) /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
r /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
f (#) (r /* s) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
dom (f (#) r) is V71() V72() V73() Element of K19(REAL)
s is V30() real ext-real Element of REAL
k is V30() real ext-real Element of REAL
(dom (f (#) r)) /\ (left_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim s is V30() real ext-real Element of REAL
rng s is V71() V72() V73() Element of K19(REAL)
(f (#) r) /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
r /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
f (#) (r /* s) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
dom (f (#) r) is V71() V72() V73() Element of K19(REAL)
s is V30() real ext-real Element of REAL
k is V30() real ext-real Element of REAL
(dom (f (#) r)) /\ (left_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim s is V30() real ext-real Element of REAL
rng s is V71() V72() V73() Element of K19(REAL)
(f (#) r) /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
r /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
f (#) (r /* s) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
x0 is V30() real ext-real Element of REAL
f is V30() real ext-real Element of REAL
r is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
f (#) r is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom r is V71() V72() V73() Element of K19(REAL)
right_open_halfline x0 is V71() V72() V73() Element of K19(REAL)
K213(x0,+infty) is set
(dom r) /\ (right_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
dom (f (#) r) is V71() V72() V73() Element of K19(REAL)
s is V30() real ext-real Element of REAL
k is V30() real ext-real Element of REAL
(dom (f (#) r)) /\ (right_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim s is V30() real ext-real Element of REAL
rng s is V71() V72() V73() Element of K19(REAL)
(f (#) r) /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
r /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
f (#) (r /* s) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
dom (f (#) r) is V71() V72() V73() Element of K19(REAL)
s is V30() real ext-real Element of REAL
k is V30() real ext-real Element of REAL
(dom (f (#) r)) /\ (right_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim s is V30() real ext-real Element of REAL
rng s is V71() V72() V73() Element of K19(REAL)
(f (#) r) /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
r /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
f (#) (r /* s) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
dom (f (#) r) is V71() V72() V73() Element of K19(REAL)
s is V30() real ext-real Element of REAL
k is V30() real ext-real Element of REAL
(dom (f (#) r)) /\ (right_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim s is V30() real ext-real Element of REAL
rng s is V71() V72() V73() Element of K19(REAL)
(f (#) r) /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
r /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
f (#) (r /* s) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
dom (f (#) r) is V71() V72() V73() Element of K19(REAL)
s is V30() real ext-real Element of REAL
k is V30() real ext-real Element of REAL
(dom (f (#) r)) /\ (right_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim s is V30() real ext-real Element of REAL
rng s is V71() V72() V73() Element of K19(REAL)
(f (#) r) /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
r /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
f (#) (r /* s) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
x0 is V30() real ext-real Element of REAL
f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
abs f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
r is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim r is V30() real ext-real Element of REAL
rng r is V71() V72() V73() Element of K19(REAL)
dom (abs f) is V71() V72() V73() Element of K19(REAL)
left_open_halfline x0 is V71() V72() V73() Element of K19(REAL)
K213(-infty,x0) is set
(dom (abs f)) /\ (left_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
dom f is V71() V72() V73() Element of K19(REAL)
(dom f) /\ (left_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
f /* r is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
abs (f /* r) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(abs f) /* r is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
r is V30() real ext-real Element of REAL
s is V30() real ext-real Element of REAL
k is V30() real ext-real Element of REAL
r is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim r is V30() real ext-real Element of REAL
rng r is V71() V72() V73() Element of K19(REAL)
dom (abs f) is V71() V72() V73() Element of K19(REAL)
left_open_halfline x0 is V71() V72() V73() Element of K19(REAL)
K213(-infty,x0) is set
(dom (abs f)) /\ (left_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
dom f is V71() V72() V73() Element of K19(REAL)
(dom f) /\ (left_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
f /* r is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
abs (f /* r) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(abs f) /* r is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
r is V30() real ext-real Element of REAL
s is V30() real ext-real Element of REAL
k is V30() real ext-real Element of REAL
x0 is V30() real ext-real Element of REAL
f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
abs f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
r is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim r is V30() real ext-real Element of REAL
rng r is V71() V72() V73() Element of K19(REAL)
dom (abs f) is V71() V72() V73() Element of K19(REAL)
right_open_halfline x0 is V71() V72() V73() Element of K19(REAL)
K213(x0,+infty) is set
(dom (abs f)) /\ (right_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
dom f is V71() V72() V73() Element of K19(REAL)
(dom f) /\ (right_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
f /* r is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
abs (f /* r) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(abs f) /* r is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
r is V30() real ext-real Element of REAL
s is V30() real ext-real Element of REAL
k is V30() real ext-real Element of REAL
r is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim r is V30() real ext-real Element of REAL
rng r is V71() V72() V73() Element of K19(REAL)
dom (abs f) is V71() V72() V73() Element of K19(REAL)
right_open_halfline x0 is V71() V72() V73() Element of K19(REAL)
K213(x0,+infty) is set
(dom (abs f)) /\ (right_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
dom f is V71() V72() V73() Element of K19(REAL)
(dom f) /\ (right_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
f /* r is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
abs (f /* r) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(abs f) /* r is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
r is V30() real ext-real Element of REAL
s is V30() real ext-real Element of REAL
k is V30() real ext-real Element of REAL
x0 is V30() real ext-real Element of REAL
f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom f is V71() V72() V73() Element of K19(REAL)
r is V30() real ext-real Element of REAL
x0 - r is V30() real ext-real Element of REAL
].(x0 - r),x0.[ is V71() V72() V73() Element of K19(REAL)
f | ].(x0 - r),x0.[ is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
s is V30() real ext-real Element of REAL
left_open_halfline x0 is V71() V72() V73() Element of K19(REAL)
K213(-infty,x0) is set
(dom f) /\ (left_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim s is V30() real ext-real Element of REAL
rng s is V71() V72() V73() Element of K19(REAL)
f /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
].(x0 - r),x0.[ /\ (dom f) is V71() V72() V73() Element of K19(REAL)
k is V30() real ext-real Element of REAL
n is set
f . n is V30() real ext-real Element of REAL
g2 is V30() real ext-real Element of REAL
{ b₁ where b₁ is V30() real ext-real Element of REAL : ( not b₁ <= x0 - r & not x0 <= b₁ ) } is set
n is V30() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
s . n is V30() real ext-real Element of REAL
{ b₁ where b₁ is V30() real ext-real Element of REAL : not x0 <= b₁ } is set
g is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
c₁₁ is V30() real ext-real Element of REAL
c₁₁ is V30() real ext-real Element of REAL
f . g2 is V30() real ext-real Element of REAL
f . (s . n) is V30() real ext-real Element of REAL
(f /* s) . n is V30() real ext-real Element of REAL
r is V30() real ext-real Element of REAL
f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
x0 is V30() real ext-real Element of REAL
x0 - r is V30() real ext-real Element of REAL
].(x0 - r),x0.[ is V71() V72() V73() Element of K19(REAL)
f | ].(x0 - r),x0.[ is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom f is V71() V72() V73() Element of K19(REAL)
x0 is V30() real ext-real Element of REAL
f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom f is V71() V72() V73() Element of K19(REAL)
r is V30() real ext-real Element of REAL
x0 - r is V30() real ext-real Element of REAL
].(x0 - r),x0.[ is V71() V72() V73() Element of K19(REAL)
f | ].(x0 - r),x0.[ is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
s is V30() real ext-real Element of REAL
left_open_halfline x0 is V71() V72() V73() Element of K19(REAL)
K213(-infty,x0) is set
(dom f) /\ (left_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim s is V30() real ext-real Element of REAL
rng s is V71() V72() V73() Element of K19(REAL)
f /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
].(x0 - r),x0.[ /\ (dom f) is V71() V72() V73() Element of K19(REAL)
k is V30() real ext-real Element of REAL
n is set
f . n is V30() real ext-real Element of REAL
g2 is V30() real ext-real Element of REAL
{ b₁ where b₁ is V30() real ext-real Element of REAL : ( not b₁ <= x0 - r & not x0 <= b₁ ) } is set
n is V30() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
s . n is V30() real ext-real Element of REAL
{ b₁ where b₁ is V30() real ext-real Element of REAL : not x0 <= b₁ } is set
g is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
c₁₁ is V30() real ext-real Element of REAL
c₁₁ is V30() real ext-real Element of REAL
f . (s . n) is V30() real ext-real Element of REAL
f . g2 is V30() real ext-real Element of REAL
(f /* s) . n is V30() real ext-real Element of REAL
r is V30() real ext-real Element of REAL
f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
x0 is V30() real ext-real Element of REAL
x0 - r is V30() real ext-real Element of REAL
].(x0 - r),x0.[ is V71() V72() V73() Element of K19(REAL)
f | ].(x0 - r),x0.[ is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom f is V71() V72() V73() Element of K19(REAL)
x0 is V30() real ext-real Element of REAL
f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom f is V71() V72() V73() Element of K19(REAL)
r is V30() real ext-real Element of REAL
x0 + r is V30() real ext-real Element of REAL
].x0,(x0 + r).[ is V71() V72() V73() Element of K19(REAL)
f | ].x0,(x0 + r).[ is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
s is V30() real ext-real Element of REAL
right_open_halfline x0 is V71() V72() V73() Element of K19(REAL)
K213(x0,+infty) is set
(dom f) /\ (right_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim s is V30() real ext-real Element of REAL
rng s is V71() V72() V73() Element of K19(REAL)
f /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
].x0,(x0 + r).[ /\ (dom f) is V71() V72() V73() Element of K19(REAL)
k is V30() real ext-real Element of REAL
n is set
f . n is V30() real ext-real Element of REAL
g2 is V30() real ext-real Element of REAL
{ b₁ where b₁ is V30() real ext-real Element of REAL : ( not b₁ <= x0 & not x0 + r <= b₁ ) } is set
n is V30() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
s . n is V30() real ext-real Element of REAL
{ b₁ where b₁ is V30() real ext-real Element of REAL : not b₁ <= x0 } is set
g is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
c₁₁ is V30() real ext-real Element of REAL
c₁₁ is V30() real ext-real Element of REAL
f . g2 is V30() real ext-real Element of REAL
f . (s . n) is V30() real ext-real Element of REAL
(f /* s) . n is V30() real ext-real Element of REAL
r is V30() real ext-real Element of REAL
f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
x0 is V30() real ext-real Element of REAL
x0 + r is V30() real ext-real Element of REAL
].x0,(x0 + r).[ is V71() V72() V73() Element of K19(REAL)
f | ].x0,(x0 + r).[ is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom f is V71() V72() V73() Element of K19(REAL)
x0 is V30() real ext-real Element of REAL
f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom f is V71() V72() V73() Element of K19(REAL)
r is V30() real ext-real Element of REAL
x0 + r is V30() real ext-real Element of REAL
].x0,(x0 + r).[ is V71() V72() V73() Element of K19(REAL)
f | ].x0,(x0 + r).[ is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
s is V30() real ext-real Element of REAL
right_open_halfline x0 is V71() V72() V73() Element of K19(REAL)
K213(x0,+infty) is set
(dom f) /\ (right_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim s is V30() real ext-real Element of REAL
rng s is V71() V72() V73() Element of K19(REAL)
f /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
].x0,(x0 + r).[ /\ (dom f) is V71() V72() V73() Element of K19(REAL)
k is V30() real ext-real Element of REAL
n is set
f . n is V30() real ext-real Element of REAL
g2 is V30() real ext-real Element of REAL
{ b₁ where b₁ is V30() real ext-real Element of REAL : ( not b₁ <= x0 & not x0 + r <= b₁ ) } is set
n is V30() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
s . n is V30() real ext-real Element of REAL
{ b₁ where b₁ is V30() real ext-real Element of REAL : not b₁ <= x0 } is set
g is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
c₁₁ is V30() real ext-real Element of REAL
c₁₁ is V30() real ext-real Element of REAL
f . (s . n) is V30() real ext-real Element of REAL
f . g2 is V30() real ext-real Element of REAL
(f /* s) . n is V30() real ext-real Element of REAL
r is V30() real ext-real Element of REAL
f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
x0 is V30() real ext-real Element of REAL
x0 + r is V30() real ext-real Element of REAL
].x0,(x0 + r).[ is V71() V72() V73() Element of K19(REAL)
f | ].x0,(x0 + r).[ is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom f is V71() V72() V73() Element of K19(REAL)
x0 is V30() real ext-real Element of REAL
f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom f is V71() V72() V73() Element of K19(REAL)
r is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom r is V71() V72() V73() Element of K19(REAL)
s is V30() real ext-real Element of REAL
x0 - s is V30() real ext-real Element of REAL
].(x0 - s),x0.[ is V71() V72() V73() Element of K19(REAL)
(dom r) /\ ].(x0 - s),x0.[ is V71() V72() V73() Element of K19(REAL)
(dom f) /\ ].(x0 - s),x0.[ is V71() V72() V73() Element of K19(REAL)
k is V30() real ext-real Element of REAL
left_open_halfline x0 is V71() V72() V73() Element of K19(REAL)
K213(-infty,x0) is set
(dom r) /\ (left_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
k is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim k is V30() real ext-real Element of REAL
rng k is V71() V72() V73() Element of K19(REAL)
r /* k is V1() V4( NAT ) V5( REAL ) V6() 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 V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
k ^\ n is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of k
rng (k ^\ n) is V71() V72() V73() Element of K19(REAL)
g2 is set
n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
(k ^\ n) . n is V30() real ext-real Element of REAL
{ b₁ where b₁ is V30() real ext-real Element of REAL : not x0 <= b₁ } is set
n + n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
k . (n + n) is V30() real ext-real Element of REAL
{ b₁ where b₁ is V30() real ext-real Element of REAL : ( not b₁ <= x0 - s & not x0 <= b₁ ) } is set
g is V30() real ext-real Element of REAL
(dom f) /\ (left_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
g2 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
(k ^\ n) . g2 is V30() real ext-real Element of REAL
f . ((k ^\ n) . g2) is V30() real ext-real Element of REAL
r . ((k ^\ n) . g2) is V30() real ext-real Element of REAL
f /* (k ^\ n) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f /* (k ^\ n)) . g2 is V30() real ext-real Element of REAL
r /* (k ^\ n) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(r /* (k ^\ n)) . g2 is V30() real ext-real Element of REAL
lim (k ^\ n) is V30() real ext-real Element of REAL
(r /* k) ^\ n is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of r /* k
x0 is V30() real ext-real Element of REAL
f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom f is V71() V72() V73() Element of K19(REAL)
r is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom r is V71() V72() V73() Element of K19(REAL)
s is V30() real ext-real Element of REAL
x0 - s is V30() real ext-real Element of REAL
].(x0 - s),x0.[ is V71() V72() V73() Element of K19(REAL)
(dom r) /\ ].(x0 - s),x0.[ is V71() V72() V73() Element of K19(REAL)
(dom f) /\ ].(x0 - s),x0.[ is V71() V72() V73() Element of K19(REAL)
k is V30() real ext-real Element of REAL
left_open_halfline x0 is V71() V72() V73() Element of K19(REAL)
K213(-infty,x0) is set
(dom r) /\ (left_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
k is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim k is V30() real ext-real Element of REAL
rng k is V71() V72() V73() Element of K19(REAL)
r /* k is V1() V4( NAT ) V5( REAL ) V6() 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 V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
k ^\ n is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of k
rng (k ^\ n) is V71() V72() V73() Element of K19(REAL)
g2 is set
n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
(k ^\ n) . n is V30() real ext-real Element of REAL
{ b₁ where b₁ is V30() real ext-real Element of REAL : not x0 <= b₁ } is set
n + n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
k . (n + n) is V30() real ext-real Element of REAL
{ b₁ where b₁ is V30() real ext-real Element of REAL : ( not b₁ <= x0 - s & not x0 <= b₁ ) } is set
g is V30() real ext-real Element of REAL
(dom f) /\ (left_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
g2 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
(k ^\ n) . g2 is V30() real ext-real Element of REAL
r . ((k ^\ n) . g2) is V30() real ext-real Element of REAL
f . ((k ^\ n) . g2) is V30() real ext-real Element of REAL
r /* (k ^\ n) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(r /* (k ^\ n)) . g2 is V30() real ext-real Element of REAL
f /* (k ^\ n) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f /* (k ^\ n)) . g2 is V30() real ext-real Element of REAL
lim (k ^\ n) is V30() real ext-real Element of REAL
(r /* k) ^\ n is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of r /* k
x0 is V30() real ext-real Element of REAL
f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom f is V71() V72() V73() Element of K19(REAL)
r is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom r is V71() V72() V73() Element of K19(REAL)
s is V30() real ext-real Element of REAL
x0 + s is V30() real ext-real Element of REAL
].x0,(x0 + s).[ is V71() V72() V73() Element of K19(REAL)
(dom r) /\ ].x0,(x0 + s).[ is V71() V72() V73() Element of K19(REAL)
(dom f) /\ ].x0,(x0 + s).[ is V71() V72() V73() Element of K19(REAL)
k is V30() real ext-real Element of REAL
right_open_halfline x0 is V71() V72() V73() Element of K19(REAL)
K213(x0,+infty) is set
(dom r) /\ (right_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
k is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim k is V30() real ext-real Element of REAL
rng k is V71() V72() V73() Element of K19(REAL)
r /* k is V1() V4( NAT ) V5( REAL ) V6() 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 V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
k ^\ n is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of k
rng (k ^\ n) is V71() V72() V73() Element of K19(REAL)
g2 is set
n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
(k ^\ n) . n is V30() real ext-real Element of REAL
{ b₁ where b₁ is V30() real ext-real Element of REAL : not b₁ <= x0 } is set
n + n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
k . (n + n) is V30() real ext-real Element of REAL
{ b₁ where b₁ is V30() real ext-real Element of REAL : ( not b₁ <= x0 & not x0 + s <= b₁ ) } is set
g is V30() real ext-real Element of REAL
(dom f) /\ (right_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
g2 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
(k ^\ n) . g2 is V30() real ext-real Element of REAL
f . ((k ^\ n) . g2) is V30() real ext-real Element of REAL
r . ((k ^\ n) . g2) is V30() real ext-real Element of REAL
f /* (k ^\ n) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f /* (k ^\ n)) . g2 is V30() real ext-real Element of REAL
r /* (k ^\ n) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(r /* (k ^\ n)) . g2 is V30() real ext-real Element of REAL
lim (k ^\ n) is V30() real ext-real Element of REAL
(r /* k) ^\ n is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of r /* k
x0 is V30() real ext-real Element of REAL
f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom f is V71() V72() V73() Element of K19(REAL)
r is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom r is V71() V72() V73() Element of K19(REAL)
s is V30() real ext-real Element of REAL
x0 + s is V30() real ext-real Element of REAL
].x0,(x0 + s).[ is V71() V72() V73() Element of K19(REAL)
(dom r) /\ ].x0,(x0 + s).[ is V71() V72() V73() Element of K19(REAL)
(dom f) /\ ].x0,(x0 + s).[ is V71() V72() V73() Element of K19(REAL)
k is V30() real ext-real Element of REAL
right_open_halfline x0 is V71() V72() V73() Element of K19(REAL)
K213(x0,+infty) is set
(dom r) /\ (right_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
k is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim k is V30() real ext-real Element of REAL
rng k is V71() V72() V73() Element of K19(REAL)
r /* k is V1() V4( NAT ) V5( REAL ) V6() 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 V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
k ^\ n is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of k
rng (k ^\ n) is V71() V72() V73() Element of K19(REAL)
g2 is set
n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
(k ^\ n) . n is V30() real ext-real Element of REAL
{ b₁ where b₁ is V30() real ext-real Element of REAL : not b₁ <= x0 } is set
n + n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
k . (n + n) is V30() real ext-real Element of REAL
{ b₁ where b₁ is V30() real ext-real Element of REAL : ( not b₁ <= x0 & not x0 + s <= b₁ ) } is set
g is V30() real ext-real Element of REAL
(dom f) /\ (right_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
g2 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
(k ^\ n) . g2 is V30() real ext-real Element of REAL
r . ((k ^\ n) . g2) is V30() real ext-real Element of REAL
f . ((k ^\ n) . g2) is V30() real ext-real Element of REAL
r /* (k ^\ n) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(r /* (k ^\ n)) . g2 is V30() real ext-real Element of REAL
f /* (k ^\ n) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f /* (k ^\ n)) . g2 is V30() real ext-real Element of REAL
lim (k ^\ n) is V30() real ext-real Element of REAL
(r /* k) ^\ n is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of r /* k
x0 is V30() real ext-real Element of REAL
f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom f is V71() V72() V73() Element of K19(REAL)
r is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom r is V71() V72() V73() Element of K19(REAL)
(dom r) /\ (dom f) is V71() V72() V73() Element of K19(REAL)
s is V30() real ext-real Element of REAL
x0 - s is V30() real ext-real Element of REAL
].(x0 - s),x0.[ is V71() V72() V73() Element of K19(REAL)
(dom r) /\ ].(x0 - s),x0.[ is V71() V72() V73() Element of K19(REAL)
(dom f) /\ ].(x0 - s),x0.[ is V71() V72() V73() Element of K19(REAL)
k is V30() real ext-real Element of REAL
x0 is V30() real ext-real Element of REAL
f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom f is V71() V72() V73() Element of K19(REAL)
r is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom r is V71() V72() V73() Element of K19(REAL)
(dom r) /\ (dom f) is V71() V72() V73() Element of K19(REAL)
s is V30() real ext-real Element of REAL
x0 - s is V30() real ext-real Element of REAL
].(x0 - s),x0.[ is V71() V72() V73() Element of K19(REAL)
(dom r) /\ ].(x0 - s),x0.[ is V71() V72() V73() Element of K19(REAL)
(dom f) /\ ].(x0 - s),x0.[ is V71() V72() V73() Element of K19(REAL)
k is V30() real ext-real Element of REAL
x0 is V30() real ext-real Element of REAL
f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom f is V71() V72() V73() Element of K19(REAL)
r is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom r is V71() V72() V73() Element of K19(REAL)
(dom r) /\ (dom f) is V71() V72() V73() Element of K19(REAL)
s is V30() real ext-real Element of REAL
x0 + s is V30() real ext-real Element of REAL
].x0,(x0 + s).[ is V71() V72() V73() Element of K19(REAL)
(dom r) /\ ].x0,(x0 + s).[ is V71() V72() V73() Element of K19(REAL)
(dom f) /\ ].x0,(x0 + s).[ is V71() V72() V73() Element of K19(REAL)
k is V30() real ext-real Element of REAL
x0 is V30() real ext-real Element of REAL
f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom f is V71() V72() V73() Element of K19(REAL)
r is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom r is V71() V72() V73() Element of K19(REAL)
(dom r) /\ (dom f) is V71() V72() V73() Element of K19(REAL)
s is V30() real ext-real Element of REAL
x0 + s is V30() real ext-real Element of REAL
].x0,(x0 + s).[ is V71() V72() V73() Element of K19(REAL)
(dom r) /\ ].x0,(x0 + s).[ is V71() V72() V73() Element of K19(REAL)
(dom f) /\ ].x0,(x0 + s).[ is V71() V72() V73() Element of K19(REAL)
k is V30() real ext-real Element of REAL
x0 is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
f is V30() real ext-real Element of REAL
dom x0 is V71() V72() V73() Element of K19(REAL)
left_open_halfline f is V71() V72() V73() Element of K19(REAL)
K213(-infty,f) is set
(dom x0) /\ (left_open_halfline f) is V71() V72() V73() Element of K19(REAL)
r is V30() real ext-real Element of REAL
s is V30() real ext-real Element of REAL
k is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
k + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
1 / (k + 1) is V30() real ext-real non negative Element of REAL
f - (1 / (k + 1)) is V30() real ext-real Element of REAL
n is V30() real ext-real Element of REAL
g2 is V30() real ext-real Element of REAL
k is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
rng k is V71() V72() V73() Element of K19(REAL)
lim k is V30() real ext-real Element of REAL
x0 /* k is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim (x0 /* k) is V30() real ext-real Element of REAL
x0 is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
f is V30() real ext-real Element of REAL
dom x0 is V71() V72() V73() Element of K19(REAL)
right_open_halfline f is V71() V72() V73() Element of K19(REAL)
K213(f,+infty) is set
(dom x0) /\ (right_open_halfline f) is V71() V72() V73() Element of K19(REAL)
r is V30() real ext-real Element of REAL
s is V30() real ext-real Element of REAL
k is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
k + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
1 / (k + 1) is V30() real ext-real non negative Element of REAL
f + (1 / (k + 1)) is V30() real ext-real Element of REAL
n is V30() real ext-real Element of REAL
g2 is V30() real ext-real Element of REAL
k is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
rng k is V71() V72() V73() Element of K19(REAL)
lim k is V30() real ext-real Element of REAL
x0 /* k is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim (x0 /* k) is V30() real ext-real Element of REAL
x0 is V30() real ext-real Element of REAL
f is V30() real ext-real Element of REAL
r is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
(r,x0) is V30() real ext-real Element of REAL
dom r is V71() V72() V73() Element of K19(REAL)
s is V30() real ext-real Element of REAL
s is V30() real ext-real Element of REAL
k is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
k + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
1 / (k + 1) is V30() real ext-real non negative Element of REAL
x0 - (1 / (k + 1)) is V30() real ext-real Element of REAL
n is V30() real ext-real Element of REAL
r . n is V30() real ext-real Element of REAL
(r . n) - f is V30() real ext-real Element of REAL
abs ((r . n) - f) is V30() real ext-real Element of REAL
g2 is V30() real ext-real Element of REAL
r . g2 is V30() real ext-real Element of REAL
(r . g2) - f is V30() real ext-real Element of REAL
abs ((r . g2) - f) is V30() real ext-real Element of REAL
k is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
rng k is V71() V72() V73() Element of K19(REAL)
left_open_halfline x0 is V71() V72() V73() Element of K19(REAL)
K213(-infty,x0) is set
(dom r) /\ (left_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
lim k is V30() real ext-real Element of REAL
r /* k is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim (r /* k) is V30() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
(r /* k) . n is V30() real ext-real Element of REAL
((r /* k) . n) - f is V30() real ext-real Element of REAL
abs (((r /* k) . n) - f) is V30() real ext-real Element of REAL
k . n is V30() real ext-real Element of REAL
r . (k . n) is V30() real ext-real Element of REAL
(r . (k . n)) - f is V30() real ext-real Element of REAL
abs ((r . (k . n)) - f) is V30() real ext-real Element of REAL
s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim s is V30() real ext-real Element of REAL
rng s is V71() V72() V73() Element of K19(REAL)
left_open_halfline x0 is V71() V72() V73() Element of K19(REAL)
K213(-infty,x0) is set
(dom r) /\ (left_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
k is V30() real ext-real set
n is V30() real ext-real Element of REAL
g2 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
g is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
s . g is V30() real ext-real Element of REAL
{ b₁ where b₁ is V30() real ext-real Element of REAL : not x0 <= b₁ } is set
r . (s . g) is V30() real ext-real Element of REAL
(r . (s . g)) - f is V30() real ext-real Element of REAL
abs ((r . (s . g)) - f) is V30() real ext-real Element of REAL
n is V30() real ext-real Element of REAL
r /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(r /* s) . g is V30() real ext-real Element of REAL
((r /* s) . g) - f is V30() real ext-real Element of REAL
abs (((r /* s) . g) - f) is V30() real ext-real Element of REAL
lim (r /* s) is V30() real ext-real Element of REAL
x0 is V30() real ext-real Element of REAL
f is V30() real ext-real Element of REAL
r is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
(r,x0) is V30() real ext-real Element of REAL
dom r is V71() V72() V73() Element of K19(REAL)
s is V30() real ext-real Element of REAL
s is V30() real ext-real Element of REAL
k is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
k + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
1 / (k + 1) is V30() real ext-real non negative Element of REAL
x0 + (1 / (k + 1)) is V30() real ext-real Element of REAL
n is V30() real ext-real Element of REAL
r . n is V30() real ext-real Element of REAL
(r . n) - f is V30() real ext-real Element of REAL
abs ((r . n) - f) is V30() real ext-real Element of REAL
g2 is V30() real ext-real Element of REAL
r . g2 is V30() real ext-real Element of REAL
(r . g2) - f is V30() real ext-real Element of REAL
abs ((r . g2) - f) is V30() real ext-real Element of REAL
k is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
rng k is V71() V72() V73() Element of K19(REAL)
right_open_halfline x0 is V71() V72() V73() Element of K19(REAL)
K213(x0,+infty) is set
(dom r) /\ (right_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
lim k is V30() real ext-real Element of REAL
r /* k is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim (r /* k) is V30() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
(r /* k) . n is V30() real ext-real Element of REAL
((r /* k) . n) - f is V30() real ext-real Element of REAL
abs (((r /* k) . n) - f) is V30() real ext-real Element of REAL
k . n is V30() real ext-real Element of REAL
r . (k . n) is V30() real ext-real Element of REAL
(r . (k . n)) - f is V30() real ext-real Element of REAL
abs ((r . (k . n)) - f) is V30() real ext-real Element of REAL
s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim s is V30() real ext-real Element of REAL
rng s is V71() V72() V73() Element of K19(REAL)
right_open_halfline x0 is V71() V72() V73() Element of K19(REAL)
K213(x0,+infty) is set
(dom r) /\ (right_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
k is V30() real ext-real set
n is V30() real ext-real Element of REAL
g2 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
g is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
s . g is V30() real ext-real Element of REAL
{ b₁ where b₁ is V30() real ext-real Element of REAL : not b₁ <= x0 } is set
r . (s . g) is V30() real ext-real Element of REAL
(r . (s . g)) - f is V30() real ext-real Element of REAL
abs ((r . (s . g)) - f) is V30() real ext-real Element of REAL
n is V30() real ext-real Element of REAL
r /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(r /* s) . g is V30() real ext-real Element of REAL
((r /* s) . g) - f is V30() real ext-real Element of REAL
abs (((r /* s) . g) - f) is V30() real ext-real Element of REAL
lim (r /* s) is V30() real ext-real Element of REAL
x0 is V30() real ext-real Element of REAL
f is V30() real ext-real Element of REAL
r is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
f (#) r is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
((f (#) r),x0) is V30() real ext-real Element of REAL
(r,x0) is V30() real ext-real Element of REAL
f * (r,x0) is V30() real ext-real Element of REAL
s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim s is V30() real ext-real Element of REAL
rng s is V71() V72() V73() Element of K19(REAL)
dom (f (#) r) is V71() V72() V73() Element of K19(REAL)
left_open_halfline x0 is V71() V72() V73() Element of K19(REAL)
K213(-infty,x0) is set
(dom (f (#) r)) /\ (left_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
dom r is V71() V72() V73() Element of K19(REAL)
(dom r) /\ (left_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
r /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
f (#) (r /* s) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f (#) r) /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim (r /* s) is V30() real ext-real Element of REAL
lim ((f (#) r) /* s) is V30() real ext-real Element of REAL
s is V30() real ext-real Element of REAL
k is V30() real ext-real Element of REAL
n is V30() real ext-real Element of REAL
x0 is V30() real ext-real Element of REAL
f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
- f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
- 1 is V30() real ext-real non positive set
(- 1) (#) f is V1() V4( REAL ) V6() complex-valued ext-real-valued real-valued set
((- f),x0) is V30() real ext-real Element of REAL
(f,x0) is V30() real ext-real Element of REAL
- (f,x0) is V30() real ext-real Element of REAL
- 1 is V30() real ext-real non positive Element of REAL
(- 1) (#) f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
(- 1) * (f,x0) is V30() real ext-real Element of REAL
x0 is V30() real ext-real Element of REAL
f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
(f,x0) is V30() real ext-real Element of REAL
r is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
f + r is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom (f + r) is V71() V72() V73() Element of K19(REAL)
((f + r),x0) is V30() real ext-real Element of REAL
(r,x0) is V30() real ext-real Element of REAL
(f,x0) + (r,x0) is V30() real ext-real Element of REAL
s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim s is V30() real ext-real Element of REAL
rng s is V71() V72() V73() Element of K19(REAL)
left_open_halfline x0 is V71() V72() V73() Element of K19(REAL)
K213(-infty,x0) is set
(dom (f + r)) /\ (left_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
dom f is V71() V72() V73() Element of K19(REAL)
dom r is V71() V72() V73() Element of K19(REAL)
(dom f) /\ (dom r) is V71() V72() V73() Element of K19(REAL)
(dom f) /\ (left_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
(dom r) /\ (left_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
r /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim (r /* s) is V30() real ext-real Element of REAL
f /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f /* s) + (r /* s) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f + r) /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim (f /* s) is V30() real ext-real Element of REAL
lim ((f + r) /* s) is V30() real ext-real Element of REAL
x0 is V30() real ext-real Element of REAL
f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
(f,x0) is V30() real ext-real Element of REAL
r is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
f - r is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
- r is V1() V4( REAL ) V6() complex-valued ext-real-valued real-valued set
- 1 is V30() real ext-real non positive set
(- 1) (#) r is V1() V4( REAL ) V6() complex-valued ext-real-valued real-valued set
f + (- r) is V1() V4( REAL ) V6() complex-valued ext-real-valued real-valued set
dom (f - r) is V71() V72() V73() Element of K19(REAL)
((f - r),x0) is V30() real ext-real Element of REAL
(r,x0) is V30() real ext-real Element of REAL
(f,x0) - (r,x0) is V30() real ext-real Element of REAL
- r is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
((- r),x0) is V30() real ext-real Element of REAL
(f,x0) + ((- r),x0) is V30() real ext-real Element of REAL
- (r,x0) is V30() real ext-real Element of REAL
(f,x0) + (- (r,x0)) is V30() real ext-real Element of REAL
x0 is V30() real ext-real Element of REAL
f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
f " {0} is V71() V72() V73() Element of K19(REAL)
(f,x0) is V30() real ext-real Element of REAL
f ^ is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
((f ^),x0) is V30() real ext-real Element of REAL
(f,x0) " is V30() real ext-real Element of REAL
dom f is V71() V72() V73() Element of K19(REAL)
(dom f) \ (f " {0}) is V71() V72() V73() Element of K19(REAL)
dom (f ^) is V71() V72() V73() Element of K19(REAL)
r is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim r is V30() real ext-real Element of REAL
rng r is V71() V72() V73() Element of K19(REAL)
left_open_halfline x0 is V71() V72() V73() Element of K19(REAL)
K213(-infty,x0) is set
(dom (f ^)) /\ (left_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
f /* r is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim (f /* r) is V30() real ext-real Element of REAL
(dom f) /\ (left_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
(f /* r) " is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f ^) /* r is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim ((f ^) /* r) is V30() real ext-real Element of REAL
r is V30() real ext-real Element of REAL
x0 is V30() real ext-real Element of REAL
f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
abs f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
((abs f),x0) is V30() real ext-real Element of REAL
(f,x0) is V30() real ext-real Element of REAL
abs (f,x0) is V30() real ext-real Element of REAL
r is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim r is V30() real ext-real Element of REAL
rng r is V71() V72() V73() Element of K19(REAL)
dom (abs f) is V71() V72() V73() Element of K19(REAL)
left_open_halfline x0 is V71() V72() V73() Element of K19(REAL)
K213(-infty,x0) is set
(dom (abs f)) /\ (left_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
dom f is V71() V72() V73() Element of K19(REAL)
(dom f) /\ (left_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
f /* r is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
abs (f /* r) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(abs f) /* r is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim (f /* r) is V30() real ext-real Element of REAL
lim ((abs f) /* r) is V30() real ext-real Element of REAL
r is V30() real ext-real Element of REAL
s is V30() real ext-real Element of REAL
k is V30() real ext-real Element of REAL
x0 is V30() real ext-real Element of REAL
f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
(f,x0) is V30() real ext-real Element of REAL
dom f is V71() V72() V73() Element of K19(REAL)
f ^ is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
((f ^),x0) is V30() real ext-real Element of REAL
(f,x0) " is V30() real ext-real Element of REAL
f " {0} is V71() V72() V73() Element of K19(REAL)
(dom f) \ (f " {0}) is V71() V72() V73() Element of K19(REAL)
dom (f ^) is V71() V72() V73() Element of K19(REAL)
r is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim r is V30() real ext-real Element of REAL
rng r is V71() V72() V73() Element of K19(REAL)
left_open_halfline x0 is V71() V72() V73() Element of K19(REAL)
K213(-infty,x0) is set
(dom (f ^)) /\ (left_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
f /* r is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(dom f) /\ (left_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
lim (f /* r) is V30() real ext-real Element of REAL
(f /* r) " is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f ^) /* r is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim ((f ^) /* r) is V30() real ext-real Element of REAL
r is V30() real ext-real Element of REAL
s is V30() real ext-real Element of REAL
f . s is V30() real ext-real Element of REAL
k is V30() real ext-real Element of REAL
f . k is V30() real ext-real Element of REAL
x0 is V30() real ext-real Element of REAL
f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
(f,x0) is V30() real ext-real Element of REAL
r is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
f (#) r is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom (f (#) r) is V71() V72() V73() Element of K19(REAL)
((f (#) r),x0) is V30() real ext-real Element of REAL
(r,x0) is V30() real ext-real Element of REAL
(f,x0) * (r,x0) is V30() real ext-real Element of REAL
s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim s is V30() real ext-real Element of REAL
rng s is V71() V72() V73() Element of K19(REAL)
left_open_halfline x0 is V71() V72() V73() Element of K19(REAL)
K213(-infty,x0) is set
(dom (f (#) r)) /\ (left_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
dom f is V71() V72() V73() Element of K19(REAL)
dom r is V71() V72() V73() Element of K19(REAL)
(dom f) /\ (dom r) is V71() V72() V73() Element of K19(REAL)
(dom f) /\ (left_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
(dom r) /\ (left_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
r /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim (r /* s) is V30() real ext-real Element of REAL
f /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f /* s) (#) (r /* s) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f (#) r) /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim (f /* s) is V30() real ext-real Element of REAL
lim ((f (#) r) /* s) is V30() real ext-real Element of REAL
x0 is V30() real ext-real Element of REAL
f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
(f,x0) is V30() real ext-real Element of REAL
r is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
(r,x0) is V30() real ext-real Element of REAL
f / r is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom (f / r) is V71() V72() V73() Element of K19(REAL)
((f / r),x0) is V30() real ext-real Element of REAL
(f,x0) / (r,x0) is V30() real ext-real Element of REAL
s is V30() real ext-real Element of REAL
k is V30() real ext-real Element of REAL
n is V30() real ext-real Element of REAL
dom f is V71() V72() V73() Element of K19(REAL)
dom r is V71() V72() V73() Element of K19(REAL)
r " {0} is V71() V72() V73() Element of K19(REAL)
(dom r) \ (r " {0}) is V71() V72() V73() Element of K19(REAL)
(dom f) /\ ((dom r) \ (r " {0})) is V71() V72() V73() Element of K19(REAL)
r . n is V30() real ext-real Element of REAL
r ^ is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
f (#) (r ^) is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
((r ^),x0) is V30() real ext-real Element of REAL
(r,x0) " is V30() real ext-real Element of REAL
(f,x0) * ((r,x0) ") is V30() real ext-real Element of REAL
x0 is V30() real ext-real Element of REAL
f is V30() real ext-real Element of REAL
r is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
f (#) r is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
((f (#) r),x0) is V30() real ext-real Element of REAL
(r,x0) is V30() real ext-real Element of REAL
f * (r,x0) is V30() real ext-real Element of REAL
s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim s is V30() real ext-real Element of REAL
rng s is V71() V72() V73() Element of K19(REAL)
dom (f (#) r) is V71() V72() V73() Element of K19(REAL)
right_open_halfline x0 is V71() V72() V73() Element of K19(REAL)
K213(x0,+infty) is set
(dom (f (#) r)) /\ (right_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
dom r is V71() V72() V73() Element of K19(REAL)
(dom r) /\ (right_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
r /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
f (#) (r /* s) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f (#) r) /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim (r /* s) is V30() real ext-real Element of REAL
lim ((f (#) r) /* s) is V30() real ext-real Element of REAL
s is V30() real ext-real Element of REAL
k is V30() real ext-real Element of REAL
n is V30() real ext-real Element of REAL
x0 is V30() real ext-real Element of REAL
f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
- f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
- 1 is V30() real ext-real non positive set
(- 1) (#) f is V1() V4( REAL ) V6() complex-valued ext-real-valued real-valued set
((- f),x0) is V30() real ext-real Element of REAL
(f,x0) is V30() real ext-real Element of REAL
- (f,x0) is V30() real ext-real Element of REAL
- 1 is V30() real ext-real non positive Element of REAL
(- 1) (#) f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
(- 1) * (f,x0) is V30() real ext-real Element of REAL
x0 is V30() real ext-real Element of REAL
f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
(f,x0) is V30() real ext-real Element of REAL
r is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
f + r is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom (f + r) is V71() V72() V73() Element of K19(REAL)
((f + r),x0) is V30() real ext-real Element of REAL
(r,x0) is V30() real ext-real Element of REAL
(f,x0) + (r,x0) is V30() real ext-real Element of REAL
s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim s is V30() real ext-real Element of REAL
rng s is V71() V72() V73() Element of K19(REAL)
right_open_halfline x0 is V71() V72() V73() Element of K19(REAL)
K213(x0,+infty) is set
(dom (f + r)) /\ (right_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
dom f is V71() V72() V73() Element of K19(REAL)
dom r is V71() V72() V73() Element of K19(REAL)
(dom f) /\ (dom r) is V71() V72() V73() Element of K19(REAL)
(dom f) /\ (right_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
(dom r) /\ (right_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
r /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim (r /* s) is V30() real ext-real Element of REAL
f /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f /* s) + (r /* s) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f + r) /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim (f /* s) is V30() real ext-real Element of REAL
lim ((f + r) /* s) is V30() real ext-real Element of REAL
x0 is V30() real ext-real Element of REAL
f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
(f,x0) is V30() real ext-real Element of REAL
r is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
f - r is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
- r is V1() V4( REAL ) V6() complex-valued ext-real-valued real-valued set
- 1 is V30() real ext-real non positive set
(- 1) (#) r is V1() V4( REAL ) V6() complex-valued ext-real-valued real-valued set
f + (- r) is V1() V4( REAL ) V6() complex-valued ext-real-valued real-valued set
dom (f - r) is V71() V72() V73() Element of K19(REAL)
((f - r),x0) is V30() real ext-real Element of REAL
(r,x0) is V30() real ext-real Element of REAL
(f,x0) - (r,x0) is V30() real ext-real Element of REAL
- r is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
((- r),x0) is V30() real ext-real Element of REAL
(f,x0) + ((- r),x0) is V30() real ext-real Element of REAL
- (r,x0) is V30() real ext-real Element of REAL
(f,x0) + (- (r,x0)) is V30() real ext-real Element of REAL
x0 is V30() real ext-real Element of REAL
f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
f " {0} is V71() V72() V73() Element of K19(REAL)
(f,x0) is V30() real ext-real Element of REAL
f ^ is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
((f ^),x0) is V30() real ext-real Element of REAL
(f,x0) " is V30() real ext-real Element of REAL
dom f is V71() V72() V73() Element of K19(REAL)
(dom f) \ (f " {0}) is V71() V72() V73() Element of K19(REAL)
dom (f ^) is V71() V72() V73() Element of K19(REAL)
r is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim r is V30() real ext-real Element of REAL
rng r is V71() V72() V73() Element of K19(REAL)
right_open_halfline x0 is V71() V72() V73() Element of K19(REAL)
K213(x0,+infty) is set
(dom (f ^)) /\ (right_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
f /* r is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim (f /* r) is V30() real ext-real Element of REAL
(dom f) /\ (right_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
(f /* r) " is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f ^) /* r is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim ((f ^) /* r) is V30() real ext-real Element of REAL
r is V30() real ext-real Element of REAL
x0 is V30() real ext-real Element of REAL
f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
abs f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
((abs f),x0) is V30() real ext-real Element of REAL
(f,x0) is V30() real ext-real Element of REAL
abs (f,x0) is V30() real ext-real Element of REAL
r is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim r is V30() real ext-real Element of REAL
rng r is V71() V72() V73() Element of K19(REAL)
dom (abs f) is V71() V72() V73() Element of K19(REAL)
right_open_halfline x0 is V71() V72() V73() Element of K19(REAL)
K213(x0,+infty) is set
(dom (abs f)) /\ (right_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
dom f is V71() V72() V73() Element of K19(REAL)
(dom f) /\ (right_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
f /* r is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
abs (f /* r) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(abs f) /* r is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim (f /* r) is V30() real ext-real Element of REAL
lim ((abs f) /* r) is V30() real ext-real Element of REAL
r is V30() real ext-real Element of REAL
s is V30() real ext-real Element of REAL
k is V30() real ext-real Element of REAL
x0 is V30() real ext-real Element of REAL
f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
(f,x0) is V30() real ext-real Element of REAL
dom f is V71() V72() V73() Element of K19(REAL)
f ^ is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
((f ^),x0) is V30() real ext-real Element of REAL
(f,x0) " is V30() real ext-real Element of REAL
f " {0} is V71() V72() V73() Element of K19(REAL)
(dom f) \ (f " {0}) is V71() V72() V73() Element of K19(REAL)
dom (f ^) is V71() V72() V73() Element of K19(REAL)
r is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim r is V30() real ext-real Element of REAL
rng r is V71() V72() V73() Element of K19(REAL)
right_open_halfline x0 is V71() V72() V73() Element of K19(REAL)
K213(x0,+infty) is set
(dom (f ^)) /\ (right_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
f /* r is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(dom f) /\ (right_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
lim (f /* r) is V30() real ext-real Element of REAL
(f /* r) " is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f ^) /* r is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim ((f ^) /* r) is V30() real ext-real Element of REAL
r is V30() real ext-real Element of REAL
s is V30() real ext-real Element of REAL
f . s is V30() real ext-real Element of REAL
k is V30() real ext-real Element of REAL
f . k is V30() real ext-real Element of REAL
x0 is V30() real ext-real Element of REAL
f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
(f,x0) is V30() real ext-real Element of REAL
r is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
f (#) r is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom (f (#) r) is V71() V72() V73() Element of K19(REAL)
((f (#) r),x0) is V30() real ext-real Element of REAL
(r,x0) is V30() real ext-real Element of REAL
(f,x0) * (r,x0) is V30() real ext-real Element of REAL
s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim s is V30() real ext-real Element of REAL
rng s is V71() V72() V73() Element of K19(REAL)
right_open_halfline x0 is V71() V72() V73() Element of K19(REAL)
K213(x0,+infty) is set
(dom (f (#) r)) /\ (right_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
dom f is V71() V72() V73() Element of K19(REAL)
dom r is V71() V72() V73() Element of K19(REAL)
(dom f) /\ (dom r) is V71() V72() V73() Element of K19(REAL)
(dom f) /\ (right_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
(dom r) /\ (right_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
r /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim (r /* s) is V30() real ext-real Element of REAL
f /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f /* s) (#) (r /* s) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f (#) r) /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim (f /* s) is V30() real ext-real Element of REAL
lim ((f (#) r) /* s) is V30() real ext-real Element of REAL
x0 is V30() real ext-real Element of REAL
f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
(f,x0) is V30() real ext-real Element of REAL
r is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
(r,x0) is V30() real ext-real Element of REAL
f / r is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom (f / r) is V71() V72() V73() Element of K19(REAL)
((f / r),x0) is V30() real ext-real Element of REAL
(f,x0) / (r,x0) is V30() real ext-real Element of REAL
s is V30() real ext-real Element of REAL
k is V30() real ext-real Element of REAL
n is V30() real ext-real Element of REAL
dom f is V71() V72() V73() Element of K19(REAL)
dom r is V71() V72() V73() Element of K19(REAL)
r " {0} is V71() V72() V73() Element of K19(REAL)
(dom r) \ (r " {0}) is V71() V72() V73() Element of K19(REAL)
(dom f) /\ ((dom r) \ (r " {0})) is V71() V72() V73() Element of K19(REAL)
r . n is V30() real ext-real Element of REAL
r ^ is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
f (#) (r ^) is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
((r ^),x0) is V30() real ext-real Element of REAL
(r,x0) " is V30() real ext-real Element of REAL
(f,x0) * ((r,x0) ") is V30() real ext-real Element of REAL
x0 is V30() real ext-real Element of REAL
f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
(f,x0) is V30() real ext-real Element of REAL
r is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
f (#) r is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom (f (#) r) is V71() V72() V73() Element of K19(REAL)
((f (#) r),x0) is V30() real ext-real Element of REAL
s is V30() real ext-real Element of REAL
x0 - s is V30() real ext-real Element of REAL
].(x0 - s),x0.[ is V71() V72() V73() Element of K19(REAL)
r | ].(x0 - s),x0.[ is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom r is V71() V72() V73() Element of K19(REAL)
].(x0 - s),x0.[ /\ (dom r) is V71() V72() V73() Element of K19(REAL)
k is V30() real ext-real set
left_open_halfline x0 is V71() V72() V73() Element of K19(REAL)
K213(-infty,x0) is set
g2 is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim g2 is V30() real ext-real Element of REAL
rng g2 is V71() V72() V73() Element of K19(REAL)
(dom (f (#) r)) /\ (left_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
g2 ^\ n is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of g2
rng (g2 ^\ n) is V71() V72() V73() Element of K19(REAL)
dom f is V71() V72() V73() Element of K19(REAL)
(dom f) /\ (dom r) is V71() V72() V73() Element of K19(REAL)
f /* (g2 ^\ n) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
r /* (g2 ^\ n) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f /* (g2 ^\ n)) (#) (r /* (g2 ^\ n)) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f (#) r) /* (g2 ^\ n) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f (#) r) /* g2 is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
((f (#) r) /* g2) ^\ n is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of (f (#) r) /* g2
(dom f) /\ (left_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
lim (g2 ^\ n) is V30() real ext-real Element of REAL
abs k is V30() real ext-real Element of REAL
(abs k) + 1 is V30() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
n + n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
g2 . (n + n) is V30() real ext-real Element of REAL
(g2 ^\ n) . n is V30() real ext-real Element of REAL
{ b₁ where b₁ is V30() real ext-real Element of REAL : not x0 <= b₁ } is set
{ b₁ where b₁ is V30() real ext-real Element of REAL : ( not b₁ <= x0 - s & not x0 <= b₁ ) } is set
c₁₁ is V30() real ext-real Element of REAL
r . ((g2 ^\ n) . n) is V30() real ext-real Element of REAL
abs (r . ((g2 ^\ n) . n)) is V30() real ext-real Element of REAL
(r /* (g2 ^\ n)) . n is V30() real ext-real Element of REAL
abs ((r /* (g2 ^\ n)) . n) is V30() real ext-real Element of REAL
lim (f /* (g2 ^\ n)) is V30() real ext-real Element of REAL
lim ((f /* (g2 ^\ n)) (#) (r /* (g2 ^\ n))) is V30() real ext-real Element of REAL
lim ((f (#) r) /* g2) is V30() real ext-real Element of REAL
x0 is V30() real ext-real Element of REAL
f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
(f,x0) is V30() real ext-real Element of REAL
r is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
f (#) r is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom (f (#) r) is V71() V72() V73() Element of K19(REAL)
((f (#) r),x0) is V30() real ext-real Element of REAL
s is V30() real ext-real Element of REAL
x0 + s is V30() real ext-real Element of REAL
].x0,(x0 + s).[ is V71() V72() V73() Element of K19(REAL)
r | ].x0,(x0 + s).[ is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom r is V71() V72() V73() Element of K19(REAL)
].x0,(x0 + s).[ /\ (dom r) is V71() V72() V73() Element of K19(REAL)
k is V30() real ext-real set
right_open_halfline x0 is V71() V72() V73() Element of K19(REAL)
K213(x0,+infty) is set
g2 is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim g2 is V30() real ext-real Element of REAL
rng g2 is V71() V72() V73() Element of K19(REAL)
(dom (f (#) r)) /\ (right_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
g2 ^\ n is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of g2
rng (g2 ^\ n) is V71() V72() V73() Element of K19(REAL)
dom f is V71() V72() V73() Element of K19(REAL)
(dom f) /\ (dom r) is V71() V72() V73() Element of K19(REAL)
f /* (g2 ^\ n) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
r /* (g2 ^\ n) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f /* (g2 ^\ n)) (#) (r /* (g2 ^\ n)) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f (#) r) /* (g2 ^\ n) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f (#) r) /* g2 is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
((f (#) r) /* g2) ^\ n is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of (f (#) r) /* g2
(dom f) /\ (right_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
lim (g2 ^\ n) is V30() real ext-real Element of REAL
abs k is V30() real ext-real Element of REAL
(abs k) + 1 is V30() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
n + n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
g2 . (n + n) is V30() real ext-real Element of REAL
(g2 ^\ n) . n is V30() real ext-real Element of REAL
{ b₁ where b₁ is V30() real ext-real Element of REAL : not b₁ <= x0 } is set
{ b₁ where b₁ is V30() real ext-real Element of REAL : ( not b₁ <= x0 & not x0 + s <= b₁ ) } is set
c₁₁ is V30() real ext-real Element of REAL
r . ((g2 ^\ n) . n) is V30() real ext-real Element of REAL
abs (r . ((g2 ^\ n) . n)) is V30() real ext-real Element of REAL
(r /* (g2 ^\ n)) . n is V30() real ext-real Element of REAL
abs ((r /* (g2 ^\ n)) . n) is V30() real ext-real Element of REAL
lim (f /* (g2 ^\ n)) is V30() real ext-real Element of REAL
lim ((f /* (g2 ^\ n)) (#) (r /* (g2 ^\ n))) is V30() real ext-real Element of REAL
lim ((f (#) r) /* g2) is V30() real ext-real Element of REAL
x0 is V30() real ext-real Element of REAL
f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
(f,x0) is V30() real ext-real Element of REAL
dom f is V71() V72() V73() Element of K19(REAL)
r is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
(r,x0) is V30() real ext-real Element of REAL
dom r is V71() V72() V73() Element of K19(REAL)
s is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom s is V71() V72() V73() Element of K19(REAL)
(s,x0) is V30() real ext-real Element of REAL
k is V30() real ext-real Element of REAL
x0 - k is V30() real ext-real Element of REAL
].(x0 - k),x0.[ is V71() V72() V73() Element of K19(REAL)
(dom s) /\ ].(x0 - k),x0.[ is V71() V72() V73() Element of K19(REAL)
(dom f) /\ ].(x0 - k),x0.[ is V71() V72() V73() Element of K19(REAL)
(dom r) /\ ].(x0 - k),x0.[ is V71() V72() V73() Element of K19(REAL)
n is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim n is V30() real ext-real Element of REAL
rng n is V71() V72() V73() Element of K19(REAL)
left_open_halfline x0 is V71() V72() V73() Element of K19(REAL)
K213(-infty,x0) is set
(dom s) /\ (left_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
g2 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
n ^\ g2 is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of n
rng (n ^\ g2) is V71() V72() V73() Element of K19(REAL)
n is set
g is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
(n ^\ g2) . g is V30() real ext-real Element of REAL
{ b₁ where b₁ is V30() real ext-real Element of REAL : not x0 <= b₁ } is set
g + g2 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
n . (g + g2) is V30() real ext-real Element of REAL
{ b₁ where b₁ is V30() real ext-real Element of REAL : ( not b₁ <= x0 - k & not x0 <= b₁ ) } is set
n is V30() real ext-real Element of REAL
lim (n ^\ g2) is V30() real ext-real Element of REAL
(dom r) /\ (left_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
r /* (n ^\ g2) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim (r /* (n ^\ g2)) is V30() real ext-real Element of REAL
(dom f) /\ (left_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
f /* (n ^\ g2) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim (f /* (n ^\ g2)) is V30() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
(n ^\ g2) . n is V30() real ext-real Element of REAL
s . ((n ^\ g2) . n) is V30() real ext-real Element of REAL
r . ((n ^\ g2) . n) is V30() real ext-real Element of REAL
s /* (n ^\ g2) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(s /* (n ^\ g2)) . n is V30() real ext-real Element of REAL
f . ((n ^\ g2) . n) is V30() real ext-real Element of REAL
(f /* (n ^\ g2)) . n is V30() real ext-real Element of REAL
(r /* (n ^\ g2)) . n is V30() real ext-real Element of REAL
s /* n is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(s /* n) ^\ g2 is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of s /* n
lim (s /* (n ^\ g2)) is V30() real ext-real Element of REAL
lim ((s /* n) ^\ g2) is V30() real ext-real Element of REAL
lim (s /* n) is V30() real ext-real Element of REAL
n is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim n is V30() real ext-real Element of REAL
rng n is V71() V72() V73() Element of K19(REAL)
left_open_halfline x0 is V71() V72() V73() Element of K19(REAL)
K213(-infty,x0) is set
(dom s) /\ (left_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
g2 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
n ^\ g2 is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of n
rng (n ^\ g2) is V71() V72() V73() Element of K19(REAL)
n is set
g is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
(n ^\ g2) . g is V30() real ext-real Element of REAL
{ b₁ where b₁ is V30() real ext-real Element of REAL : not x0 <= b₁ } is set
g + g2 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
n . (g + g2) is V30() real ext-real Element of REAL
{ b₁ where b₁ is V30() real ext-real Element of REAL : ( not b₁ <= x0 - k & not x0 <= b₁ ) } is set
n is V30() real ext-real Element of REAL
lim (n ^\ g2) is V30() real ext-real Element of REAL
(dom r) /\ (left_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
r /* (n ^\ g2) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim (r /* (n ^\ g2)) is V30() real ext-real Element of REAL
(dom f) /\ (left_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
f /* (n ^\ g2) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim (f /* (n ^\ g2)) is V30() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
(n ^\ g2) . n is V30() real ext-real Element of REAL
s . ((n ^\ g2) . n) is V30() real ext-real Element of REAL
r . ((n ^\ g2) . n) is V30() real ext-real Element of REAL
s /* (n ^\ g2) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(s /* (n ^\ g2)) . n is V30() real ext-real Element of REAL
f . ((n ^\ g2) . n) is V30() real ext-real Element of REAL
(f /* (n ^\ g2)) . n is V30() real ext-real Element of REAL
(r /* (n ^\ g2)) . n is V30() real ext-real Element of REAL
s /* n is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(s /* n) ^\ g2 is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of s /* n
lim (s /* (n ^\ g2)) is V30() real ext-real Element of REAL
lim ((s /* n) ^\ g2) is V30() real ext-real Element of REAL
lim (s /* n) is V30() real ext-real Element of REAL
x0 is V30() real ext-real Element of REAL
f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
(f,x0) is V30() real ext-real Element of REAL
dom f is V71() V72() V73() Element of K19(REAL)
r is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
(r,x0) is V30() real ext-real Element of REAL
dom r is V71() V72() V73() Element of K19(REAL)
(dom f) /\ (dom r) is V71() V72() V73() Element of K19(REAL)
s is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom s is V71() V72() V73() Element of K19(REAL)
((dom f) /\ (dom r)) /\ (dom s) is V71() V72() V73() Element of K19(REAL)
(s,x0) is V30() real ext-real Element of REAL
k is V30() real ext-real Element of REAL
x0 - k is V30() real ext-real Element of REAL
].(x0 - k),x0.[ is V71() V72() V73() Element of K19(REAL)
n is V30() real ext-real Element of REAL
g2 is V30() real ext-real set
n is V30() real ext-real Element of REAL
g is V30() real ext-real Element of REAL
{ b₁ where b₁ is V30() real ext-real Element of REAL : ( not b₁ <= x0 - k & not x0 <= b₁ ) } is set
g2 is V30() real ext-real Element of REAL
g2 is V30() real ext-real set
n is V30() real ext-real Element of REAL
g is V30() real ext-real Element of REAL
{ b₁ where b₁ is V30() real ext-real Element of REAL : ( not b₁ <= x0 - k & not x0 <= b₁ ) } is set
g2 is V30() real ext-real Element of REAL
g2 is V30() real ext-real Element of REAL
(dom r) /\ ].(x0 - k),x0.[ is V71() V72() V73() Element of K19(REAL)
(dom f) /\ ].(x0 - k),x0.[ is V71() V72() V73() Element of K19(REAL)
(dom s) /\ ].(x0 - k),x0.[ is V71() V72() V73() Element of K19(REAL)
x0 is V30() real ext-real Element of REAL
f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
(f,x0) is V30() real ext-real Element of REAL
dom f is V71() V72() V73() Element of K19(REAL)
r is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
(r,x0) is V30() real ext-real Element of REAL
dom r is V71() V72() V73() Element of K19(REAL)
s is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom s is V71() V72() V73() Element of K19(REAL)
(s,x0) is V30() real ext-real Element of REAL
k is V30() real ext-real Element of REAL
x0 + k is V30() real ext-real Element of REAL
].x0,(x0 + k).[ is V71() V72() V73() Element of K19(REAL)
(dom s) /\ ].x0,(x0 + k).[ is V71() V72() V73() Element of K19(REAL)
(dom f) /\ ].x0,(x0 + k).[ is V71() V72() V73() Element of K19(REAL)
(dom r) /\ ].x0,(x0 + k).[ is V71() V72() V73() Element of K19(REAL)
n is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim n is V30() real ext-real Element of REAL
rng n is V71() V72() V73() Element of K19(REAL)
right_open_halfline x0 is V71() V72() V73() Element of K19(REAL)
K213(x0,+infty) is set
(dom s) /\ (right_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
(lim n) + k is V30() real ext-real Element of REAL
g2 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
n ^\ g2 is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of n
rng (n ^\ g2) is V71() V72() V73() Element of K19(REAL)
n is set
g is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
(n ^\ g2) . g is V30() real ext-real Element of REAL
{ b₁ where b₁ is V30() real ext-real Element of REAL : not b₁ <= x0 } is set
g + g2 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
n . (g + g2) is V30() real ext-real Element of REAL
{ b₁ where b₁ is V30() real ext-real Element of REAL : ( not b₁ <= x0 & not x0 + k <= b₁ ) } is set
n is V30() real ext-real Element of REAL
lim (n ^\ g2) is V30() real ext-real Element of REAL
(dom r) /\ (right_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
r /* (n ^\ g2) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim (r /* (n ^\ g2)) is V30() real ext-real Element of REAL
(dom f) /\ (right_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
f /* (n ^\ g2) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim (f /* (n ^\ g2)) is V30() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
(n ^\ g2) . n is V30() real ext-real Element of REAL
s . ((n ^\ g2) . n) is V30() real ext-real Element of REAL
r . ((n ^\ g2) . n) is V30() real ext-real Element of REAL
s /* (n ^\ g2) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(s /* (n ^\ g2)) . n is V30() real ext-real Element of REAL
f . ((n ^\ g2) . n) is V30() real ext-real Element of REAL
(f /* (n ^\ g2)) . n is V30() real ext-real Element of REAL
(r /* (n ^\ g2)) . n is V30() real ext-real Element of REAL
s /* n is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(s /* n) ^\ g2 is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of s /* n
lim (s /* (n ^\ g2)) is V30() real ext-real Element of REAL
lim ((s /* n) ^\ g2) is V30() real ext-real Element of REAL
lim (s /* n) is V30() real ext-real Element of REAL
n is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim n is V30() real ext-real Element of REAL
rng n is V71() V72() V73() Element of K19(REAL)
right_open_halfline x0 is V71() V72() V73() Element of K19(REAL)
K213(x0,+infty) is set
(dom s) /\ (right_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
(lim n) + k is V30() real ext-real Element of REAL
g2 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
n ^\ g2 is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of n
rng (n ^\ g2) is V71() V72() V73() Element of K19(REAL)
n is set
g is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
(n ^\ g2) . g is V30() real ext-real Element of REAL
{ b₁ where b₁ is V30() real ext-real Element of REAL : not b₁ <= x0 } is set
g + g2 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
n . (g + g2) is V30() real ext-real Element of REAL
{ b₁ where b₁ is V30() real ext-real Element of REAL : ( not b₁ <= x0 & not x0 + k <= b₁ ) } is set
n is V30() real ext-real Element of REAL
lim (n ^\ g2) is V30() real ext-real Element of REAL
(dom r) /\ (right_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
r /* (n ^\ g2) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim (r /* (n ^\ g2)) is V30() real ext-real Element of REAL
(dom f) /\ (right_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
f /* (n ^\ g2) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim (f /* (n ^\ g2)) is V30() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
(n ^\ g2) . n is V30() real ext-real Element of REAL
s . ((n ^\ g2) . n) is V30() real ext-real Element of REAL
r . ((n ^\ g2) . n) is V30() real ext-real Element of REAL
s /* (n ^\ g2) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(s /* (n ^\ g2)) . n is V30() real ext-real Element of REAL
f . ((n ^\ g2) . n) is V30() real ext-real Element of REAL
(f /* (n ^\ g2)) . n is V30() real ext-real Element of REAL
(r /* (n ^\ g2)) . n is V30() real ext-real Element of REAL
s /* n is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(s /* n) ^\ g2 is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of s /* n
lim (s /* (n ^\ g2)) is V30() real ext-real Element of REAL
lim ((s /* n) ^\ g2) is V30() real ext-real Element of REAL
lim (s /* n) is V30() real ext-real Element of REAL
x0 is V30() real ext-real Element of REAL
f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
(f,x0) is V30() real ext-real Element of REAL
dom f is V71() V72() V73() Element of K19(REAL)
r is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
(r,x0) is V30() real ext-real Element of REAL
dom r is V71() V72() V73() Element of K19(REAL)
(dom f) /\ (dom r) is V71() V72() V73() Element of K19(REAL)
s is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom s is V71() V72() V73() Element of K19(REAL)
((dom f) /\ (dom r)) /\ (dom s) is V71() V72() V73() Element of K19(REAL)
(s,x0) is V30() real ext-real Element of REAL
k is V30() real ext-real Element of REAL
x0 + k is V30() real ext-real Element of REAL
].x0,(x0 + k).[ is V71() V72() V73() Element of K19(REAL)
n is V30() real ext-real Element of REAL
g2 is V30() real ext-real set
n is V30() real ext-real Element of REAL
g is V30() real ext-real Element of REAL
{ b₁ where b₁ is V30() real ext-real Element of REAL : ( not b₁ <= x0 & not x0 + k <= b₁ ) } is set
g2 is V30() real ext-real Element of REAL
x0 + 0 is V30() real ext-real Element of REAL
g2 is V30() real ext-real set
n is V30() real ext-real Element of REAL
g is V30() real ext-real Element of REAL
{ b₁ where b₁ is V30() real ext-real Element of REAL : ( not b₁ <= x0 & not x0 + k <= b₁ ) } is set
g2 is V30() real ext-real Element of REAL
g2 is V30() real ext-real Element of REAL
(dom r) /\ ].x0,(x0 + k).[ is V71() V72() V73() Element of K19(REAL)
(dom f) /\ ].x0,(x0 + k).[ is V71() V72() V73() Element of K19(REAL)
(dom s) /\ ].x0,(x0 + k).[ is V71() V72() V73() Element of K19(REAL)
x0 is V30() real ext-real Element of REAL
f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom f is V71() V72() V73() Element of K19(REAL)
(f,x0) is V30() real ext-real Element of REAL
r is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom r is V71() V72() V73() Element of K19(REAL)
(r,x0) is V30() real ext-real Element of REAL
s is V30() real ext-real Element of REAL
x0 - s is V30() real ext-real Element of REAL
].(x0 - s),x0.[ is V71() V72() V73() Element of K19(REAL)
(dom f) /\ ].(x0 - s),x0.[ is V71() V72() V73() Element of K19(REAL)
(dom r) /\ ].(x0 - s),x0.[ is V71() V72() V73() Element of K19(REAL)
k is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
k + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
1 / (k + 1) is V30() real ext-real non negative Element of REAL
x0 - (1 / (k + 1)) is V30() real ext-real Element of REAL
n is V30() real ext-real Element of REAL
g2 is V30() real ext-real Element of REAL
k is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim k is V30() real ext-real Element of REAL
rng k is V71() V72() V73() Element of K19(REAL)
left_open_halfline x0 is V71() V72() V73() Element of K19(REAL)
K213(-infty,x0) is set
(dom f) /\ (left_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
k ^\ n is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of k
lim (k ^\ n) is V30() real ext-real Element of REAL
g2 is set
rng (k ^\ n) is V71() V72() V73() Element of K19(REAL)
n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
(k ^\ n) . n is V30() real ext-real Element of REAL
n + n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
k . (n + n) is V30() real ext-real Element of REAL
{ b₁ where b₁ is V30() real ext-real Element of REAL : ( not b₁ <= x0 - s & not x0 <= b₁ ) } is set
(dom r) /\ (left_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
r /* (k ^\ n) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim (r /* (k ^\ n)) is V30() real ext-real Element of REAL
f /* (k ^\ n) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim (f /* (k ^\ n)) is V30() real ext-real Element of REAL
g2 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
(k ^\ n) . g2 is V30() real ext-real Element of REAL
f . ((k ^\ n) . g2) is V30() real ext-real Element of REAL
r . ((k ^\ n) . g2) is V30() real ext-real Element of REAL
(r /* (k ^\ n)) . g2 is V30() real ext-real Element of REAL
(f /* (k ^\ n)) . g2 is V30() real ext-real Element of REAL
k is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
k + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
1 / (k + 1) is V30() real ext-real non negative Element of REAL
x0 - 0 is V30() real ext-real Element of REAL
x0 - (1 / (k + 1)) is V30() real ext-real Element of REAL
n is V30() real ext-real Element of REAL
g2 is V30() real ext-real Element of REAL
k is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim k is V30() real ext-real Element of REAL
rng k is V71() V72() V73() Element of K19(REAL)
left_open_halfline x0 is V71() V72() V73() Element of K19(REAL)
K213(-infty,x0) is set
(dom r) /\ (left_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
k ^\ n is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of k
lim (k ^\ n) is V30() real ext-real Element of REAL
g2 is set
rng (k ^\ n) is V71() V72() V73() Element of K19(REAL)
n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
(k ^\ n) . n is V30() real ext-real Element of REAL
n + n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
k . (n + n) is V30() real ext-real Element of REAL
{ b₁ where b₁ is V30() real ext-real Element of REAL : ( not b₁ <= x0 - s & not x0 <= b₁ ) } is set
(dom f) /\ (left_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
f /* (k ^\ n) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim (f /* (k ^\ n)) is V30() real ext-real Element of REAL
r /* (k ^\ n) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim (r /* (k ^\ n)) is V30() real ext-real Element of REAL
g2 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
(k ^\ n) . g2 is V30() real ext-real Element of REAL
f . ((k ^\ n) . g2) is V30() real ext-real Element of REAL
r . ((k ^\ n) . g2) is V30() real ext-real Element of REAL
(r /* (k ^\ n)) . g2 is V30() real ext-real Element of REAL
(f /* (k ^\ n)) . g2 is V30() real ext-real Element of REAL
k is V30() real ext-real Element of REAL
f . k is V30() real ext-real Element of REAL
r . k is V30() real ext-real Element of REAL
n is V30() real ext-real Element of REAL
f . n is V30() real ext-real Element of REAL
r . n is V30() real ext-real Element of REAL
x0 is V30() real ext-real Element of REAL
f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom f is V71() V72() V73() Element of K19(REAL)
(f,x0) is V30() real ext-real Element of REAL
r is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom r is V71() V72() V73() Element of K19(REAL)
(r,x0) is V30() real ext-real Element of REAL
s is V30() real ext-real Element of REAL
x0 + s is V30() real ext-real Element of REAL
].x0,(x0 + s).[ is V71() V72() V73() Element of K19(REAL)
(dom f) /\ ].x0,(x0 + s).[ is V71() V72() V73() Element of K19(REAL)
(dom r) /\ ].x0,(x0 + s).[ is V71() V72() V73() Element of K19(REAL)
k is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
k + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
1 / (k + 1) is V30() real ext-real non negative Element of REAL
x0 + (1 / (k + 1)) is V30() real ext-real Element of REAL
n is V30() real ext-real Element of REAL
g2 is V30() real ext-real Element of REAL
k is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim k is V30() real ext-real Element of REAL
rng k is V71() V72() V73() Element of K19(REAL)
right_open_halfline x0 is V71() V72() V73() Element of K19(REAL)
K213(x0,+infty) is set
(dom f) /\ (right_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
k ^\ n is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of k
lim (k ^\ n) is V30() real ext-real Element of REAL
g2 is set
rng (k ^\ n) is V71() V72() V73() Element of K19(REAL)
n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
(k ^\ n) . n is V30() real ext-real Element of REAL
n + n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
k . (n + n) is V30() real ext-real Element of REAL
{ b₁ where b₁ is V30() real ext-real Element of REAL : ( not b₁ <= x0 & not x0 + s <= b₁ ) } is set
(dom r) /\ (right_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
r /* (k ^\ n) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim (r /* (k ^\ n)) is V30() real ext-real Element of REAL
f /* (k ^\ n) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim (f /* (k ^\ n)) is V30() real ext-real Element of REAL
g2 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
(k ^\ n) . g2 is V30() real ext-real Element of REAL
f . ((k ^\ n) . g2) is V30() real ext-real Element of REAL
r . ((k ^\ n) . g2) is V30() real ext-real Element of REAL
(r /* (k ^\ n)) . g2 is V30() real ext-real Element of REAL
(f /* (k ^\ n)) . g2 is V30() real ext-real Element of REAL
k is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
k + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
1 / (k + 1) is V30() real ext-real non negative Element of REAL
x0 + (1 / (k + 1)) is V30() real ext-real Element of REAL
x0 + 0 is V30() real ext-real Element of REAL
n is V30() real ext-real Element of REAL
g2 is V30() real ext-real Element of REAL
k is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim k is V30() real ext-real Element of REAL
rng k is V71() V72() V73() Element of K19(REAL)
right_open_halfline x0 is V71() V72() V73() Element of K19(REAL)
K213(x0,+infty) is set
(dom r) /\ (right_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
k ^\ n is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of k
lim (k ^\ n) is V30() real ext-real Element of REAL
g2 is set
rng (k ^\ n) is V71() V72() V73() Element of K19(REAL)
n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
(k ^\ n) . n is V30() real ext-real Element of REAL
n + n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
k . (n + n) is V30() real ext-real Element of REAL
{ b₁ where b₁ is V30() real ext-real Element of REAL : ( not b₁ <= x0 & not x0 + s <= b₁ ) } is set
(dom f) /\ (right_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
f /* (k ^\ n) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim (f /* (k ^\ n)) is V30() real ext-real Element of REAL
r /* (k ^\ n) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim (r /* (k ^\ n)) is V30() real ext-real Element of REAL
g2 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
(k ^\ n) . g2 is V30() real ext-real Element of REAL
f . ((k ^\ n) . g2) is V30() real ext-real Element of REAL
r . ((k ^\ n) . g2) is V30() real ext-real Element of REAL
(r /* (k ^\ n)) . g2 is V30() real ext-real Element of REAL
(f /* (k ^\ n)) . g2 is V30() real ext-real Element of REAL
k is V30() real ext-real Element of REAL
f . k is V30() real ext-real Element of REAL
r . k is V30() real ext-real Element of REAL
n is V30() real ext-real Element of REAL
f . n is V30() real ext-real Element of REAL
r . n is V30() real ext-real Element of REAL
x0 is V30() real ext-real Element of REAL
f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom f is V71() V72() V73() Element of K19(REAL)
f ^ is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
((f ^),x0) is V30() real ext-real Element of REAL
dom (f ^) is V71() V72() V73() Element of K19(REAL)
f " {0} is V71() V72() V73() Element of K19(REAL)
(dom f) \ (f " {0}) is V71() V72() V73() Element of K19(REAL)
r is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim r is V30() real ext-real Element of REAL
rng r is V71() V72() V73() Element of K19(REAL)
left_open_halfline x0 is V71() V72() V73() Element of K19(REAL)
K213(-infty,x0) is set
(dom (f ^)) /\ (left_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
(dom f) /\ (left_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
f /* r is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f /* r) " is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim ((f /* r) ") is V30() real ext-real Element of REAL
(f ^) /* r is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim ((f ^) /* r) is V30() real ext-real Element of REAL
f /* r is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f /* r) " is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim ((f /* r) ") is V30() real ext-real Element of REAL
(f ^) /* r is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim ((f ^) /* r) is V30() real ext-real Element of REAL
(f ^) /* r is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim ((f ^) /* r) is V30() real ext-real Element of REAL
(f ^) /* r is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim ((f ^) /* r) is V30() real ext-real Element of REAL
r is V30() real ext-real Element of REAL
s is V30() real ext-real Element of REAL
f . s is V30() real ext-real Element of REAL
k is V30() real ext-real Element of REAL
f . k is V30() real ext-real Element of REAL
x0 is V30() real ext-real Element of REAL
f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom f is V71() V72() V73() Element of K19(REAL)
f ^ is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
((f ^),x0) is V30() real ext-real Element of REAL
dom (f ^) is V71() V72() V73() Element of K19(REAL)
f " {0} is V71() V72() V73() Element of K19(REAL)
(dom f) \ (f " {0}) is V71() V72() V73() Element of K19(REAL)
r is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim r is V30() real ext-real Element of REAL
rng r is V71() V72() V73() Element of K19(REAL)
right_open_halfline x0 is V71() V72() V73() Element of K19(REAL)
K213(x0,+infty) is set
(dom (f ^)) /\ (right_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
(dom f) /\ (right_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
f /* r is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f /* r) " is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim ((f /* r) ") is V30() real ext-real Element of REAL
(f ^) /* r is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim ((f ^) /* r) is V30() real ext-real Element of REAL
f /* r is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f /* r) " is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim ((f /* r) ") is V30() real ext-real Element of REAL
(f ^) /* r is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim ((f ^) /* r) is V30() real ext-real Element of REAL
(f ^) /* r is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim ((f ^) /* r) is V30() real ext-real Element of REAL
(f ^) /* r is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim ((f ^) /* r) is V30() real ext-real Element of REAL
r is V30() real ext-real Element of REAL
s is V30() real ext-real Element of REAL
f . s is V30() real ext-real Element of REAL
k is V30() real ext-real Element of REAL
f . k is V30() real ext-real Element of REAL
x0 is V30() real ext-real Element of REAL
f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
(f,x0) is V30() real ext-real Element of REAL
dom f is V71() V72() V73() Element of K19(REAL)
f ^ is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
r is V30() real ext-real Element of REAL
x0 - r is V30() real ext-real Element of REAL
].(x0 - r),x0.[ is V71() V72() V73() Element of K19(REAL)
(dom f) /\ ].(x0 - r),x0.[ is V71() V72() V73() Element of K19(REAL)
dom (f ^) is V71() V72() V73() Element of K19(REAL)
s is V30() real ext-real Element of REAL
k is V30() real ext-real Element of REAL
n is V30() real ext-real Element of REAL
g2 is V30() real ext-real Element of REAL
{ b₁ where b₁ is V30() real ext-real Element of REAL : ( not b₁ <= x0 - r & not x0 <= b₁ ) } is set
f . g2 is V30() real ext-real Element of REAL
f " {0} is V71() V72() V73() Element of K19(REAL)
(dom f) \ (f " {0}) is V71() V72() V73() Element of K19(REAL)
n is V30() real ext-real Element of REAL
g2 is V30() real ext-real Element of REAL
{ b₁ where b₁ is V30() real ext-real Element of REAL : ( not b₁ <= x0 - r & not x0 <= b₁ ) } is set
f . g2 is V30() real ext-real Element of REAL
f " {0} is V71() V72() V73() Element of K19(REAL)
(dom f) \ (f " {0}) is V71() V72() V73() Element of K19(REAL)
n is V30() real ext-real Element of REAL
left_open_halfline x0 is V71() V72() V73() Element of K19(REAL)
K213(-infty,x0) is set
(dom (f ^)) /\ (left_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim s is V30() real ext-real Element of REAL
rng s is V71() V72() V73() Element of K19(REAL)
(f ^) /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
k is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
s ^\ k is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of s
lim (s ^\ k) is V30() real ext-real Element of REAL
f " {0} is V71() V72() V73() Element of K19(REAL)
(dom f) \ (f " {0}) is V71() V72() V73() Element of K19(REAL)
rng (s ^\ k) is V71() V72() V73() Element of K19(REAL)
(dom f) /\ (left_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
f /* (s ^\ k) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim (f /* (s ^\ k)) is V30() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
n + k is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
s . (n + k) is V30() real ext-real Element of REAL
(s ^\ k) . n is V30() real ext-real Element of REAL
{ b₁ where b₁ is V30() real ext-real Element of REAL : not x0 <= b₁ } is set
{ b₁ where b₁ is V30() real ext-real Element of REAL : ( not b₁ <= x0 - r & not x0 <= b₁ ) } is set
g2 is V30() real ext-real Element of REAL
f . ((s ^\ k) . n) is V30() real ext-real Element of REAL
(f /* (s ^\ k)) . n is V30() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
(f /* (s ^\ k)) . n is V30() real ext-real Element of REAL
(f /* (s ^\ k)) " is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
f /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f /* s) ^\ k is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of f /* s
((f /* s) ^\ k) " is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f /* s) " is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
((f /* s) ") ^\ k is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of (f /* s) "
((f ^) /* s) ^\ k is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of (f ^) /* s
x0 is V30() real ext-real Element of REAL
f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
(f,x0) is V30() real ext-real Element of REAL
dom f is V71() V72() V73() Element of K19(REAL)
f ^ is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
r is V30() real ext-real Element of REAL
x0 - r is V30() real ext-real Element of REAL
].(x0 - r),x0.[ is V71() V72() V73() Element of K19(REAL)
(dom f) /\ ].(x0 - r),x0.[ is V71() V72() V73() Element of K19(REAL)
dom (f ^) is V71() V72() V73() Element of K19(REAL)
s is V30() real ext-real Element of REAL
k is V30() real ext-real Element of REAL
n is V30() real ext-real Element of REAL
g2 is V30() real ext-real Element of REAL
{ b₁ where b₁ is V30() real ext-real Element of REAL : ( not b₁ <= x0 - r & not x0 <= b₁ ) } is set
f . g2 is V30() real ext-real Element of REAL
f " {0} is V71() V72() V73() Element of K19(REAL)
(dom f) \ (f " {0}) is V71() V72() V73() Element of K19(REAL)
n is V30() real ext-real Element of REAL
g2 is V30() real ext-real Element of REAL
{ b₁ where b₁ is V30() real ext-real Element of REAL : ( not b₁ <= x0 - r & not x0 <= b₁ ) } is set
f . g2 is V30() real ext-real Element of REAL
f " {0} is V71() V72() V73() Element of K19(REAL)
(dom f) \ (f " {0}) is V71() V72() V73() Element of K19(REAL)
n is V30() real ext-real Element of REAL
left_open_halfline x0 is V71() V72() V73() Element of K19(REAL)
K213(-infty,x0) is set
(dom (f ^)) /\ (left_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim s is V30() real ext-real Element of REAL
rng s is V71() V72() V73() Element of K19(REAL)
(f ^) /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
k is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
s ^\ k is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of s
lim (s ^\ k) is V30() real ext-real Element of REAL
f " {0} is V71() V72() V73() Element of K19(REAL)
(dom f) \ (f " {0}) is V71() V72() V73() Element of K19(REAL)
rng (s ^\ k) is V71() V72() V73() Element of K19(REAL)
(dom f) /\ (left_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
f /* (s ^\ k) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim (f /* (s ^\ k)) is V30() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
n + k is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
s . (n + k) is V30() real ext-real Element of REAL
(s ^\ k) . n is V30() real ext-real Element of REAL
{ b₁ where b₁ is V30() real ext-real Element of REAL : not x0 <= b₁ } is set
{ b₁ where b₁ is V30() real ext-real Element of REAL : ( not b₁ <= x0 - r & not x0 <= b₁ ) } is set
g2 is V30() real ext-real Element of REAL
f . ((s ^\ k) . n) is V30() real ext-real Element of REAL
(f /* (s ^\ k)) . n is V30() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
(f /* (s ^\ k)) . n is V30() real ext-real Element of REAL
(f /* (s ^\ k)) " is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
f /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f /* s) ^\ k is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of f /* s
((f /* s) ^\ k) " is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f /* s) " is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
((f /* s) ") ^\ k is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of (f /* s) "
((f ^) /* s) ^\ k is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of (f ^) /* s
x0 is V30() real ext-real Element of REAL
f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
(f,x0) is V30() real ext-real Element of REAL
dom f is V71() V72() V73() Element of K19(REAL)
f ^ is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
r is V30() real ext-real Element of REAL
x0 + r is V30() real ext-real Element of REAL
].x0,(x0 + r).[ is V71() V72() V73() Element of K19(REAL)
(dom f) /\ ].x0,(x0 + r).[ is V71() V72() V73() Element of K19(REAL)
dom (f ^) is V71() V72() V73() Element of K19(REAL)
s is V30() real ext-real Element of REAL
k is V30() real ext-real Element of REAL
n is V30() real ext-real Element of REAL
g2 is V30() real ext-real Element of REAL
{ b₁ where b₁ is V30() real ext-real Element of REAL : ( not b₁ <= x0 & not x0 + r <= b₁ ) } is set
f . g2 is V30() real ext-real Element of REAL
f " {0} is V71() V72() V73() Element of K19(REAL)
(dom f) \ (f " {0}) is V71() V72() V73() Element of K19(REAL)
n is V30() real ext-real Element of REAL
g2 is V30() real ext-real Element of REAL
{ b₁ where b₁ is V30() real ext-real Element of REAL : ( not b₁ <= x0 & not x0 + r <= b₁ ) } is set
f . g2 is V30() real ext-real Element of REAL
f " {0} is V71() V72() V73() Element of K19(REAL)
(dom f) \ (f " {0}) is V71() V72() V73() Element of K19(REAL)
n is V30() real ext-real Element of REAL
right_open_halfline x0 is V71() V72() V73() Element of K19(REAL)
K213(x0,+infty) is set
(dom (f ^)) /\ (right_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim s is V30() real ext-real Element of REAL
rng s is V71() V72() V73() Element of K19(REAL)
(f ^) /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
k is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
s ^\ k is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of s
lim (s ^\ k) is V30() real ext-real Element of REAL
f " {0} is V71() V72() V73() Element of K19(REAL)
(dom f) \ (f " {0}) is V71() V72() V73() Element of K19(REAL)
rng (s ^\ k) is V71() V72() V73() Element of K19(REAL)
(dom f) /\ (right_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
f /* (s ^\ k) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim (f /* (s ^\ k)) is V30() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
n + k is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
s . (n + k) is V30() real ext-real Element of REAL
(s ^\ k) . n is V30() real ext-real Element of REAL
{ b₁ where b₁ is V30() real ext-real Element of REAL : not b₁ <= x0 } is set
{ b₁ where b₁ is V30() real ext-real Element of REAL : ( not b₁ <= x0 & not x0 + r <= b₁ ) } is set
g2 is V30() real ext-real Element of REAL
f . ((s ^\ k) . n) is V30() real ext-real Element of REAL
(f /* (s ^\ k)) . n is V30() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
(f /* (s ^\ k)) . n is V30() real ext-real Element of REAL
(f /* (s ^\ k)) " is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
f /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f /* s) ^\ k is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of f /* s
((f /* s) ^\ k) " is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f /* s) " is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
((f /* s) ") ^\ k is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of (f /* s) "
((f ^) /* s) ^\ k is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of (f ^) /* s
x0 is V30() real ext-real Element of REAL
f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
(f,x0) is V30() real ext-real Element of REAL
dom f is V71() V72() V73() Element of K19(REAL)
f ^ is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
r is V30() real ext-real Element of REAL
x0 + r is V30() real ext-real Element of REAL
].x0,(x0 + r).[ is V71() V72() V73() Element of K19(REAL)
(dom f) /\ ].x0,(x0 + r).[ is V71() V72() V73() Element of K19(REAL)
dom (f ^) is V71() V72() V73() Element of K19(REAL)
s is V30() real ext-real Element of REAL
k is V30() real ext-real Element of REAL
n is V30() real ext-real Element of REAL
g2 is V30() real ext-real Element of REAL
{ b₁ where b₁ is V30() real ext-real Element of REAL : ( not b₁ <= x0 & not x0 + r <= b₁ ) } is set
f . g2 is V30() real ext-real Element of REAL
f " {0} is V71() V72() V73() Element of K19(REAL)
(dom f) \ (f " {0}) is V71() V72() V73() Element of K19(REAL)
n is V30() real ext-real Element of REAL
g2 is V30() real ext-real Element of REAL
{ b₁ where b₁ is V30() real ext-real Element of REAL : ( not b₁ <= x0 & not x0 + r <= b₁ ) } is set
f . g2 is V30() real ext-real Element of REAL
f " {0} is V71() V72() V73() Element of K19(REAL)
(dom f) \ (f " {0}) is V71() V72() V73() Element of K19(REAL)
n is V30() real ext-real Element of REAL
right_open_halfline x0 is V71() V72() V73() Element of K19(REAL)
K213(x0,+infty) is set
(dom (f ^)) /\ (right_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim s is V30() real ext-real Element of REAL
rng s is V71() V72() V73() Element of K19(REAL)
(f ^) /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
k is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
s ^\ k is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of s
lim (s ^\ k) is V30() real ext-real Element of REAL
f " {0} is V71() V72() V73() Element of K19(REAL)
(dom f) \ (f " {0}) is V71() V72() V73() Element of K19(REAL)
rng (s ^\ k) is V71() V72() V73() Element of K19(REAL)
(dom f) /\ (right_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
f /* (s ^\ k) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim (f /* (s ^\ k)) is V30() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
n + k is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
s . (n + k) is V30() real ext-real Element of REAL
(s ^\ k) . n is V30() real ext-real Element of REAL
{ b₁ where b₁ is V30() real ext-real Element of REAL : not b₁ <= x0 } is set
{ b₁ where b₁ is V30() real ext-real Element of REAL : ( not b₁ <= x0 & not x0 + r <= b₁ ) } is set
g2 is V30() real ext-real Element of REAL
f . ((s ^\ k) . n) is V30() real ext-real Element of REAL
(f /* (s ^\ k)) . n is V30() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
(f /* (s ^\ k)) . n is V30() real ext-real Element of REAL
(f /* (s ^\ k)) " is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
f /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f /* s) ^\ k is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of f /* s
((f /* s) ^\ k) " is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f /* s) " is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
((f /* s) ") ^\ k is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of (f /* s) "
((f ^) /* s) ^\ k is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of (f ^) /* s
x0 is V30() real ext-real Element of REAL
f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
(f,x0) is V30() real ext-real Element of REAL
dom f is V71() V72() V73() Element of K19(REAL)
f ^ is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
r is V30() real ext-real Element of REAL
x0 - r is V30() real ext-real Element of REAL
].(x0 - r),x0.[ is V71() V72() V73() Element of K19(REAL)
(dom f) /\ ].(x0 - r),x0.[ is V71() V72() V73() Element of K19(REAL)
dom (f ^) is V71() V72() V73() Element of K19(REAL)
s is V30() real ext-real Element of REAL
k is V30() real ext-real Element of REAL
f . k is V30() real ext-real Element of REAL
f " {0} is V71() V72() V73() Element of K19(REAL)
(dom f) \ (f " {0}) is V71() V72() V73() Element of K19(REAL)
left_open_halfline x0 is V71() V72() V73() Element of K19(REAL)
K213(-infty,x0) is set
(dom (f ^)) /\ (left_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim s is V30() real ext-real Element of REAL
rng s is V71() V72() V73() Element of K19(REAL)
(f ^) /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
k is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
s ^\ k is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of s
lim (s ^\ k) is V30() real ext-real Element of REAL
rng (s ^\ k) is V71() V72() V73() Element of K19(REAL)
f " {0} is V71() V72() V73() Element of K19(REAL)
(dom f) \ (f " {0}) is V71() V72() V73() Element of K19(REAL)
(dom f) /\ (left_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
f /* (s ^\ k) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim (f /* (s ^\ k)) is V30() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
n + k is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
s . (n + k) is V30() real ext-real Element of REAL
(s ^\ k) . n is V30() real ext-real Element of REAL
{ b₁ where b₁ is V30() real ext-real Element of REAL : not x0 <= b₁ } is set
{ b₁ where b₁ is V30() real ext-real Element of REAL : ( not b₁ <= x0 - r & not x0 <= b₁ ) } is set
g2 is V30() real ext-real Element of REAL
f . ((s ^\ k) . n) is V30() real ext-real Element of REAL
(f /* (s ^\ k)) . n is V30() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
(f /* (s ^\ k)) . n is V30() real ext-real Element of REAL
(f /* (s ^\ k)) " is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
f /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f /* s) ^\ k is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of f /* s
((f /* s) ^\ k) " is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f /* s) " is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
((f /* s) ") ^\ k is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of (f /* s) "
((f ^) /* s) ^\ k is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of (f ^) /* s
x0 is V30() real ext-real Element of REAL
f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
(f,x0) is V30() real ext-real Element of REAL
dom f is V71() V72() V73() Element of K19(REAL)
f ^ is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
r is V30() real ext-real Element of REAL
x0 - r is V30() real ext-real Element of REAL
].(x0 - r),x0.[ is V71() V72() V73() Element of K19(REAL)
(dom f) /\ ].(x0 - r),x0.[ is V71() V72() V73() Element of K19(REAL)
dom (f ^) is V71() V72() V73() Element of K19(REAL)
s is V30() real ext-real Element of REAL
k is V30() real ext-real Element of REAL
f . k is V30() real ext-real Element of REAL
f " {0} is V71() V72() V73() Element of K19(REAL)
(dom f) \ (f " {0}) is V71() V72() V73() Element of K19(REAL)
left_open_halfline x0 is V71() V72() V73() Element of K19(REAL)
K213(-infty,x0) is set
(dom (f ^)) /\ (left_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim s is V30() real ext-real Element of REAL
rng s is V71() V72() V73() Element of K19(REAL)
(f ^) /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
k is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
s ^\ k is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of s
lim (s ^\ k) is V30() real ext-real Element of REAL
rng (s ^\ k) is V71() V72() V73() Element of K19(REAL)
f " {0} is V71() V72() V73() Element of K19(REAL)
(dom f) \ (f " {0}) is V71() V72() V73() Element of K19(REAL)
(dom f) /\ (left_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
f /* (s ^\ k) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim (f /* (s ^\ k)) is V30() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
n + k is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
s . (n + k) is V30() real ext-real Element of REAL
(s ^\ k) . n is V30() real ext-real Element of REAL
{ b₁ where b₁ is V30() real ext-real Element of REAL : not x0 <= b₁ } is set
{ b₁ where b₁ is V30() real ext-real Element of REAL : ( not b₁ <= x0 - r & not x0 <= b₁ ) } is set
g2 is V30() real ext-real Element of REAL
f . ((s ^\ k) . n) is V30() real ext-real Element of REAL
(f /* (s ^\ k)) . n is V30() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
(f /* (s ^\ k)) . n is V30() real ext-real Element of REAL
(f /* (s ^\ k)) " is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
f /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f /* s) ^\ k is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of f /* s
((f /* s) ^\ k) " is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f /* s) " is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
((f /* s) ") ^\ k is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of (f /* s) "
((f ^) /* s) ^\ k is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of (f ^) /* s
x0 is V30() real ext-real Element of REAL
f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
(f,x0) is V30() real ext-real Element of REAL
dom f is V71() V72() V73() Element of K19(REAL)
f ^ is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
r is V30() real ext-real Element of REAL
x0 + r is V30() real ext-real Element of REAL
].x0,(x0 + r).[ is V71() V72() V73() Element of K19(REAL)
(dom f) /\ ].x0,(x0 + r).[ is V71() V72() V73() Element of K19(REAL)
dom (f ^) is V71() V72() V73() Element of K19(REAL)
s is V30() real ext-real Element of REAL
k is V30() real ext-real Element of REAL
f . k is V30() real ext-real Element of REAL
f " {0} is V71() V72() V73() Element of K19(REAL)
(dom f) \ (f " {0}) is V71() V72() V73() Element of K19(REAL)
right_open_halfline x0 is V71() V72() V73() Element of K19(REAL)
K213(x0,+infty) is set
(dom (f ^)) /\ (right_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim s is V30() real ext-real Element of REAL
rng s is V71() V72() V73() Element of K19(REAL)
(f ^) /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
k is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
s ^\ k is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of s
lim (s ^\ k) is V30() real ext-real Element of REAL
rng (s ^\ k) is V71() V72() V73() Element of K19(REAL)
f " {0} is V71() V72() V73() Element of K19(REAL)
(dom f) \ (f " {0}) is V71() V72() V73() Element of K19(REAL)
(dom f) /\ (right_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
f /* (s ^\ k) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim (f /* (s ^\ k)) is V30() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
n + k is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
s . (n + k) is V30() real ext-real Element of REAL
(s ^\ k) . n is V30() real ext-real Element of REAL
{ b₁ where b₁ is V30() real ext-real Element of REAL : not b₁ <= x0 } is set
{ b₁ where b₁ is V30() real ext-real Element of REAL : ( not b₁ <= x0 & not x0 + r <= b₁ ) } is set
g2 is V30() real ext-real Element of REAL
f . ((s ^\ k) . n) is V30() real ext-real Element of REAL
(f /* (s ^\ k)) . n is V30() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
(f /* (s ^\ k)) . n is V30() real ext-real Element of REAL
(f /* (s ^\ k)) " is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
f /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f /* s) ^\ k is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of f /* s
((f /* s) ^\ k) " is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f /* s) " is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
((f /* s) ") ^\ k is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of (f /* s) "
((f ^) /* s) ^\ k is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of (f ^) /* s
x0 is V30() real ext-real Element of REAL
f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
(f,x0) is V30() real ext-real Element of REAL
dom f is V71() V72() V73() Element of K19(REAL)
f ^ is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
r is V30() real ext-real Element of REAL
x0 + r is V30() real ext-real Element of REAL
].x0,(x0 + r).[ is V71() V72() V73() Element of K19(REAL)
(dom f) /\ ].x0,(x0 + r).[ is V71() V72() V73() Element of K19(REAL)
dom (f ^) is V71() V72() V73() Element of K19(REAL)
s is V30() real ext-real Element of REAL
k is V30() real ext-real Element of REAL
f . k is V30() real ext-real Element of REAL
f " {0} is V71() V72() V73() Element of K19(REAL)
(dom f) \ (f " {0}) is V71() V72() V73() Element of K19(REAL)
right_open_halfline x0 is V71() V72() V73() Element of K19(REAL)
K213(x0,+infty) is set
(dom (f ^)) /\ (right_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim s is V30() real ext-real Element of REAL
rng s is V71() V72() V73() Element of K19(REAL)
(f ^) /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
k is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
s ^\ k is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of s
lim (s ^\ k) is V30() real ext-real Element of REAL
rng (s ^\ k) is V71() V72() V73() Element of K19(REAL)
f " {0} is V71() V72() V73() Element of K19(REAL)
(dom f) \ (f " {0}) is V71() V72() V73() Element of K19(REAL)
(dom f) /\ (right_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
f /* (s ^\ k) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim (f /* (s ^\ k)) is V30() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
n + k is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
s . (n + k) is V30() real ext-real Element of REAL
(s ^\ k) . n is V30() real ext-real Element of REAL
{ b₁ where b₁ is V30() real ext-real Element of REAL : not b₁ <= x0 } is set
{ b₁ where b₁ is V30() real ext-real Element of REAL : ( not b₁ <= x0 & not x0 + r <= b₁ ) } is set
g2 is V30() real ext-real Element of REAL
f . ((s ^\ k) . n) is V30() real ext-real Element of REAL
(f /* (s ^\ k)) . n is V30() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT
(f /* (s ^\ k)) . n is V30() real ext-real Element of REAL
(f /* (s ^\ k)) " is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
f /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f /* s) ^\ k is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of f /* s
((f /* s) ^\ k) " is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f /* s) " is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
((f /* s) ") ^\ k is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of (f /* s) "
((f ^) /* s) ^\ k is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of (f ^) /* s