REAL is non empty V49() V69() V70() V71() V75() set
NAT is non empty epsilon-transitive epsilon-connected ordinal V69() V70() V71() V72() V73() V74() V75() Element of K6(REAL)
K6(REAL) is set
COMPLEX is non empty V49() V69() V75() set
omega is non empty epsilon-transitive epsilon-connected ordinal V69() V70() V71() V72() V73() V74() V75() set
K6(omega) is set
K7(NAT,REAL) is complex-valued ext-real-valued real-valued set
K6(K7(NAT,REAL)) is set
K6(K6(REAL)) is set
{} is set
the empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative V69() V70() V71() V72() V73() V74() V75() set is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative V69() V70() V71() V72() V73() V74() V75() set
1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
{{},1} is set
RAT is non empty V49() V69() V70() V71() V72() V75() set
INT is non empty V49() V69() V70() V71() V72() V73() V75() set
0 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
{0} is V69() V70() V71() V72() V73() V74() set
K7(REAL,REAL) is complex-valued ext-real-valued real-valued set
K6(K7(REAL,REAL)) is 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
K7(NAT,NAT) is RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued set
K6(K7(NAT,NAT)) is set
x0 is V11() real ext-real set
f is V11() real ext-real set
r is V11() real ext-real set
f - x0 is V11() real ext-real set
r + x0 is V11() real ext-real set
r - 0 is V11() real ext-real Element of REAL
f + 0 is V11() real ext-real Element of REAL
x0 is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
rng x0 is V69() V70() V71() set
f is Relation-like REAL -defined REAL -valued V21() complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
dom f is set
r is Relation-like REAL -defined REAL -valued V21() complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
f (#) r is Relation-like REAL -defined REAL -valued V21() complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
dom (f (#) r) is set
dom r is set
(dom f) /\ (dom r) is set
g is set
(dom (f (#) r)) \ g is Element of K6((dom (f (#) r)))
K6((dom (f (#) r))) is set
(dom f) \ g is Element of K6((dom f))
K6((dom f)) is set
(dom r) \ g is Element of K6((dom r))
K6((dom r)) is set
x0 is V11() real ext-real Element of REAL
f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
f + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
1 / (f + 1) is V11() real ext-real non negative Element of REAL
x0 - (1 / (f + 1)) is V11() real ext-real Element of REAL
x0 + (1 / (f + 1)) is V11() real ext-real Element of REAL
x0 is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
rng x0 is V69() V70() V71() set
f is Relation-like REAL -defined REAL -valued V21() complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
dom f is set
r is Relation-like REAL -defined REAL -valued V21() complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
f + r is Relation-like REAL -defined REAL -valued V21() complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
dom (f + r) is set
dom r is set
(dom f) /\ (dom r) is set
g is set
(dom (f + r)) \ g is Element of K6((dom (f + r)))
K6((dom (f + r))) is set
(dom f) \ g is Element of K6((dom f))
K6((dom f)) is set
(dom r) \ g is Element of K6((dom r))
K6((dom r)) is set
x0 is V11() real ext-real Element of REAL
left_open_halfline x0 is V69() V70() V71() Element of K6(REAL)
K195(-infty,x0) is set
right_open_halfline x0 is V69() V70() V71() Element of K6(REAL)
K195(x0,+infty) is set
{x0} is V69() V70() V71() set
f is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
rng f is V69() V70() V71() set
r is Relation-like REAL -defined REAL -valued V21() complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
dom r is set
(dom r) /\ (left_open_halfline x0) is V69() V70() V71() Element of K6(REAL)
(dom r) /\ (right_open_halfline x0) is V69() V70() V71() Element of K6(REAL)
(dom r) \ {x0} is Element of K6((dom r))
K6((dom r)) is set
g is set
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
f . k is V11() real ext-real Element of REAL
{ b1 where b1 is V11() real ext-real Element of REAL : not x0 <= b1 } is set
n is V11() real ext-real Element of REAL
{ b1 where b1 is V11() real ext-real Element of REAL : not b1 <= x0 } is set
n is V11() real ext-real Element of REAL
x0 is V11() real ext-real Element of REAL
{x0} is V69() V70() V71() set
f is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
lim f is V11() real ext-real Element of REAL
rng f is V69() V70() V71() set
r is Relation-like REAL -defined REAL -valued V21() complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
dom r is set
(dom r) \ {x0} is Element of K6((dom r))
K6((dom r)) is set
g is V11() real ext-real set
g " is V11() real ext-real set
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
g2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
n + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
g2 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
1 / (g2 + 1) is V11() real ext-real non negative Element of REAL
1 / (n + 1) is V11() real ext-real non negative Element of REAL
1 / (g ") is V11() real ext-real Element of REAL
f . g2 is V11() real ext-real Element of REAL
x0 - (f . g2) is V11() real ext-real Element of REAL
abs (x0 - (f . g2)) is V11() real ext-real Element of REAL
(f . g2) - x0 is V11() real ext-real Element of REAL
- ((f . g2) - x0) is V11() real ext-real Element of REAL
abs (- ((f . g2) - x0)) is V11() real ext-real Element of REAL
abs ((f . g2) - x0) is V11() real ext-real Element of REAL
g is set
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
f . k is V11() real ext-real Element of REAL
g is set
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
f . k is V11() real ext-real Element of REAL
x0 - (f . k) is V11() real ext-real Element of REAL
abs (x0 - (f . k)) is V11() real ext-real Element of REAL
(x0 - (f . k)) + (f . k) is V11() real ext-real Element of REAL
0 + (f . k) is V11() real ext-real Element of REAL
x0 is V11() real ext-real Element of REAL
{x0} is V69() V70() V71() set
f is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
lim f is V11() real ext-real Element of REAL
rng f is V69() V70() V71() set
r is Relation-like REAL -defined REAL -valued V21() complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
dom r is set
(dom r) \ {x0} is Element of K6((dom r))
K6((dom r)) is set
g is V11() real ext-real Element of REAL
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
f . n is V11() real ext-real Element of REAL
x0 - (f . n) is V11() real ext-real Element of REAL
abs (x0 - (f . n)) is V11() real ext-real Element of REAL
(f . n) - x0 is V11() real ext-real Element of REAL
abs ((f . n) - x0) is V11() real ext-real Element of REAL
- (x0 - (f . n)) is V11() real ext-real Element of REAL
abs (- (x0 - (f . n))) is V11() real ext-real Element of REAL
g2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
f . g2 is V11() real ext-real Element of REAL
(f . g2) - x0 is V11() real ext-real Element of REAL
x0 is V11() real ext-real Element of REAL
f is V11() real ext-real Element of REAL
f - x0 is V11() real ext-real Element of REAL
f + x0 is V11() real ext-real Element of REAL
].(f - x0),(f + x0).[ is V69() V70() V71() Element of K6(REAL)
{f} is V69() V70() V71() set
].(f - x0),(f + x0).[ \ {f} is V69() V70() V71() Element of K6(REAL)
].(f - x0),f.[ is V69() V70() V71() Element of K6(REAL)
].f,(f + x0).[ is V69() V70() V71() Element of K6(REAL)
].(f - x0),f.[ \/ ].f,(f + x0).[ is V69() V70() V71() Element of K6(REAL)
r is set
g is V11() real ext-real Element of REAL
{ b1 where b1 is V11() real ext-real Element of REAL : ( not b1 <= f - x0 & not f + x0 <= b1 ) } is set
{ b1 where b1 is V11() real ext-real Element of REAL : ( not b1 <= f - x0 & not f <= b1 ) } is set
k is V11() real ext-real Element of REAL
{ b1 where b1 is V11() real ext-real Element of REAL : ( not b1 <= f & not f + x0 <= b1 ) } is set
k is V11() real ext-real Element of REAL
r is set
{ b1 where b1 is V11() real ext-real Element of REAL : ( not b1 <= f - x0 & not f <= b1 ) } is set
g is V11() real ext-real Element of REAL
{ b1 where b1 is V11() real ext-real Element of REAL : ( not b1 <= f - x0 & not f + x0 <= b1 ) } is set
{ b1 where b1 is V11() real ext-real Element of REAL : ( not b1 <= f & not f + x0 <= b1 ) } is set
g is V11() real ext-real Element of REAL
{ b1 where b1 is V11() real ext-real Element of REAL : ( not b1 <= f - x0 & not f + x0 <= b1 ) } is set
x0 is V11() real ext-real Element of REAL
f is V11() real ext-real Element of REAL
f - x0 is V11() real ext-real Element of REAL
].(f - x0),f.[ is V69() V70() V71() Element of K6(REAL)
f + x0 is V11() real ext-real Element of REAL
].f,(f + x0).[ is V69() V70() V71() Element of K6(REAL)
].(f - x0),f.[ \/ ].f,(f + x0).[ is V69() V70() V71() Element of K6(REAL)
r is Relation-like REAL -defined REAL -valued V21() complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
dom r is set
g is V11() real ext-real Element of REAL
k is V11() real ext-real Element of REAL
n is V11() real ext-real Element of REAL
g2 is V11() real ext-real Element of REAL
x0 is V11() real ext-real Element of REAL
{x0} is V69() V70() V71() set
f is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
lim f is V11() real ext-real Element of REAL
rng f is V69() V70() V71() set
r is Relation-like REAL -defined REAL -valued V21() complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
dom r is set
(dom r) \ {x0} is Element of K6((dom r))
K6((dom r)) is set
left_open_halfline x0 is V69() V70() V71() Element of K6(REAL)
K195(-infty,x0) is set
(dom r) /\ (left_open_halfline x0) is V69() V70() V71() Element of K6(REAL)
x0 is V11() real ext-real Element of REAL
f is V11() real ext-real Element of REAL
x0 - f is V11() real ext-real Element of REAL
x0 + f is V11() real ext-real Element of REAL
r is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
lim r is V11() real ext-real Element of REAL
g is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
max (g,k) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
g2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
r . g2 is V11() real ext-real Element of REAL
x0 is V11() real ext-real Element of REAL
f is Relation-like REAL -defined REAL -valued V21() complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
dom f is set
x0 + 1 is V11() real ext-real Element of REAL
r is V11() real ext-real Element of REAL
g is V11() real ext-real Element of REAL
k is V11() real ext-real Element of REAL
x0 - 1 is V11() real ext-real Element of REAL
r is V11() real ext-real Element of REAL
g is V11() real ext-real Element of REAL
k is V11() real ext-real Element of REAL
r is V11() real ext-real Element of REAL
g is V11() real ext-real Element of REAL
k is V11() real ext-real Element of REAL
n is V11() real ext-real Element of REAL
x0 is V11() real ext-real Element of REAL
f is Relation-like REAL -defined REAL -valued V21() complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
dom f is set
{x0} is V69() V70() V71() set
(dom f) \ {x0} is Element of K6((dom f))
K6((dom f)) is set
r is V11() real ext-real Element of REAL
g is V11() real ext-real Element of REAL
k is V11() real ext-real Element of REAL
g is V11() real ext-real Element of REAL
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
k + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
1 / (k + 1) is V11() real ext-real non negative Element of REAL
k is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
rng k is V69() V70() V71() set
lim k is V11() real ext-real Element of REAL
f /* k is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
lim (f /* k) is V11() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
(f /* k) . n is V11() real ext-real Element of REAL
((f /* k) . n) - r is V11() real ext-real Element of REAL
abs (((f /* k) . n) - r) is V11() real ext-real Element of REAL
k . n is V11() real ext-real Element of REAL
f . (k . n) is V11() real ext-real Element of REAL
(f . (k . n)) - r is V11() real ext-real Element of REAL
abs ((f . (k . n)) - r) is V11() real ext-real Element of REAL
r is V11() real ext-real Element of REAL
g is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
lim g is V11() real ext-real Element of REAL
rng g is V69() V70() V71() set
{x0} is V69() V70() V71() set
(dom f) \ {x0} is Element of K6((dom f))
K6((dom f)) is set
k is V11() real ext-real set
n is V11() real ext-real Element of REAL
g2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
c8 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
g . n is V11() real ext-real Element of REAL
x0 - (g . n) is V11() real ext-real Element of REAL
abs (x0 - (g . n)) is V11() real ext-real Element of REAL
f . (g . n) is V11() real ext-real Element of REAL
(f . (g . n)) - r is V11() real ext-real Element of REAL
abs ((f . (g . n)) - r) is V11() real ext-real Element of REAL
f /* g is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(f /* g) . n is V11() real ext-real Element of REAL
((f /* g) . n) - r is V11() real ext-real Element of REAL
abs (((f /* g) . n) - r) is V11() real ext-real Element of REAL
lim (f /* g) is V11() real ext-real Element of REAL
x0 is V11() real ext-real Element of REAL
f is Relation-like REAL -defined REAL -valued V21() complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
dom f is set
r is V11() real ext-real Element of REAL
g is V11() real ext-real Element of REAL
k is V11() real ext-real Element of REAL
r is V11() real ext-real Element of REAL
g is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
g + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
1 / (g + 1) is V11() real ext-real non negative Element of REAL
g is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
rng g is V69() V70() V71() set
{x0} is V69() V70() V71() set
(dom f) \ {x0} is Element of K6((dom f))
K6((dom f)) is set
lim g is V11() real ext-real Element of REAL
f /* g is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
(f /* g) . k is V11() real ext-real Element of REAL
g . k is V11() real ext-real Element of REAL
f . (g . k) is V11() real ext-real Element of REAL
r is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
lim r is V11() real ext-real Element of REAL
rng r is V69() V70() V71() set
{x0} is V69() V70() V71() set
(dom f) \ {x0} is Element of K6((dom f))
K6((dom f)) is set
g is V11() real ext-real Element of REAL
k is V11() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
g2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
c8 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
r . c8 is V11() real ext-real Element of REAL
x0 - (r . c8) is V11() real ext-real Element of REAL
abs (x0 - (r . c8)) is V11() real ext-real Element of REAL
f . (r . c8) is V11() real ext-real Element of REAL
f /* r is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(f /* r) . c8 is V11() real ext-real Element of REAL
x0 is V11() real ext-real Element of REAL
f is Relation-like REAL -defined REAL -valued V21() complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
dom f is set
r is V11() real ext-real Element of REAL
g is V11() real ext-real Element of REAL
k is V11() real ext-real Element of REAL
r is V11() real ext-real Element of REAL
g is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
g + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
1 / (g + 1) is V11() real ext-real non negative Element of REAL
g is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
rng g is V69() V70() V71() set
{x0} is V69() V70() V71() set
(dom f) \ {x0} is Element of K6((dom f))
K6((dom f)) is set
lim g is V11() real ext-real Element of REAL
f /* g is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
(f /* g) . k is V11() real ext-real Element of REAL
g . k is V11() real ext-real Element of REAL
f . (g . k) is V11() real ext-real Element of REAL
r is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
lim r is V11() real ext-real Element of REAL
rng r is V69() V70() V71() set
{x0} is V69() V70() V71() set
(dom f) \ {x0} is Element of K6((dom f))
K6((dom f)) is set
g is V11() real ext-real Element of REAL
k is V11() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
g2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
c8 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
r . c8 is V11() real ext-real Element of REAL
x0 - (r . c8) is V11() real ext-real Element of REAL
abs (x0 - (r . c8)) is V11() real ext-real Element of REAL
f . (r . c8) is V11() real ext-real Element of REAL
f /* r is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(f /* r) . c8 is V11() real ext-real Element of REAL
x0 is V11() real ext-real Element of REAL
f is Relation-like REAL -defined REAL -valued V21() complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
r is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
lim r is V11() real ext-real Element of REAL
rng r is V69() V70() V71() set
dom f is set
left_open_halfline x0 is V69() V70() V71() Element of K6(REAL)
K195(-infty,x0) is set
(dom f) /\ (left_open_halfline x0) is V69() V70() V71() Element of K6(REAL)
{x0} is V69() V70() V71() set
(dom f) \ {x0} is Element of K6((dom f))
K6((dom f)) is set
f /* r is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
r is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
lim r is V11() real ext-real Element of REAL
rng r is V69() V70() V71() set
right_open_halfline x0 is V69() V70() V71() Element of K6(REAL)
K195(x0,+infty) is set
(dom f) /\ (right_open_halfline x0) is V69() V70() V71() Element of K6(REAL)
f /* r is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
r is V11() real ext-real Element of REAL
g is V11() real ext-real Element of REAL
r is V11() real ext-real Element of REAL
r is V11() real ext-real Element of REAL
dom f is set
r is V11() real ext-real Element of REAL
r is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
lim r is V11() real ext-real Element of REAL
rng r is V69() V70() V71() set
{x0} is V69() V70() V71() set
(dom f) \ {x0} is Element of K6((dom f))
K6((dom f)) is set
g is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
g is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
r ^\ g is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued subsequence of r
rng (r ^\ g) is V69() V70() V71() set
left_open_halfline x0 is V69() V70() V71() Element of K6(REAL)
K195(-infty,x0) is set
(dom f) /\ (left_open_halfline x0) is V69() V70() V71() Element of K6(REAL)
k is set
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
(r ^\ g) . n is V11() real ext-real Element of REAL
n + g is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
r . (n + g) is V11() real ext-real Element of REAL
{ b1 where b1 is V11() real ext-real Element of REAL : not x0 <= b1 } is set
f /* (r ^\ g) is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
f /* r is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(f /* r) ^\ g is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued subsequence of f /* r
lim (r ^\ g) is V11() real ext-real Element of REAL
g is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
g is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
r ^\ g is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued subsequence of r
rng (r ^\ g) is V69() V70() V71() set
right_open_halfline x0 is V69() V70() V71() Element of K6(REAL)
K195(x0,+infty) is set
(dom f) /\ (right_open_halfline x0) is V69() V70() V71() Element of K6(REAL)
k is set
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
(r ^\ g) . n is V11() real ext-real Element of REAL
n + g is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
r . (n + g) is V11() real ext-real Element of REAL
{ b1 where b1 is V11() real ext-real Element of REAL : not b1 <= x0 } is set
f /* (r ^\ g) is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
f /* r is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(f /* r) ^\ g is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued subsequence of f /* r
lim (r ^\ g) is V11() real ext-real Element of REAL
g is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
r . k is V11() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
r . n is V11() real ext-real Element of REAL
g is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
r . g is V11() real ext-real Element of REAL
g is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
r . g is V11() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
n + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
g2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
r . g2 is V11() real ext-real Element of REAL
c8 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
r . c8 is V11() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
g2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
c8 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
r . c8 is V11() real ext-real Element of REAL
c8 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
r . c8 is V11() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
N is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
r . N is V11() real ext-real Element of REAL
N9 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
r . N9 is V11() real ext-real Element of REAL
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
n is non empty Relation-like NAT -defined NAT -valued V21() total quasi_total complex-valued ext-real-valued real-valued natural-valued Element of K6(K7(NAT,NAT))
n . 0 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
rng n is V69() V70() V71() V72() V73() V74() set
dom n is V69() V70() V71() V72() V73() V74() set
g2 is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
c8 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
g2 . c8 is V11() real ext-real Element of REAL
rng g2 is V69() V70() V71() set
c8 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
c8 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
g2 . (c8 + 1) is V11() real ext-real Element of REAL
g2 . c8 is V11() real ext-real Element of REAL
c8 is non empty Relation-like NAT -defined NAT -valued V21() total quasi_total complex-valued ext-real-valued real-valued natural-valued increasing non-decreasing Element of K6(K7(NAT,NAT))
r * c8 is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
rng (r * c8) is V69() V70() V71() set
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
r . n is V11() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
r . n is V11() real ext-real Element of REAL
c8 . 0 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
N is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
r . N is V11() real ext-real Element of REAL
N9 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
c8 . N9 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
N is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
r . N is V11() real ext-real Element of REAL
N9 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
r . N9 is V11() real ext-real Element of REAL
G is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
c8 . G is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
G is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
c8 . G is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
G is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
c8 . G is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
N9 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
c8 . N9 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
N9 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
c8 . N9 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
N9 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
c8 . (N9 + 1) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
G is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
c8 . G is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
r . (c8 . (N9 + 1)) is V11() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
N is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
r . N is V11() real ext-real Element of REAL
N9 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
r . N9 is V11() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
r . n is V11() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
r . n is V11() real ext-real Element of REAL
N is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
(r * c8) . N is V11() real ext-real Element of REAL
N + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
(r * c8) . (N + 1) is V11() real ext-real Element of REAL
c8 . N is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
c8 . (N + 1) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
N9 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
G is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
r . G is V11() real ext-real Element of REAL
G is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
r . G is V11() real ext-real Element of REAL
r . (c8 . (N + 1)) is V11() real ext-real Element of REAL
(r * c8) . 0 is V11() real ext-real Element of REAL
left_open_halfline x0 is V69() V70() V71() Element of K6(REAL)
K195(-infty,x0) is set
(dom f) /\ (left_open_halfline x0) is V69() V70() V71() Element of K6(REAL)
N is set
N9 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
(r * c8) . N9 is V11() real ext-real Element of REAL
{ b1 where b1 is V11() real ext-real Element of REAL : not x0 <= b1 } is set
N9 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
N9 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
G is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
r . G is V11() real ext-real Element of REAL
G is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
r . G is V11() real ext-real Element of REAL
N9 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
G is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
G is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
r . G is V11() real ext-real Element of REAL
G is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
r . G is V11() real ext-real Element of REAL
G is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
r is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
n1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
r . n1 is V11() real ext-real Element of REAL
n2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
r . n2 is V11() real ext-real Element of REAL
N is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
N9 is non empty Relation-like NAT -defined NAT -valued V21() total quasi_total complex-valued ext-real-valued real-valued natural-valued Element of K6(K7(NAT,NAT))
N9 . 0 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
rng N9 is V69() V70() V71() V72() V73() V74() set
dom N9 is V69() V70() V71() V72() V73() V74() set
G is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
G is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
G . G is V11() real ext-real Element of REAL
rng G is V69() V70() V71() set
G is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
G + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
G . (G + 1) is V11() real ext-real Element of REAL
G . G is V11() real ext-real Element of REAL
G is non empty Relation-like NAT -defined NAT -valued V21() total quasi_total complex-valued ext-real-valued real-valued natural-valued increasing non-decreasing Element of K6(K7(NAT,NAT))
r * G is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
rng (r * G) is V69() V70() V71() set
G is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
r . G is V11() real ext-real Element of REAL
G is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
r . G is V11() real ext-real Element of REAL
G . 0 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
r is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
r . r is V11() real ext-real Element of REAL
n1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
G . n1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
r is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
r . r is V11() real ext-real Element of REAL
n1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
r . n1 is V11() real ext-real Element of REAL
n2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
G . n2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
G . n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
n2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
G . n2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
n1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
G . n1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
n1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
G . n1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
n1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
G . (n1 + 1) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
n2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
G . n2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
r . (G . (n1 + 1)) is V11() real ext-real Element of REAL
G is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
(r * G) . G is V11() real ext-real Element of REAL
G + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
(r * G) . (G + 1) is V11() real ext-real Element of REAL
G . G is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
G . (G + 1) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
r is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
n1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
r . n1 is V11() real ext-real Element of REAL
n2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
r . n2 is V11() real ext-real Element of REAL
r . (G . (G + 1)) is V11() real ext-real Element of REAL
(r * G) . 0 is V11() real ext-real Element of REAL
right_open_halfline x0 is V69() V70() V71() Element of K6(REAL)
K195(x0,+infty) is set
(dom f) /\ (right_open_halfline x0) is V69() V70() V71() Element of K6(REAL)
G is set
r is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
(r * G) . r is V11() real ext-real Element of REAL
{ b1 where b1 is V11() real ext-real Element of REAL : not b1 <= x0 } is set
lim (r * G) is V11() real ext-real Element of REAL
f /* (r * G) is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
lim (r * c8) is V11() real ext-real Element of REAL
f /* (r * c8) is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
G is V11() real ext-real Element of REAL
r is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
n1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
c8 . r is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
G . n1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
max ((c8 . r),(G . n1)) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
n2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
r . n is V11() real ext-real Element of REAL
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
c8 . k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
(f /* (r * c8)) . k is V11() real ext-real Element of REAL
(r * c8) . k is V11() real ext-real Element of REAL
f . ((r * c8) . k) is V11() real ext-real Element of REAL
f . (r . n) is V11() real ext-real Element of REAL
f /* r is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(f /* r) . n is V11() real ext-real Element of REAL
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
G . k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
(f /* (r * G)) . k is V11() real ext-real Element of REAL
(r * G) . k is V11() real ext-real Element of REAL
f . ((r * G) . k) is V11() real ext-real Element of REAL
f . (r . n) is V11() real ext-real Element of REAL
f /* r is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(f /* r) . n is V11() real ext-real Element of REAL
f /* r is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(f /* r) . n is V11() real ext-real Element of REAL
f /* r is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(f /* r) . n is V11() real ext-real Element of REAL
g is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
f /* r is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
f /* r is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
g is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
f /* r is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
f /* r is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
r is V11() real ext-real Element of REAL
r is V11() real ext-real Element of REAL
g is V11() real ext-real Element of REAL
x0 is V11() real ext-real Element of REAL
f is Relation-like REAL -defined REAL -valued V21() complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
r is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
lim r is V11() real ext-real Element of REAL
rng r is V69() V70() V71() set
dom f is set
left_open_halfline x0 is V69() V70() V71() Element of K6(REAL)
K195(-infty,x0) is set
(dom f) /\ (left_open_halfline x0) is V69() V70() V71() Element of K6(REAL)
{x0} is V69() V70() V71() set
(dom f) \ {x0} is Element of K6((dom f))
K6((dom f)) is set
f /* r is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
r is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
lim r is V11() real ext-real Element of REAL
rng r is V69() V70() V71() set
right_open_halfline x0 is V69() V70() V71() Element of K6(REAL)
K195(x0,+infty) is set
(dom f) /\ (right_open_halfline x0) is V69() V70() V71() Element of K6(REAL)
f /* r is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
r is V11() real ext-real Element of REAL
g is V11() real ext-real Element of REAL
r is V11() real ext-real Element of REAL
r is V11() real ext-real Element of REAL
r is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
lim r is V11() real ext-real Element of REAL
rng r is V69() V70() V71() set
dom f is set
{x0} is V69() V70() V71() set
(dom f) \ {x0} is Element of K6((dom f))
K6((dom f)) is set
g is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
g is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
r ^\ g is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued subsequence of r
rng (r ^\ g) is V69() V70() V71() set
left_open_halfline x0 is V69() V70() V71() Element of K6(REAL)
K195(-infty,x0) is set
(dom f) /\ (left_open_halfline x0) is V69() V70() V71() Element of K6(REAL)
k is set
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
(r ^\ g) . n is V11() real ext-real Element of REAL
n + g is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
r . (n + g) is V11() real ext-real Element of REAL
{ b1 where b1 is V11() real ext-real Element of REAL : not x0 <= b1 } is set
f /* (r ^\ g) is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
f /* r is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(f /* r) ^\ g is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued subsequence of f /* r
lim (r ^\ g) is V11() real ext-real Element of REAL
g is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
g is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
r ^\ g is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued subsequence of r
rng (r ^\ g) is V69() V70() V71() set
right_open_halfline x0 is V69() V70() V71() Element of K6(REAL)
K195(x0,+infty) is set
(dom f) /\ (right_open_halfline x0) is V69() V70() V71() Element of K6(REAL)
k is set
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
(r ^\ g) . n is V11() real ext-real Element of REAL
n + g is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
r . (n + g) is V11() real ext-real Element of REAL
{ b1 where b1 is V11() real ext-real Element of REAL : not b1 <= x0 } is set
f /* (r ^\ g) is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
f /* r is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(f /* r) ^\ g is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued subsequence of f /* r
lim (r ^\ g) is V11() real ext-real Element of REAL
g is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
r . k is V11() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
r . n is V11() real ext-real Element of REAL
g is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
r . g is V11() real ext-real Element of REAL
g is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
r . g is V11() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
n + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
g2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
r . g2 is V11() real ext-real Element of REAL
c8 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
r . c8 is V11() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
g2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
c8 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
r . c8 is V11() real ext-real Element of REAL
c8 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
r . c8 is V11() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
N is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
r . N is V11() real ext-real Element of REAL
N9 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
r . N9 is V11() real ext-real Element of REAL
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
n is non empty Relation-like NAT -defined NAT -valued V21() total quasi_total complex-valued ext-real-valued real-valued natural-valued Element of K6(K7(NAT,NAT))
n . 0 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
rng n is V69() V70() V71() V72() V73() V74() set
dom n is V69() V70() V71() V72() V73() V74() set
g2 is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
c8 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
g2 . c8 is V11() real ext-real Element of REAL
rng g2 is V69() V70() V71() set
c8 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
c8 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
g2 . (c8 + 1) is V11() real ext-real Element of REAL
g2 . c8 is V11() real ext-real Element of REAL
c8 is non empty Relation-like NAT -defined NAT -valued V21() total quasi_total complex-valued ext-real-valued real-valued natural-valued increasing non-decreasing Element of K6(K7(NAT,NAT))
r * c8 is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
rng (r * c8) is V69() V70() V71() set
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
r . n is V11() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
r . n is V11() real ext-real Element of REAL
c8 . 0 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
N is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
r . N is V11() real ext-real Element of REAL
N9 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
c8 . N9 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
N is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
r . N is V11() real ext-real Element of REAL
N9 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
r . N9 is V11() real ext-real Element of REAL
G is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
c8 . G is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
G is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
c8 . G is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
G is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
c8 . G is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
N9 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
c8 . N9 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
N9 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
c8 . N9 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
N9 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
c8 . (N9 + 1) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
G is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
c8 . G is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
r . (c8 . (N9 + 1)) is V11() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
N is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
r . N is V11() real ext-real Element of REAL
N9 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
r . N9 is V11() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
r . n is V11() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
r . n is V11() real ext-real Element of REAL
N is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
(r * c8) . N is V11() real ext-real Element of REAL
N + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
(r * c8) . (N + 1) is V11() real ext-real Element of REAL
c8 . N is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
c8 . (N + 1) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
N9 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
G is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
r . G is V11() real ext-real Element of REAL
G is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
r . G is V11() real ext-real Element of REAL
r . (c8 . (N + 1)) is V11() real ext-real Element of REAL
(r * c8) . 0 is V11() real ext-real Element of REAL
left_open_halfline x0 is V69() V70() V71() Element of K6(REAL)
K195(-infty,x0) is set
(dom f) /\ (left_open_halfline x0) is V69() V70() V71() Element of K6(REAL)
N is set
N9 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
(r * c8) . N9 is V11() real ext-real Element of REAL
{ b1 where b1 is V11() real ext-real Element of REAL : not x0 <= b1 } is set
lim (r * c8) is V11() real ext-real Element of REAL
f /* (r * c8) is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
N9 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
N9 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
G is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
r . G is V11() real ext-real Element of REAL
G is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
r . G is V11() real ext-real Element of REAL
N9 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
G is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
G is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
r . G is V11() real ext-real Element of REAL
G is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
r . G is V11() real ext-real Element of REAL
G is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
r is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
r . r is V11() real ext-real Element of REAL
n1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
r . n1 is V11() real ext-real Element of REAL
N is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
N9 is non empty Relation-like NAT -defined NAT -valued V21() total quasi_total complex-valued ext-real-valued real-valued natural-valued Element of K6(K7(NAT,NAT))
N9 . 0 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
rng N9 is V69() V70() V71() V72() V73() V74() set
dom N9 is V69() V70() V71() V72() V73() V74() set
G is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
G is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
G . G is V11() real ext-real Element of REAL
rng G is V69() V70() V71() set
G is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
G + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
G . (G + 1) is V11() real ext-real Element of REAL
G . G is V11() real ext-real Element of REAL
G is non empty Relation-like NAT -defined NAT -valued V21() total quasi_total complex-valued ext-real-valued real-valued natural-valued increasing non-decreasing Element of K6(K7(NAT,NAT))
r * G is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
rng (r * G) is V69() V70() V71() set
G is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
r . G is V11() real ext-real Element of REAL
G is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
r . G is V11() real ext-real Element of REAL
G . 0 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
r is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
r . r is V11() real ext-real Element of REAL
n1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
G . n1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
r is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
r . r is V11() real ext-real Element of REAL
n1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
r . n1 is V11() real ext-real Element of REAL
n2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
G . n2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
G . n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
n2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
G . n2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
n1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
G . n1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
n1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
G . n1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
n1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
G . (n1 + 1) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
n2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
G . n2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
r . (G . (n1 + 1)) is V11() real ext-real Element of REAL
G is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
(r * G) . G is V11() real ext-real Element of REAL
G + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
(r * G) . (G + 1) is V11() real ext-real Element of REAL
G . G is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
G . (G + 1) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
r is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
n1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
r . n1 is V11() real ext-real Element of REAL
n2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
r . n2 is V11() real ext-real Element of REAL
r . (G . (G + 1)) is V11() real ext-real Element of REAL
(r * G) . 0 is V11() real ext-real Element of REAL
right_open_halfline x0 is V69() V70() V71() Element of K6(REAL)
K195(x0,+infty) is set
(dom f) /\ (right_open_halfline x0) is V69() V70() V71() Element of K6(REAL)
G is set
r is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
(r * G) . r is V11() real ext-real Element of REAL
{ b1 where b1 is V11() real ext-real Element of REAL : not b1 <= x0 } is set
lim (r * G) is V11() real ext-real Element of REAL
f /* (r * G) is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
G is V11() real ext-real Element of REAL
r is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
n1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
c8 . r is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
G . n1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
max ((c8 . r),(G . n1)) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
n2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
r . n is V11() real ext-real Element of REAL
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
c8 . k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
(f /* (r * c8)) . k is V11() real ext-real Element of REAL
(r * c8) . k is V11() real ext-real Element of REAL
f . ((r * c8) . k) is V11() real ext-real Element of REAL
f . (r . n) is V11() real ext-real Element of REAL
f /* r is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(f /* r) . n is V11() real ext-real Element of REAL
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
G . k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
(f /* (r * G)) . k is V11() real ext-real Element of REAL
(r * G) . k is V11() real ext-real Element of REAL
f . ((r * G) . k) is V11() real ext-real Element of REAL
f . (r . n) is V11() real ext-real Element of REAL
f /* r is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(f /* r) . n is V11() real ext-real Element of REAL
f /* r is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(f /* r) . n is V11() real ext-real Element of REAL
f /* r is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(f /* r) . n is V11() real ext-real Element of REAL
g is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
f /* r is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
f /* r is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
g is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
f /* r is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
f /* r is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
r is V11() real ext-real Element of REAL
g is V11() real ext-real Element of REAL
k is V11() real ext-real Element of REAL
n is V11() real ext-real Element of REAL
g2 is V11() real ext-real Element of REAL
c8 is V11() real ext-real Element of REAL
x0 is V11() real ext-real Element of REAL
f is Relation-like REAL -defined REAL -valued V21() complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
dom f is set
r is Relation-like REAL -defined REAL -valued V21() complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
dom r is set
(dom f) /\ (dom r) is set
f + r is Relation-like REAL -defined REAL -valued V21() complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
f (#) r is Relation-like REAL -defined REAL -valued V21() complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
g is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
lim g is V11() real ext-real Element of REAL
rng g is V69() V70() V71() set
dom (f + r) is set
{x0} is V69() V70() V71() set
(dom (f + r)) \ {x0} is Element of K6((dom (f + r)))
K6((dom (f + r))) is set
(dom r) \ {x0} is Element of K6((dom r))
K6((dom r)) is set
r /* g is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(dom f) \ {x0} is Element of K6((dom f))
K6((dom f)) is set
f /* g is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(f /* g) + (r /* g) is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(f + r) /* g is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
g is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
lim g is V11() real ext-real Element of REAL
rng g is V69() V70() V71() set
dom (f (#) r) is set
(dom (f (#) r)) \ {x0} is Element of K6((dom (f (#) r)))
K6((dom (f (#) r))) is set
r /* g is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
f /* g is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(f /* g) (#) (r /* g) is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(f (#) r) /* g is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
g is V11() real ext-real Element of REAL
k is V11() real ext-real Element of REAL
n is V11() real ext-real Element of REAL
g2 is V11() real ext-real Element of REAL
c8 is V11() real ext-real Element of REAL
n is V11() real ext-real Element of REAL
g is V11() real ext-real Element of REAL
k is V11() real ext-real Element of REAL
n is V11() real ext-real Element of REAL
g2 is V11() real ext-real Element of REAL
c8 is V11() real ext-real Element of REAL
n is V11() real ext-real Element of REAL
x0 is V11() real ext-real Element of REAL
f is Relation-like REAL -defined REAL -valued V21() complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
dom f is set
r is Relation-like REAL -defined REAL -valued V21() complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
dom r is set
(dom f) /\ (dom r) is set
f + r is Relation-like REAL -defined REAL -valued V21() complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
f (#) r is Relation-like REAL -defined REAL -valued V21() complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
g is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
lim g is V11() real ext-real Element of REAL
rng g is V69() V70() V71() set
dom (f + r) is set
{x0} is V69() V70() V71() set
(dom (f + r)) \ {x0} is Element of K6((dom (f + r)))
K6((dom (f + r))) is set
(dom r) \ {x0} is Element of K6((dom r))
K6((dom r)) is set
r /* g is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(dom f) \ {x0} is Element of K6((dom f))
K6((dom f)) is set
f /* g is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(f /* g) + (r /* g) is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(f + r) /* g is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
g is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
lim g is V11() real ext-real Element of REAL
rng g is V69() V70() V71() set
dom (f (#) r) is set
(dom (f (#) r)) \ {x0} is Element of K6((dom (f (#) r)))
K6((dom (f (#) r))) is set
r /* g is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
f /* g is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(f /* g) (#) (r /* g) is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(f (#) r) /* g is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
g is V11() real ext-real Element of REAL
k is V11() real ext-real Element of REAL
n is V11() real ext-real Element of REAL
g2 is V11() real ext-real Element of REAL
c8 is V11() real ext-real Element of REAL
n is V11() real ext-real Element of REAL
g is V11() real ext-real Element of REAL
k is V11() real ext-real Element of REAL
n is V11() real ext-real Element of REAL
g2 is V11() real ext-real Element of REAL
c8 is V11() real ext-real Element of REAL
n is V11() real ext-real Element of REAL
x0 is V11() real ext-real Element of REAL
f is Relation-like REAL -defined REAL -valued V21() complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
r is Relation-like REAL -defined REAL -valued V21() complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
f + r is Relation-like REAL -defined REAL -valued V21() complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
dom (f + r) is set
g is V11() real ext-real Element of REAL
x0 - g is V11() real ext-real Element of REAL
].(x0 - g),x0.[ is V69() V70() V71() Element of K6(REAL)
x0 + g is V11() real ext-real Element of REAL
].x0,(x0 + g).[ is V69() V70() V71() Element of K6(REAL)
].(x0 - g),x0.[ \/ ].x0,(x0 + g).[ is V69() V70() V71() Element of K6(REAL)
r | (].(x0 - g),x0.[ \/ ].x0,(x0 + g).[) is Relation-like REAL -defined REAL -valued V21() complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
k is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
lim k is V11() real ext-real Element of REAL
rng k is V69() V70() V71() set
{x0} is V69() V70() V71() set
(dom (f + r)) \ {x0} is Element of K6((dom (f + r)))
K6((dom (f + r))) is set
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
k ^\ n is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued subsequence of k
rng (k ^\ n) is V69() V70() V71() set
dom f is set
(dom f) \ {x0} is Element of K6((dom f))
K6((dom f)) is set
dom r is set
(].(x0 - g),x0.[ \/ ].x0,(x0 + g).[) /\ (dom r) is V69() V70() V71() Element of K6(REAL)
g2 is V11() real ext-real set
g2 - 1 is V11() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
n + n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
k . (n + n) is V11() real ext-real Element of REAL
(k ^\ n) . n is V11() real ext-real Element of REAL
{ b1 where b1 is V11() real ext-real Element of REAL : ( not b1 <= x0 - g & not x0 + g <= b1 ) } is set
].(x0 - g),(x0 + g).[ is V69() V70() V71() Element of K6(REAL)
].(x0 - g),(x0 + g).[ \ {x0} is V69() V70() V71() Element of K6(REAL)
r . ((k ^\ n) . n) is V11() real ext-real Element of REAL
(r . ((k ^\ n) . n)) - 0 is V11() real ext-real Element of REAL
r /* (k ^\ n) is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(r /* (k ^\ n)) . n is V11() real ext-real Element of REAL
c8 is V11() real ext-real Element of REAL
g2 is V11() real ext-real Element of REAL
lim (k ^\ n) is V11() real ext-real Element of REAL
f /* (k ^\ n) is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(f /* (k ^\ n)) + (r /* (k ^\ n)) is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(dom f) /\ (dom r) is set
(f + r) /* (k ^\ n) is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(f + r) /* k is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
((f + r) /* k) ^\ n is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued subsequence of (f + r) /* k
x0 is V11() real ext-real Element of REAL
f is Relation-like REAL -defined REAL -valued V21() complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
r is Relation-like REAL -defined REAL -valued V21() complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
f (#) r is Relation-like REAL -defined REAL -valued V21() complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
dom (f (#) r) is set
dom r is set
g is V11() real ext-real Element of REAL
k is V11() real ext-real Element of REAL
x0 - g is V11() real ext-real Element of REAL
].(x0 - g),x0.[ is V69() V70() V71() Element of K6(REAL)
x0 + g is V11() real ext-real Element of REAL
].x0,(x0 + g).[ is V69() V70() V71() Element of K6(REAL)
].(x0 - g),x0.[ \/ ].x0,(x0 + g).[ is V69() V70() V71() Element of K6(REAL)
(dom r) /\ (].(x0 - g),x0.[ \/ ].x0,(x0 + g).[) is V69() V70() V71() Element of K6(REAL)
n is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
lim n is V11() real ext-real Element of REAL
rng n is V69() V70() V71() set
{x0} is V69() V70() V71() set
(dom (f (#) r)) \ {x0} is Element of K6((dom (f (#) r)))
K6((dom (f (#) r))) is set
g2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
dom f is set
(dom f) /\ (dom r) is set
n ^\ g2 is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued subsequence of n
rng (n ^\ g2) is V69() V70() V71() set
(dom f) \ {x0} is Element of K6((dom f))
K6((dom f)) is set
c8 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
c8 + g2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
n . (c8 + g2) is V11() real ext-real Element of REAL
(n ^\ g2) . c8 is V11() real ext-real Element of REAL
{ b1 where b1 is V11() real ext-real Element of REAL : ( not b1 <= x0 - g & not x0 + g <= b1 ) } is set
].(x0 - g),(x0 + g).[ is V69() V70() V71() Element of K6(REAL)
].(x0 - g),(x0 + g).[ \ {x0} is V69() V70() V71() Element of K6(REAL)
r . ((n ^\ g2) . c8) is V11() real ext-real Element of REAL
r /* (n ^\ g2) is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(r /* (n ^\ g2)) . c8 is V11() real ext-real Element of REAL
lim (n ^\ g2) is V11() real ext-real Element of REAL
f /* (n ^\ g2) is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(f /* (n ^\ g2)) (#) (r /* (n ^\ g2)) is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(f (#) r) /* (n ^\ g2) is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(f (#) r) /* n is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
((f (#) r) /* n) ^\ g2 is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued subsequence of (f (#) r) /* n
x0 is V11() real ext-real Element of REAL
f is V11() real ext-real Element of REAL
r is Relation-like REAL -defined REAL -valued V21() complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
f (#) r is Relation-like REAL -defined REAL -valued V21() complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
dom (f (#) r) is set
g is V11() real ext-real Element of REAL
k is V11() real ext-real Element of REAL
dom r is set
n is V11() real ext-real Element of REAL
g2 is V11() real ext-real Element of REAL
{x0} is V69() V70() V71() set
(dom (f (#) r)) \ {x0} is Element of K6((dom (f (#) r)))
K6((dom (f (#) r))) is set
g is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
lim g is V11() real ext-real Element of REAL
rng g is V69() V70() V71() set
(f (#) r) /* g is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
dom r is set
(dom r) \ {x0} is Element of K6((dom r))
K6((dom r)) is set
r /* g is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
f (#) (r /* g) is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
dom (f (#) r) is set
g is V11() real ext-real Element of REAL
k is V11() real ext-real Element of REAL
dom r is set
n is V11() real ext-real Element of REAL
g2 is V11() real ext-real Element of REAL
{x0} is V69() V70() V71() set
(dom (f (#) r)) \ {x0} is Element of K6((dom (f (#) r)))
K6((dom (f (#) r))) is set
g is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
lim g is V11() real ext-real Element of REAL
rng g is V69() V70() V71() set
(f (#) r) /* g is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
dom r is set
(dom r) \ {x0} is Element of K6((dom r))
K6((dom r)) is set
r /* g is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
f (#) (r /* g) is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
dom (f (#) r) is set
g is V11() real ext-real Element of REAL
k is V11() real ext-real Element of REAL
dom r is set
n is V11() real ext-real Element of REAL
g2 is V11() real ext-real Element of REAL
{x0} is V69() V70() V71() set
(dom (f (#) r)) \ {x0} is Element of K6((dom (f (#) r)))
K6((dom (f (#) r))) is set
g is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
lim g is V11() real ext-real Element of REAL
rng g is V69() V70() V71() set
(f (#) r) /* g is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
dom r is set
(dom r) \ {x0} is Element of K6((dom r))
K6((dom r)) is set
r /* g is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
f (#) (r /* g) is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
dom (f (#) r) is set
g is V11() real ext-real Element of REAL
k is V11() real ext-real Element of REAL
dom r is set
n is V11() real ext-real Element of REAL
g2 is V11() real ext-real Element of REAL
{x0} is V69() V70() V71() set
(dom (f (#) r)) \ {x0} is Element of K6((dom (f (#) r)))
K6((dom (f (#) r))) is set
g is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
lim g is V11() real ext-real Element of REAL
rng g is V69() V70() V71() set
(f (#) r) /* g is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
dom r is set
(dom r) \ {x0} is Element of K6((dom r))
K6((dom r)) is set
r /* g is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
f (#) (r /* g) is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
x0 is V11() real ext-real Element of REAL
f is Relation-like REAL -defined REAL -valued V21() complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
abs f is Relation-like REAL -defined REAL -valued V21() complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
r is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
lim r is V11() real ext-real Element of REAL
rng r is V69() V70() V71() set
dom (abs f) is set
{x0} is V69() V70() V71() set
(dom (abs f)) \ {x0} is Element of K6((dom (abs f)))
K6((dom (abs f))) is set
dom f is set
(dom f) \ {x0} is Element of K6((dom f))
K6((dom f)) is set
f /* r is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
abs (f /* r) is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(abs f) /* r is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
r is V11() real ext-real Element of REAL
g is V11() real ext-real Element of REAL
k is V11() real ext-real Element of REAL
n is V11() real ext-real Element of REAL
g2 is V11() real ext-real Element of REAL
c8 is V11() real ext-real Element of REAL
r is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
lim r is V11() real ext-real Element of REAL
rng r is V69() V70() V71() set
dom (abs f) is set
{x0} is V69() V70() V71() set
(dom (abs f)) \ {x0} is Element of K6((dom (abs f)))
K6((dom (abs f))) is set
dom f is set
(dom f) \ {x0} is Element of K6((dom f))
K6((dom f)) is set
f /* r is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
abs (f /* r) is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(abs f) /* r is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
r is V11() real ext-real Element of REAL
g is V11() real ext-real Element of REAL
k is V11() real ext-real Element of REAL
n is V11() real ext-real Element of REAL
g2 is V11() real ext-real Element of REAL
c8 is V11() real ext-real Element of REAL
x0 is V11() real ext-real Element of REAL
f is Relation-like REAL -defined REAL -valued V21() complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
dom f is set
r is V11() real ext-real Element of REAL
x0 - r is V11() real ext-real Element of REAL
].(x0 - r),x0.[ is V69() V70() V71() Element of K6(REAL)
f | ].(x0 - r),x0.[ is Relation-like REAL -defined REAL -valued V21() complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
x0 + r is V11() real ext-real Element of REAL
].x0,(x0 + r).[ is V69() V70() V71() Element of K6(REAL)
f | ].x0,(x0 + r).[ is Relation-like REAL -defined REAL -valued V21() complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
g is V11() real ext-real Element of REAL
g is V11() real ext-real Element of REAL
r is V11() real ext-real Element of REAL
f is Relation-like REAL -defined REAL -valued V21() complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
x0 is V11() real ext-real Element of REAL
x0 - r is V11() real ext-real Element of REAL
].(x0 - r),x0.[ is V69() V70() V71() Element of K6(REAL)
f | ].(x0 - r),x0.[ is Relation-like REAL -defined REAL -valued V21() complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
x0 + r is V11() real ext-real Element of REAL
].x0,(x0 + r).[ is V69() V70() V71() Element of K6(REAL)
f | ].x0,(x0 + r).[ is Relation-like REAL -defined REAL -valued V21() complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
dom f is set
x0 is V11() real ext-real Element of REAL
f is Relation-like REAL -defined REAL -valued V21() complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
dom f is set
r is V11() real ext-real Element of REAL
x0 - r is V11() real ext-real Element of REAL
].(x0 - r),x0.[ is V69() V70() V71() Element of K6(REAL)
f | ].(x0 - r),x0.[ is Relation-like REAL -defined REAL -valued V21() complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
x0 + r is V11() real ext-real Element of REAL
].x0,(x0 + r).[ is V69() V70() V71() Element of K6(REAL)
f | ].x0,(x0 + r).[ is Relation-like REAL -defined REAL -valued V21() complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
g is V11() real ext-real Element of REAL
g is V11() real ext-real Element of REAL
r is V11() real ext-real Element of REAL
f is Relation-like REAL -defined REAL -valued V21() complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
x0 is V11() real ext-real Element of REAL
x0 - r is V11() real ext-real Element of REAL
].(x0 - r),x0.[ is V69() V70() V71() Element of K6(REAL)
f | ].(x0 - r),x0.[ is Relation-like REAL -defined REAL -valued V21() complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
x0 + r is V11() real ext-real Element of REAL
].x0,(x0 + r).[ is V69() V70() V71() Element of K6(REAL)
f | ].x0,(x0 + r).[ is Relation-like REAL -defined REAL -valued V21() complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
dom f is set
x0 is V11() real ext-real Element of REAL
f is Relation-like REAL -defined REAL -valued V21() complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
dom f is set
r is Relation-like REAL -defined REAL -valued V21() complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
dom r is set
g is V11() real ext-real Element of REAL
x0 - g is V11() real ext-real Element of REAL
].(x0 - g),x0.[ is V69() V70() V71() Element of K6(REAL)
x0 + g is V11() real ext-real Element of REAL
].x0,(x0 + g).[ is V69() V70() V71() Element of K6(REAL)
].(x0 - g),x0.[ \/ ].x0,(x0 + g).[ is V69() V70() V71() Element of K6(REAL)
(dom r) /\ (].(x0 - g),x0.[ \/ ].x0,(x0 + g).[) is V69() V70() V71() Element of K6(REAL)
(dom f) /\ (].(x0 - g),x0.[ \/ ].x0,(x0 + g).[) is V69() V70() V71() Element of K6(REAL)
k is V11() real ext-real Element of REAL
n is V11() real ext-real Element of REAL
{x0} is V69() V70() V71() set
(dom r) \ {x0} is Element of K6((dom r))
K6((dom r)) is set
k is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
lim k is V11() real ext-real Element of REAL
rng k is V69() V70() V71() set
r /* k is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
k ^\ n is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued subsequence of k
rng (k ^\ n) is V69() V70() V71() set
g2 is set
c8 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
(k ^\ n) . c8 is V11() real ext-real Element of REAL
c8 + n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
k . (c8 + n) is V11() real ext-real Element of REAL
{ b1 where b1 is V11() real ext-real Element of REAL : ( not b1 <= x0 - g & not x0 + g <= b1 ) } is set
].(x0 - g),(x0 + g).[ is V69() V70() V71() Element of K6(REAL)
].(x0 - g),(x0 + g).[ \ {x0} is V69() V70() V71() Element of K6(REAL)
g2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
(k ^\ n) . g2 is V11() real ext-real Element of REAL
f . ((k ^\ n) . g2) is V11() real ext-real Element of REAL
r . ((k ^\ n) . g2) is V11() real ext-real Element of REAL
f /* (k ^\ n) is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(f /* (k ^\ n)) . g2 is V11() real ext-real Element of REAL
r /* (k ^\ n) is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(r /* (k ^\ n)) . g2 is V11() real ext-real Element of REAL
g2 is set
(dom f) \ {x0} is Element of K6((dom f))
K6((dom f)) is set
lim (k ^\ n) is V11() real ext-real Element of REAL
(r /* k) ^\ n is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued subsequence of r /* k
x0 is V11() real ext-real Element of REAL
f is Relation-like REAL -defined REAL -valued V21() complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
dom f is set
r is Relation-like REAL -defined REAL -valued V21() complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
dom r is set
g is V11() real ext-real Element of REAL
x0 - g is V11() real ext-real Element of REAL
].(x0 - g),x0.[ is V69() V70() V71() Element of K6(REAL)
x0 + g is V11() real ext-real Element of REAL
].x0,(x0 + g).[ is V69() V70() V71() Element of K6(REAL)
].(x0 - g),x0.[ \/ ].x0,(x0 + g).[ is V69() V70() V71() Element of K6(REAL)
(dom r) /\ (].(x0 - g),x0.[ \/ ].x0,(x0 + g).[) is V69() V70() V71() Element of K6(REAL)
(dom f) /\ (].(x0 - g),x0.[ \/ ].x0,(x0 + g).[) is V69() V70() V71() Element of K6(REAL)
k is V11() real ext-real Element of REAL
n is V11() real ext-real Element of REAL
{x0} is V69() V70() V71() set
(dom r) \ {x0} is Element of K6((dom r))
K6((dom r)) is set
k is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
lim k is V11() real ext-real Element of REAL
rng k is V69() V70() V71() set
r /* k is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
k ^\ n is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued subsequence of k
rng (k ^\ n) is V69() V70() V71() set
g2 is set
c8 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
(k ^\ n) . c8 is V11() real ext-real Element of REAL
c8 + n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
k . (c8 + n) is V11() real ext-real Element of REAL
{ b1 where b1 is V11() real ext-real Element of REAL : ( not b1 <= x0 - g & not x0 + g <= b1 ) } is set
].(x0 - g),(x0 + g).[ is V69() V70() V71() Element of K6(REAL)
].(x0 - g),(x0 + g).[ \ {x0} is V69() V70() V71() Element of K6(REAL)
g2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
(k ^\ n) . g2 is V11() real ext-real Element of REAL
r . ((k ^\ n) . g2) is V11() real ext-real Element of REAL
f . ((k ^\ n) . g2) is V11() real ext-real Element of REAL
r /* (k ^\ n) is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(r /* (k ^\ n)) . g2 is V11() real ext-real Element of REAL
f /* (k ^\ n) is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(f /* (k ^\ n)) . g2 is V11() real ext-real Element of REAL
g2 is set
(dom f) \ {x0} is Element of K6((dom f))
K6((dom f)) is set
lim (k ^\ n) is V11() real ext-real Element of REAL
(r /* k) ^\ n is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued subsequence of r /* k
x0 is V11() real ext-real Element of REAL
f is Relation-like REAL -defined REAL -valued V21() complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
dom f is set
r is Relation-like REAL -defined REAL -valued V21() complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
dom r is set
(dom r) /\ (dom f) is set
g is V11() real ext-real Element of REAL
x0 - g is V11() real ext-real Element of REAL
].(x0 - g),x0.[ is V69() V70() V71() Element of K6(REAL)
x0 + g is V11() real ext-real Element of REAL
].x0,(x0 + g).[ is V69() V70() V71() Element of K6(REAL)
].(x0 - g),x0.[ \/ ].x0,(x0 + g).[ is V69() V70() V71() Element of K6(REAL)
(dom r) /\ (].(x0 - g),x0.[ \/ ].x0,(x0 + g).[) is V69() V70() V71() Element of K6(REAL)
(dom f) /\ (].(x0 - g),x0.[ \/ ].x0,(x0 + g).[) is V69() V70() V71() Element of K6(REAL)
k is V11() real ext-real Element of REAL
n is V11() real ext-real Element of REAL
x0 is V11() real ext-real Element of REAL
f is Relation-like REAL -defined REAL -valued V21() complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
dom f is set
r is Relation-like REAL -defined REAL -valued V21() complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
dom r is set
(dom r) /\ (dom f) is set
g is V11() real ext-real Element of REAL
x0 - g is V11() real ext-real Element of REAL
].(x0 - g),x0.[ is V69() V70() V71() Element of K6(REAL)
x0 + g is V11() real ext-real Element of REAL
].x0,(x0 + g).[ is V69() V70() V71() Element of K6(REAL)
].(x0 - g),x0.[ \/ ].x0,(x0 + g).[ is V69() V70() V71() Element of K6(REAL)
(dom r) /\ (].(x0 - g),x0.[ \/ ].x0,(x0 + g).[) is V69() V70() V71() Element of K6(REAL)
(dom f) /\ (].(x0 - g),x0.[ \/ ].x0,(x0 + g).[) is V69() V70() V71() Element of K6(REAL)
k is V11() real ext-real Element of REAL
n is V11() real ext-real Element of REAL
x0 is Relation-like REAL -defined REAL -valued V21() complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
f is V11() real ext-real Element of REAL
dom x0 is set
{f} is V69() V70() V71() set
(dom x0) \ {f} is Element of K6((dom x0))
K6((dom x0)) is set
f + 1 is V11() real ext-real Element of REAL
f + 0 is V11() real ext-real Element of REAL
r is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
r + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
1 / (r + 1) is V11() real ext-real non negative Element of REAL
f - (1 / (r + 1)) is V11() real ext-real Element of REAL
g is V11() real ext-real Element of REAL
k is V11() real ext-real Element of REAL
n is V11() real ext-real Element of REAL
r is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
rng r is V69() V70() V71() set
lim r is V11() real ext-real Element of REAL
g is V11() real ext-real Element of REAL
k is V11() real ext-real Element of REAL
x0 /* r is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
lim (x0 /* r) is V11() real ext-real Element of REAL
x0 is V11() real ext-real Element of REAL
f is V11() real ext-real Element of REAL
r is Relation-like REAL -defined REAL -valued V21() complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
(r,x0) is V11() real ext-real Element of REAL
dom r is set
g is V11() real ext-real Element of REAL
g is V11() real ext-real Element of REAL
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
k + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
1 / (k + 1) is V11() real ext-real non negative Element of REAL
k is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
rng k is V69() V70() V71() set
{x0} is V69() V70() V71() set
(dom r) \ {x0} is Element of K6((dom r))
K6((dom r)) is set
lim k is V11() real ext-real Element of REAL
r /* k is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
lim (r /* k) is V11() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
(r /* k) . n is V11() real ext-real Element of REAL
((r /* k) . n) - f is V11() real ext-real Element of REAL
abs (((r /* k) . n) - f) is V11() real ext-real Element of REAL
k . n is V11() real ext-real Element of REAL
r . (k . n) is V11() real ext-real Element of REAL
(r . (k . n)) - f is V11() real ext-real Element of REAL
abs ((r . (k . n)) - f) is V11() real ext-real Element of REAL
g is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
lim g is V11() real ext-real Element of REAL
rng g is V69() V70() V71() set
{x0} is V69() V70() V71() set
(dom r) \ {x0} is Element of K6((dom r))
K6((dom r)) is set
k is V11() real ext-real set
n is V11() real ext-real Element of REAL
g2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
c8 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
g . n is V11() real ext-real Element of REAL
x0 - (g . n) is V11() real ext-real Element of REAL
abs (x0 - (g . n)) is V11() real ext-real Element of REAL
r . (g . n) is V11() real ext-real Element of REAL
(r . (g . n)) - f is V11() real ext-real Element of REAL
abs ((r . (g . n)) - f) is V11() real ext-real Element of REAL
r /* g is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(r /* g) . n is V11() real ext-real Element of REAL
((r /* g) . n) - f is V11() real ext-real Element of REAL
abs (((r /* g) . n) - f) is V11() real ext-real Element of REAL
lim (r /* g) is V11() real ext-real Element of REAL
x0 is V11() real ext-real Element of REAL
f is Relation-like REAL -defined REAL -valued V21() complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
lim_left (f,x0) is V11() real ext-real Element of REAL
lim_right (f,x0) is V11() real ext-real Element of REAL
(f,x0) is V11() real ext-real Element of REAL
r is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
lim r is V11() real ext-real Element of REAL
rng r is V69() V70() V71() set
dom f is set
right_open_halfline x0 is V69() V70() V71() Element of K6(REAL)
K195(x0,+infty) is set
(dom f) /\ (right_open_halfline x0) is V69() V70() V71() Element of K6(REAL)
{x0} is V69() V70() V71() set
(dom f) \ {x0} is Element of K6((dom f))
K6((dom f)) is set
f /* r is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
lim (f /* r) is V11() real ext-real Element of REAL
r is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
lim r is V11() real ext-real Element of REAL
rng r is V69() V70() V71() set
left_open_halfline x0 is V69() V70() V71() Element of K6(REAL)
K195(-infty,x0) is set
(dom f) /\ (left_open_halfline x0) is V69() V70() V71() Element of K6(REAL)
f /* r is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
lim (f /* r) is V11() real ext-real Element of REAL
r is V11() real ext-real Element of REAL
g is V11() real ext-real Element of REAL
r is V11() real ext-real Element of REAL
r is V11() real ext-real Element of REAL
x0 is V11() real ext-real Element of REAL
f is Relation-like REAL -defined REAL -valued V21() complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
lim_left (f,x0) is V11() real ext-real Element of REAL
lim_right (f,x0) is V11() real ext-real Element of REAL
(f,x0) is V11() real ext-real Element of REAL
r is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
lim r is V11() real ext-real Element of REAL
rng r is V69() V70() V71() set
dom f is set
{x0} is V69() V70() V71() set
(dom f) \ {x0} is Element of K6((dom f))
K6((dom f)) is set
g is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
g is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
r ^\ g is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued subsequence of r
rng (r ^\ g) is V69() V70() V71() set
left_open_halfline x0 is V69() V70() V71() Element of K6(REAL)
K195(-infty,x0) is set
(dom f) /\ (left_open_halfline x0) is V69() V70() V71() Element of K6(REAL)
k is set
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
(r ^\ g) . n is V11() real ext-real Element of REAL
n + g is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
r . (n + g) is V11() real ext-real Element of REAL
{ b1 where b1 is V11() real ext-real Element of REAL : not x0 <= b1 } is set
f /* (r ^\ g) is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
f /* r is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(f /* r) ^\ g is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued subsequence of f /* r
lim (r ^\ g) is V11() real ext-real Element of REAL
lim (f /* (r ^\ g)) is V11() real ext-real Element of REAL
lim (f /* r) is V11() real ext-real Element of REAL
g is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
g is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
r ^\ g is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued subsequence of r
rng (r ^\ g) is V69() V70() V71() set
right_open_halfline x0 is V69() V70() V71() Element of K6(REAL)
K195(x0,+infty) is set
(dom f) /\ (right_open_halfline x0) is V69() V70() V71() Element of K6(REAL)
k is set
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
(r ^\ g) . n is V11() real ext-real Element of REAL
n + g is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
r . (n + g) is V11() real ext-real Element of REAL
{ b1 where b1 is V11() real ext-real Element of REAL : not b1 <= x0 } is set
f /* (r ^\ g) is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
f /* r is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(f /* r) ^\ g is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued subsequence of f /* r
lim (r ^\ g) is V11() real ext-real Element of REAL
lim (f /* (r ^\ g)) is V11() real ext-real Element of REAL
lim (f /* r) is V11() real ext-real Element of REAL
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
r . n is V11() real ext-real Element of REAL
g2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
r . g2 is V11() real ext-real Element of REAL
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
r . k is V11() real ext-real Element of REAL
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
r . k is V11() real ext-real Element of REAL
g2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
g2 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
c8 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
r . c8 is V11() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
r . n is V11() real ext-real Element of REAL
g2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
c8 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
r . n is V11() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
r . n is V11() real ext-real Element of REAL
N is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
N9 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
r . N9 is V11() real ext-real Element of REAL
G is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
r . G is V11() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
g2 is non empty Relation-like NAT -defined NAT -valued V21() total quasi_total complex-valued ext-real-valued real-valued natural-valued Element of K6(K7(NAT,NAT))
g2 . 0 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
rng g2 is V69() V70() V71() V72() V73() V74() set
dom g2 is V69() V70() V71() V72() V73() V74() set
c8 is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
c8 . n is V11() real ext-real Element of REAL
rng c8 is V69() V70() V71() set
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
n + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
c8 . (n + 1) is V11() real ext-real Element of REAL
c8 . n is V11() real ext-real Element of REAL
n is non empty Relation-like NAT -defined NAT -valued V21() total quasi_total complex-valued ext-real-valued real-valued natural-valued increasing non-decreasing Element of K6(K7(NAT,NAT))
r * n is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
rng (r * n) is V69() V70() V71() set
N is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
r . N is V11() real ext-real Element of REAL
N is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
r . N is V11() real ext-real Element of REAL
n . 0 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
N9 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
r . N9 is V11() real ext-real Element of REAL
G is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
n . G is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
N9 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
r . N9 is V11() real ext-real Element of REAL
G is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
r . G is V11() real ext-real Element of REAL
G is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
n . G is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
G is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
n . G is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
G is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
n . G is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
G is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
n . G is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
G is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
n . G is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
G + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
n . (G + 1) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
G is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
n . G is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
r . (n . (G + 1)) is V11() real ext-real Element of REAL
N is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
N9 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
r . N9 is V11() real ext-real Element of REAL
G is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
r . G is V11() real ext-real Element of REAL
N is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
r . N is V11() real ext-real Element of REAL
N is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
r . N is V11() real ext-real Element of REAL
N9 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
(r * n) . N9 is V11() real ext-real Element of REAL
N9 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
(r * n) . (N9 + 1) is V11() real ext-real Element of REAL
n . N9 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
n . (N9 + 1) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
G is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
G is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
r . G is V11() real ext-real Element of REAL
G is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
r . G is V11() real ext-real Element of REAL
r . (n . (N9 + 1)) is V11() real ext-real Element of REAL
(r * n) . 0 is V11() real ext-real Element of REAL
left_open_halfline x0 is V69() V70() V71() Element of K6(REAL)
K195(-infty,x0) is set
(dom f) /\ (left_open_halfline x0) is V69() V70() V71() Element of K6(REAL)
N9 is set
G is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
(r * n) . G is V11() real ext-real Element of REAL
{ b1 where b1 is V11() real ext-real Element of REAL : not x0 <= b1 } is set
G is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
G + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
G is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
r . G is V11() real ext-real Element of REAL
G is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
r . G is V11() real ext-real Element of REAL
G is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
G is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
G is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
r . G is V11() real ext-real Element of REAL
G is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
r . G is V11() real ext-real Element of REAL
r is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
n1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
r . n1 is V11() real ext-real Element of REAL
n2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
r . n2 is V11() real ext-real Element of REAL
N9 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
G is non empty Relation-like NAT -defined NAT -valued V21() total quasi_total complex-valued ext-real-valued real-valued natural-valued Element of K6(K7(NAT,NAT))
G . 0 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
rng G is V69() V70() V71() V72() V73() V74() set
dom G is V69() V70() V71() V72() V73() V74() set
G is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
G is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
G . G is V11() real ext-real Element of REAL
rng G is V69() V70() V71() set
G is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
G + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
G . (G + 1) is V11() real ext-real Element of REAL
G . G is V11() real ext-real Element of REAL
G is non empty Relation-like NAT -defined NAT -valued V21() total quasi_total complex-valued ext-real-valued real-valued natural-valued increasing non-decreasing Element of K6(K7(NAT,NAT))
r * G is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
rng (r * G) is V69() V70() V71() set
lim (r * n) is V11() real ext-real Element of REAL
f /* (r * n) is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
lim (f /* (r * n)) is V11() real ext-real Element of REAL
r is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
r . r is V11() real ext-real Element of REAL
r is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
r . r is V11() real ext-real Element of REAL
G . 0 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
n1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
r . n1 is V11() real ext-real Element of REAL
n2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
G . n2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
n1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
r . n1 is V11() real ext-real Element of REAL
n2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
r . n2 is V11() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
G . n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
G . k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
G . n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
n2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
G . n2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
n2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
G . n2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
n2 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
G . (n2 + 1) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
G . n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
r . (G . (n2 + 1)) is V11() real ext-real Element of REAL
r is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
(r * G) . r is V11() real ext-real Element of REAL
r + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
(r * G) . (r + 1) is V11() real ext-real Element of REAL
G . r is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
G . (r + 1) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
n1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
n2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
r . n2 is V11() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
r . n is V11() real ext-real Element of REAL
r . (G . (r + 1)) is V11() real ext-real Element of REAL
(r * G) . 0 is V11() real ext-real Element of REAL
right_open_halfline x0 is V69() V70() V71() Element of K6(REAL)
K195(x0,+infty) is set
(dom f) /\ (right_open_halfline x0) is V69() V70() V71() Element of K6(REAL)
r is set
n1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
(r * G) . n1 is V11() real ext-real Element of REAL
{ b1 where b1 is V11() real ext-real Element of REAL : not b1 <= x0 } is set
lim (r * G) is V11() real ext-real Element of REAL
f /* (r * G) is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
lim (f /* (r * G)) is V11() real ext-real Element of REAL
r is V11() real ext-real set
n1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
n2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
n . n1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
G . n2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
max ((n . n1),(G . n2)) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
r . k is V11() real ext-real Element of REAL
l is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
n . l is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
(f /* (r * n)) . l is V11() real ext-real Element of REAL
((f /* (r * n)) . l) - (lim_left (f,x0)) is V11() real ext-real Element of REAL
abs (((f /* (r * n)) . l) - (lim_left (f,x0))) is V11() real ext-real Element of REAL
(r * n) . l is V11() real ext-real Element of REAL
f . ((r * n) . l) is V11() real ext-real Element of REAL
(f . ((r * n) . l)) - (lim_left (f,x0)) is V11() real ext-real Element of REAL
abs ((f . ((r * n) . l)) - (lim_left (f,x0))) is V11() real ext-real Element of REAL
f . (r . k) is V11() real ext-real Element of REAL
(f . (r . k)) - (lim_left (f,x0)) is V11() real ext-real Element of REAL
abs ((f . (r . k)) - (lim_left (f,x0))) is V11() real ext-real Element of REAL
f /* r is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(f /* r) . k is V11() real ext-real Element of REAL
((f /* r) . k) - (lim_left (f,x0)) is V11() real ext-real Element of REAL
abs (((f /* r) . k) - (lim_left (f,x0))) is V11() real ext-real Element of REAL
l is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
G . l is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
(f /* (r * G)) . l is V11() real ext-real Element of REAL
((f /* (r * G)) . l) - (lim_left (f,x0)) is V11() real ext-real Element of REAL
abs (((f /* (r * G)) . l) - (lim_left (f,x0))) is V11() real ext-real Element of REAL
(r * G) . l is V11() real ext-real Element of REAL
f . ((r * G) . l) is V11() real ext-real Element of REAL
(f . ((r * G) . l)) - (lim_left (f,x0)) is V11() real ext-real Element of REAL
abs ((f . ((r * G) . l)) - (lim_left (f,x0))) is V11() real ext-real Element of REAL
f . (r . k) is V11() real ext-real Element of REAL
(f . (r . k)) - (lim_left (f,x0)) is V11() real ext-real Element of REAL
abs ((f . (r . k)) - (lim_left (f,x0))) is V11() real ext-real Element of REAL
f /* r is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(f /* r) . k is V11() real ext-real Element of REAL
((f /* r) . k) - (lim_left (f,x0)) is V11() real ext-real Element of REAL
abs (((f /* r) . k) - (lim_left (f,x0))) is V11() real ext-real Element of REAL
f /* r is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(f /* r) . k is V11() real ext-real Element of REAL
((f /* r) . k) - (lim_left (f,x0)) is V11() real ext-real Element of REAL
abs (((f /* r) . k) - (lim_left (f,x0))) is V11() real ext-real Element of REAL
f /* r is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(f /* r) . k is V11() real ext-real Element of REAL
((f /* r) . k) - (lim_left (f,x0)) is V11() real ext-real Element of REAL
abs (((f /* r) . k) - (lim_left (f,x0))) is V11() real ext-real Element of REAL
lim (f /* r) is V11() real ext-real Element of REAL
g is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
f /* r is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
lim (f /* r) is V11() real ext-real Element of REAL
f /* r is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
lim (f /* r) is V11() real ext-real Element of REAL
g is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
f /* r is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
lim (f /* r) is V11() real ext-real Element of REAL
f /* r is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
lim (f /* r) is V11() real ext-real Element of REAL
r is V11() real ext-real Element of REAL
g is V11() real ext-real Element of REAL
k is V11() real ext-real Element of REAL
n is V11() real ext-real Element of REAL
g2 is V11() real ext-real Element of REAL
c8 is V11() real ext-real Element of REAL
x0 is V11() real ext-real Element of REAL
f is V11() real ext-real Element of REAL
r is Relation-like REAL -defined REAL -valued V21() complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
f (#) r is Relation-like REAL -defined REAL -valued V21() complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
((f (#) r),x0) is V11() real ext-real Element of REAL
(r,x0) is V11() real ext-real Element of REAL
f * (r,x0) is V11() real ext-real Element of REAL
g is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
lim g is V11() real ext-real Element of REAL
rng g is V69() V70() V71() set
dom (f (#) r) is set
{x0} is V69() V70() V71() set
(dom (f (#) r)) \ {x0} is Element of K6((dom (f (#) r)))
K6((dom (f (#) r))) is set
dom r is set
(dom r) \ {x0} is Element of K6((dom r))
K6((dom r)) is set
r /* g is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
f (#) (r /* g) is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(f (#) r) /* g is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
lim (r /* g) is V11() real ext-real Element of REAL
lim ((f (#) r) /* g) is V11() real ext-real Element of REAL
g is V11() real ext-real Element of REAL
k is V11() real ext-real Element of REAL
n is V11() real ext-real Element of REAL
g2 is V11() real ext-real Element of REAL
c8 is V11() real ext-real Element of REAL
n is V11() real ext-real Element of REAL
x0 is V11() real ext-real Element of REAL
f is Relation-like REAL -defined REAL -valued V21() complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
- f is Relation-like REAL -defined REAL -valued V21() complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
- 1 is V11() real ext-real non positive set
(- 1) (#) f is Relation-like REAL -defined V21() complex-valued ext-real-valued real-valued set
((- f),x0) is V11() real ext-real Element of REAL
(f,x0) is V11() real ext-real Element of REAL
- (f,x0) is V11() real ext-real Element of REAL
- 1 is V11() real ext-real non positive Element of REAL
(- 1) (#) f is Relation-like REAL -defined REAL -valued V21() complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
(- 1) * (f,x0) is V11() real ext-real Element of REAL
x0 is V11() real ext-real Element of REAL
f is Relation-like REAL -defined REAL -valued V21() complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
(f,x0) is V11() real ext-real Element of REAL
r is Relation-like REAL -defined REAL -valued V21() complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
f + r is Relation-like REAL -defined REAL -valued V21() complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
dom (f + r) is set
((f + r),x0) is V11() real ext-real Element of REAL
(r,x0) is V11() real ext-real Element of REAL
(f,x0) + (r,x0) is V11() real ext-real Element of REAL
g is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
lim g is V11() real ext-real Element of REAL
rng g is V69() V70() V71() set
{x0} is V69() V70() V71() set
(dom (f + r)) \ {x0} is Element of K6((dom (f + r)))
K6((dom (f + r))) is set
dom f is set
dom r is set
(dom f) /\ (dom r) is set
(dom f) \ {x0} is Element of K6((dom f))
K6((dom f)) is set
(dom r) \ {x0} is Element of K6((dom r))
K6((dom r)) is set
r /* g is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
lim (r /* g) is V11() real ext-real Element of REAL
f /* g is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(f /* g) + (r /* g) is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(f + r) /* g is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
lim (f /* g) is V11() real ext-real Element of REAL
lim ((f + r) /* g) is V11() real ext-real Element of REAL
x0 is V11() real ext-real Element of REAL
f is Relation-like REAL -defined REAL -valued V21() complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
(f,x0) is V11() real ext-real Element of REAL
r is Relation-like REAL -defined REAL -valued V21() complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
f - r is Relation-like REAL -defined REAL -valued V21() complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
- r is Relation-like REAL -defined V21() complex-valued ext-real-valued real-valued set
- 1 is V11() real ext-real non positive set
(- 1) (#) r is Relation-like REAL -defined V21() complex-valued ext-real-valued real-valued set
f + (- r) is Relation-like REAL -defined V21() complex-valued ext-real-valued real-valued set
dom (f - r) is set
((f - r),x0) is V11() real ext-real Element of REAL
(r,x0) is V11() real ext-real Element of REAL
(f,x0) - (r,x0) is V11() real ext-real Element of REAL
- r is Relation-like REAL -defined REAL -valued V21() complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
((- r),x0) is V11() real ext-real Element of REAL
(f,x0) + ((- r),x0) is V11() real ext-real Element of REAL
- (r,x0) is V11() real ext-real Element of REAL
(f,x0) + (- (r,x0)) is V11() real ext-real Element of REAL
x0 is V11() real ext-real Element of REAL
f is Relation-like REAL -defined REAL -valued V21() complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
f " {0} is set
(f,x0) is V11() real ext-real Element of REAL
f ^ is Relation-like REAL -defined REAL -valued V21() complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
((f ^),x0) is V11() real ext-real Element of REAL
(f,x0) " is V11() real ext-real Element of REAL
dom f is set
(dom f) \ (f " {0}) is Element of K6((dom f))
K6((dom f)) is set
dom (f ^) is set
r is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
lim r is V11() real ext-real Element of REAL
rng r is V69() V70() V71() set
{x0} is V69() V70() V71() set
(dom (f ^)) \ {x0} is Element of K6((dom (f ^)))
K6((dom (f ^))) is set
f /* r is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
lim (f /* r) is V11() real ext-real Element of REAL
(f /* r) " is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(f ^) /* r is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
lim ((f ^) /* r) is V11() real ext-real Element of REAL
r is V11() real ext-real Element of REAL
g is V11() real ext-real Element of REAL
x0 is V11() real ext-real Element of REAL
f is Relation-like REAL -defined REAL -valued V21() complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
abs f is Relation-like REAL -defined REAL -valued V21() complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
((abs f),x0) is V11() real ext-real Element of REAL
(f,x0) is V11() real ext-real Element of REAL
abs (f,x0) is V11() real ext-real Element of REAL
r is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
lim r is V11() real ext-real Element of REAL
rng r is V69() V70() V71() set
dom (abs f) is set
{x0} is V69() V70() V71() set
(dom (abs f)) \ {x0} is Element of K6((dom (abs f)))
K6((dom (abs f))) is set
dom f is set
(dom f) \ {x0} is Element of K6((dom f))
K6((dom f)) is set
f /* r is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
abs (f /* r) is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(abs f) /* r is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
lim (f /* r) is V11() real ext-real Element of REAL
lim ((abs f) /* r) is V11() real ext-real Element of REAL
r is V11() real ext-real Element of REAL
g is V11() real ext-real Element of REAL
k is V11() real ext-real Element of REAL
n is V11() real ext-real Element of REAL
g2 is V11() real ext-real Element of REAL
c8 is V11() real ext-real Element of REAL
x0 is V11() real ext-real Element of REAL
f is Relation-like REAL -defined REAL -valued V21() complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
(f,x0) is V11() real ext-real Element of REAL
dom f is set
f ^ is Relation-like REAL -defined REAL -valued V21() complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
((f ^),x0) is V11() real ext-real Element of REAL
(f,x0) " is V11() real ext-real Element of REAL
f " {0} is set
(dom f) \ (f " {0}) is Element of K6((dom f))
K6((dom f)) is set
dom (f ^) is set
r is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
lim r is V11() real ext-real Element of REAL
rng r is V69() V70() V71() set
{x0} is V69() V70() V71() set
(dom (f ^)) \ {x0} is Element of K6((dom (f ^)))
K6((dom (f ^))) is set
f /* r is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
g is set
(dom f) \ {x0} is Element of K6((dom f))
lim (f /* r) is V11() real ext-real Element of REAL
(f /* r) " is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(f ^) /* r is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
lim ((f ^) /* r) is V11() real ext-real Element of REAL
r is V11() real ext-real Element of REAL
g is V11() real ext-real Element of REAL
k is V11() real ext-real Element of REAL
n is V11() real ext-real Element of REAL
f . k is V11() real ext-real Element of REAL
f . n is V11() real ext-real Element of REAL
c8 is V11() real ext-real Element of REAL
f . c8 is V11() real ext-real Element of REAL
g2 is V11() real ext-real Element of REAL
f . g2 is V11() real ext-real Element of REAL
x0 is V11() real ext-real Element of REAL
f is Relation-like REAL -defined REAL -valued V21() complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
(f,x0) is V11() real ext-real Element of REAL
r is Relation-like REAL -defined REAL -valued V21() complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
f (#) r is Relation-like REAL -defined REAL -valued V21() complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
dom (f (#) r) is set
((f (#) r),x0) is V11() real ext-real Element of REAL
(r,x0) is V11() real ext-real Element of REAL
(f,x0) * (r,x0) is V11() real ext-real Element of REAL
g is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
lim g is V11() real ext-real Element of REAL
rng g is V69() V70() V71() set
{x0} is V69() V70() V71() set
(dom (f (#) r)) \ {x0} is Element of K6((dom (f (#) r)))
K6((dom (f (#) r))) is set
dom f is set
dom r is set
(dom f) /\ (dom r) is set
(dom f) \ {x0} is Element of K6((dom f))
K6((dom f)) is set
(dom r) \ {x0} is Element of K6((dom r))
K6((dom r)) is set
r /* g is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
lim (r /* g) is V11() real ext-real Element of REAL
f /* g is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(f /* g) (#) (r /* g) is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(f (#) r) /* g is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
lim (f /* g) is V11() real ext-real Element of REAL
lim ((f (#) r) /* g) is V11() real ext-real Element of REAL
x0 is V11() real ext-real Element of REAL
f is Relation-like REAL -defined REAL -valued V21() complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
(f,x0) is V11() real ext-real Element of REAL
r is Relation-like REAL -defined REAL -valued V21() complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
(r,x0) is V11() real ext-real Element of REAL
f / r is Relation-like REAL -defined REAL -valued V21() complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
dom (f / r) is set
((f / r),x0) is V11() real ext-real Element of REAL
(f,x0) / (r,x0) is V11() real ext-real Element of REAL
g is V11() real ext-real Element of REAL
k is V11() real ext-real Element of REAL
n is V11() real ext-real Element of REAL
g2 is V11() real ext-real Element of REAL
c8 is V11() real ext-real Element of REAL
dom r is set
dom f is set
r " {0} is set
(dom r) \ (r " {0}) is Element of K6((dom r))
K6((dom r)) is set
(dom f) /\ ((dom r) \ (r " {0})) is Element of K6((dom r))
n is V11() real ext-real Element of REAL
r . n is V11() real ext-real Element of REAL
r . c8 is V11() real ext-real Element of REAL
r ^ is Relation-like REAL -defined REAL -valued V21() complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
f (#) (r ^) is Relation-like REAL -defined REAL -valued V21() complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
((r ^),x0) is V11() real ext-real Element of REAL
(r,x0) " is V11() real ext-real Element of REAL
(f,x0) * ((r,x0) ") is V11() real ext-real Element of REAL
x0 is V11() real ext-real Element of REAL
f is Relation-like REAL -defined REAL -valued V21() complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
(f,x0) is V11() real ext-real Element of REAL
r is Relation-like REAL -defined REAL -valued V21() complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
f (#) r is Relation-like REAL -defined REAL -valued V21() complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
dom (f (#) r) is set
((f (#) r),x0) is V11() real ext-real Element of REAL
g is V11() real ext-real Element of REAL
x0 - g is V11() real ext-real Element of REAL
].(x0 - g),x0.[ is V69() V70() V71() Element of K6(REAL)
x0 + g is V11() real ext-real Element of REAL
].x0,(x0 + g).[ is V69() V70() V71() Element of K6(REAL)
].(x0 - g),x0.[ \/ ].x0,(x0 + g).[ is V69() V70() V71() Element of K6(REAL)
r | (].(x0 - g),x0.[ \/ ].x0,(x0 + g).[) is Relation-like REAL -defined REAL -valued V21() complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
dom r is set
(].(x0 - g),x0.[ \/ ].x0,(x0 + g).[) /\ (dom r) is V69() V70() V71() Element of K6(REAL)
k is V11() real ext-real set
n is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
lim n is V11() real ext-real Element of REAL
rng n is V69() V70() V71() set
{x0} is V69() V70() V71() set
(dom (f (#) r)) \ {x0} is Element of K6((dom (f (#) r)))
K6((dom (f (#) r))) is set
g2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
n ^\ g2 is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued subsequence of n
rng (n ^\ g2) is V69() V70() V71() set
dom f is set
(dom f) \ {x0} is Element of K6((dom f))
K6((dom f)) is set
lim (n ^\ g2) is V11() real ext-real Element of REAL
f /* (n ^\ g2) is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
abs k is V11() real ext-real Element of REAL
(abs k) + 1 is V11() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
n + g2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
n . (n + g2) is V11() real ext-real Element of REAL
(n ^\ g2) . n is V11() real ext-real Element of REAL
{ b1 where b1 is V11() real ext-real Element of REAL : ( not b1 <= x0 - g & not x0 + g <= b1 ) } is set
].(x0 - g),(x0 + g).[ is V69() V70() V71() Element of K6(REAL)
].(x0 - g),(x0 + g).[ \ {x0} is V69() V70() V71() Element of K6(REAL)
r . ((n ^\ g2) . n) is V11() real ext-real Element of REAL
abs (r . ((n ^\ g2) . n)) is V11() real ext-real Element of REAL
r /* (n ^\ g2) is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(r /* (n ^\ g2)) . n is V11() real ext-real Element of REAL
abs ((r /* (n ^\ g2)) . n) is V11() real ext-real Element of REAL
(dom f) /\ (dom r) is set
(f /* (n ^\ g2)) (#) (r /* (n ^\ g2)) is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(f (#) r) /* (n ^\ g2) is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(f (#) r) /* n is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
((f (#) r) /* n) ^\ g2 is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued subsequence of (f (#) r) /* n
lim (f /* (n ^\ g2)) is V11() real ext-real Element of REAL
lim ((f /* (n ^\ g2)) (#) (r /* (n ^\ g2))) is V11() real ext-real Element of REAL
lim ((f (#) r) /* n) is V11() real ext-real Element of REAL
x0 is V11() real ext-real Element of REAL
f is Relation-like REAL -defined REAL -valued V21() complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
(f,x0) is V11() real ext-real Element of REAL
dom f is set
r is Relation-like REAL -defined REAL -valued V21() complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
(r,x0) is V11() real ext-real Element of REAL
dom r is set
g is Relation-like REAL -defined REAL -valued V21() complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
dom g is set
(g,x0) is V11() real ext-real Element of REAL
k is V11() real ext-real Element of REAL
x0 - k is V11() real ext-real Element of REAL
].(x0 - k),x0.[ is V69() V70() V71() Element of K6(REAL)
x0 + k is V11() real ext-real Element of REAL
].x0,(x0 + k).[ is V69() V70() V71() Element of K6(REAL)
].(x0 - k),x0.[ \/ ].x0,(x0 + k).[ is V69() V70() V71() Element of K6(REAL)
(dom g) /\ (].(x0 - k),x0.[ \/ ].x0,(x0 + k).[) is V69() V70() V71() Element of K6(REAL)
(dom f) /\ (].(x0 - k),x0.[ \/ ].x0,(x0 + k).[) is V69() V70() V71() Element of K6(REAL)
(dom r) /\ (].(x0 - k),x0.[ \/ ].x0,(x0 + k).[) is V69() V70() V71() Element of K6(REAL)
n is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
lim n is V11() real ext-real Element of REAL
rng n is V69() V70() V71() set
{x0} is V69() V70() V71() set
(dom g) \ {x0} is Element of K6((dom g))
K6((dom g)) is set
g2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
n ^\ g2 is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued subsequence of n
rng (n ^\ g2) is V69() V70() V71() set
c8 is set
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
(n ^\ g2) . n is V11() real ext-real Element of REAL
n + g2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
n . (n + g2) is V11() real ext-real Element of REAL
{ b1 where b1 is V11() real ext-real Element of REAL : ( not b1 <= x0 - k & not x0 + k <= b1 ) } is set
].(x0 - k),(x0 + k).[ is V69() V70() V71() Element of K6(REAL)
].(x0 - k),(x0 + k).[ \ {x0} is V69() V70() V71() Element of K6(REAL)
lim (n ^\ g2) is V11() real ext-real Element of REAL
(dom r) \ {x0} is Element of K6((dom r))
K6((dom r)) is set
c8 is set
r /* (n ^\ g2) is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
lim (r /* (n ^\ g2)) is V11() real ext-real Element of REAL
(dom f) \ {x0} is Element of K6((dom f))
K6((dom f)) is set
c8 is set
f /* (n ^\ g2) is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
lim (f /* (n ^\ g2)) is V11() real ext-real Element of REAL
c8 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
(n ^\ g2) . c8 is V11() real ext-real Element of REAL
g . ((n ^\ g2) . c8) is V11() real ext-real Element of REAL
r . ((n ^\ g2) . c8) is V11() real ext-real Element of REAL
g /* (n ^\ g2) is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(g /* (n ^\ g2)) . c8 is V11() real ext-real Element of REAL
f . ((n ^\ g2) . c8) is V11() real ext-real Element of REAL
(f /* (n ^\ g2)) . c8 is V11() real ext-real Element of REAL
(r /* (n ^\ g2)) . c8 is V11() real ext-real Element of REAL
g /* n is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(g /* n) ^\ g2 is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued subsequence of g /* n
lim (g /* (n ^\ g2)) is V11() real ext-real Element of REAL
lim ((g /* n) ^\ g2) is V11() real ext-real Element of REAL
lim (g /* n) is V11() real ext-real Element of REAL
n is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
lim n is V11() real ext-real Element of REAL
rng n is V69() V70() V71() set
{x0} is V69() V70() V71() set
(dom g) \ {x0} is Element of K6((dom g))
K6((dom g)) is set
g2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
n ^\ g2 is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued subsequence of n
rng (n ^\ g2) is V69() V70() V71() set
c8 is set
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
(n ^\ g2) . n is V11() real ext-real Element of REAL
n + g2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
n . (n + g2) is V11() real ext-real Element of REAL
{ b1 where b1 is V11() real ext-real Element of REAL : ( not b1 <= x0 - k & not x0 + k <= b1 ) } is set
].(x0 - k),(x0 + k).[ is V69() V70() V71() Element of K6(REAL)
].(x0 - k),(x0 + k).[ \ {x0} is V69() V70() V71() Element of K6(REAL)
lim (n ^\ g2) is V11() real ext-real Element of REAL
(dom r) \ {x0} is Element of K6((dom r))
K6((dom r)) is set
c8 is set
r /* (n ^\ g2) is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
lim (r /* (n ^\ g2)) is V11() real ext-real Element of REAL
(dom f) \ {x0} is Element of K6((dom f))
K6((dom f)) is set
c8 is set
f /* (n ^\ g2) is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
lim (f /* (n ^\ g2)) is V11() real ext-real Element of REAL
c8 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
(n ^\ g2) . c8 is V11() real ext-real Element of REAL
g . ((n ^\ g2) . c8) is V11() real ext-real Element of REAL
r . ((n ^\ g2) . c8) is V11() real ext-real Element of REAL
g /* (n ^\ g2) is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(g /* (n ^\ g2)) . c8 is V11() real ext-real Element of REAL
f . ((n ^\ g2) . c8) is V11() real ext-real Element of REAL
(f /* (n ^\ g2)) . c8 is V11() real ext-real Element of REAL
(r /* (n ^\ g2)) . c8 is V11() real ext-real Element of REAL
g /* n is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(g /* n) ^\ g2 is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued subsequence of g /* n
lim (g /* (n ^\ g2)) is V11() real ext-real Element of REAL
lim ((g /* n) ^\ g2) is V11() real ext-real Element of REAL
lim (g /* n) is V11() real ext-real Element of REAL
x0 is V11() real ext-real Element of REAL
f is Relation-like REAL -defined REAL -valued V21() complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
(f,x0) is V11() real ext-real Element of REAL
dom f is set
r is Relation-like REAL -defined REAL -valued V21() complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
(r,x0) is V11() real ext-real Element of REAL
dom r is set
(dom f) /\ (dom r) is set
g is Relation-like REAL -defined REAL -valued V21() complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
dom g is set
((dom f) /\ (dom r)) /\ (dom g) is set
(g,x0) is V11() real ext-real Element of REAL
k is V11() real ext-real Element of REAL
x0 - k is V11() real ext-real Element of REAL
].(x0 - k),x0.[ is V69() V70() V71() Element of K6(REAL)
x0 + k is V11() real ext-real Element of REAL
].x0,(x0 + k).[ is V69() V70() V71() Element of K6(REAL)
].(x0 - k),x0.[ \/ ].x0,(x0 + k).[ is V69() V70() V71() Element of K6(REAL)
(dom g) /\ (].(x0 - k),x0.[ \/ ].x0,(x0 + k).[) is V69() V70() V71() Element of K6(REAL)
(dom f) /\ (].(x0 - k),x0.[ \/ ].x0,(x0 + k).[) is V69() V70() V71() Element of K6(REAL)
(dom r) /\ (].(x0 - k),x0.[ \/ ].x0,(x0 + k).[) is V69() V70() V71() Element of K6(REAL)
n is V11() real ext-real Element of REAL
g2 is V11() real ext-real Element of REAL
x0 is V11() real ext-real Element of REAL
f is Relation-like REAL -defined REAL -valued V21() complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
dom f is set
(f,x0) is V11() real ext-real Element of REAL
r is Relation-like REAL -defined REAL -valued V21() complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
dom r is set
(r,x0) is V11() real ext-real Element of REAL
g is V11() real ext-real Element of REAL
x0 - g is V11() real ext-real Element of REAL
].(x0 - g),x0.[ is V69() V70() V71() Element of K6(REAL)
x0 + g is V11() real ext-real Element of REAL
].x0,(x0 + g).[ is V69() V70() V71() Element of K6(REAL)
].(x0 - g),x0.[ \/ ].x0,(x0 + g).[ is V69() V70() V71() Element of K6(REAL)
(dom f) /\ (].(x0 - g),x0.[ \/ ].x0,(x0 + g).[) is V69() V70() V71() Element of K6(REAL)
(dom r) /\ (].(x0 - g),x0.[ \/ ].x0,(x0 + g).[) is V69() V70() V71() Element of K6(REAL)
x0 + 1 is V11() real ext-real Element of REAL
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
k + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
1 / (k + 1) is V11() real ext-real non negative Element of REAL
x0 - (1 / (k + 1)) is V11() real ext-real Element of REAL
n is V11() real ext-real Element of REAL
g2 is V11() real ext-real Element of REAL
c8 is V11() real ext-real Element of REAL
k is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
lim k is V11() real ext-real Element of REAL
rng k is V69() V70() V71() set
{x0} is V69() V70() V71() set
(dom f) \ {x0} is Element of K6((dom f))
K6((dom f)) is set
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
k ^\ n is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued subsequence of k
lim (k ^\ n) is V11() real ext-real Element of REAL
rng (k ^\ n) is V69() V70() V71() set
f /* (k ^\ n) is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
lim (f /* (k ^\ n)) is V11() real ext-real Element of REAL
g2 is set
c8 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
(k ^\ n) . c8 is V11() real ext-real Element of REAL
c8 + n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
k . (c8 + n) is V11() real ext-real Element of REAL
{ b1 where b1 is V11() real ext-real Element of REAL : ( not b1 <= x0 - g & not x0 <= b1 ) } is set
g2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
(k ^\ n) . g2 is V11() real ext-real Element of REAL
f . ((k ^\ n) . g2) is V11() real ext-real Element of REAL
r . ((k ^\ n) . g2) is V11() real ext-real Element of REAL
r /* (k ^\ n) is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(r /* (k ^\ n)) . g2 is V11() real ext-real Element of REAL
(f /* (k ^\ n)) . g2 is V11() real ext-real Element of REAL
(dom r) \ {x0} is Element of K6((dom r))
K6((dom r)) is set
g2 is set
lim (r /* (k ^\ n)) is V11() real ext-real Element of REAL
x0 + 1 is V11() real ext-real Element of REAL
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
k + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
1 / (k + 1) is V11() real ext-real non negative Element of REAL
x0 - (1 / (k + 1)) is V11() real ext-real Element of REAL
n is V11() real ext-real Element of REAL
g2 is V11() real ext-real Element of REAL
c8 is V11() real ext-real Element of REAL
k is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
lim k is V11() real ext-real Element of REAL
rng k is V69() V70() V71() set
{x0} is V69() V70() V71() set
(dom r) \ {x0} is Element of K6((dom r))
K6((dom r)) is set
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
k ^\ n is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued subsequence of k
lim (k ^\ n) is V11() real ext-real Element of REAL
rng (k ^\ n) is V69() V70() V71() set
r /* (k ^\ n) is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
lim (r /* (k ^\ n)) is V11() real ext-real Element of REAL
g2 is set
c8 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
(k ^\ n) . c8 is V11() real ext-real Element of REAL
c8 + n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
k . (c8 + n) is V11() real ext-real Element of REAL
{ b1 where b1 is V11() real ext-real Element of REAL : ( not b1 <= x0 - g & not x0 <= b1 ) } is set
g2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
(k ^\ n) . g2 is V11() real ext-real Element of REAL
f . ((k ^\ n) . g2) is V11() real ext-real Element of REAL
r . ((k ^\ n) . g2) is V11() real ext-real Element of REAL
(r /* (k ^\ n)) . g2 is V11() real ext-real Element of REAL
f /* (k ^\ n) is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(f /* (k ^\ n)) . g2 is V11() real ext-real Element of REAL
(dom f) \ {x0} is Element of K6((dom f))
K6((dom f)) is set
g2 is set
lim (f /* (k ^\ n)) is V11() real ext-real Element of REAL
k is V11() real ext-real Element of REAL
f . k is V11() real ext-real Element of REAL
r . k is V11() real ext-real Element of REAL
n is V11() real ext-real Element of REAL
f . n is V11() real ext-real Element of REAL
r . n is V11() real ext-real Element of REAL
x0 is V11() real ext-real Element of REAL
f is Relation-like REAL -defined REAL -valued V21() complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
dom f is set
f ^ is Relation-like REAL -defined REAL -valued V21() complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
((f ^),x0) is V11() real ext-real Element of REAL
f " {0} is set
(dom f) \ (f " {0}) is Element of K6((dom f))
K6((dom f)) is set
dom (f ^) is set
r is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
lim r is V11() real ext-real Element of REAL
rng r is V69() V70() V71() set
{x0} is V69() V70() V71() set
(dom (f ^)) \ {x0} is Element of K6((dom (f ^)))
K6((dom (f ^))) is set
(dom f) \ {x0} is Element of K6((dom f))
g is set
f /* r is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(f /* r) " is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
lim ((f /* r) ") is V11() real ext-real Element of REAL
(f ^) /* r is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
lim ((f ^) /* r) is V11() real ext-real Element of REAL
f /* r is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(f /* r) " is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
lim ((f /* r) ") is V11() real ext-real Element of REAL
(f ^) /* r is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
lim ((f ^) /* r) is V11() real ext-real Element of REAL
(f ^) /* r is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
lim ((f ^) /* r) is V11() real ext-real Element of REAL
(f ^) /* r is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
lim ((f ^) /* r) is V11() real ext-real Element of REAL
r is V11() real ext-real Element of REAL
g is V11() real ext-real Element of REAL
k is V11() real ext-real Element of REAL
n is V11() real ext-real Element of REAL
f . k is V11() real ext-real Element of REAL
f . n is V11() real ext-real Element of REAL
c8 is V11() real ext-real Element of REAL
f . c8 is V11() real ext-real Element of REAL
g2 is V11() real ext-real Element of REAL
f . g2 is V11() real ext-real Element of REAL
x0 is V11() real ext-real Element of REAL
f is Relation-like REAL -defined REAL -valued V21() complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
(f,x0) is V11() real ext-real Element of REAL
dom f is set
f ^ is Relation-like REAL -defined REAL -valued V21() complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
r is V11() real ext-real Element of REAL
x0 - r is V11() real ext-real Element of REAL
].(x0 - r),x0.[ is V69() V70() V71() Element of K6(REAL)
x0 + r is V11() real ext-real Element of REAL
].x0,(x0 + r).[ is V69() V70() V71() Element of K6(REAL)
].(x0 - r),x0.[ \/ ].x0,(x0 + r).[ is V69() V70() V71() Element of K6(REAL)
(dom f) /\ (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) is V69() V70() V71() Element of K6(REAL)
dom (f ^) is set
g is V11() real ext-real Element of REAL
k is V11() real ext-real Element of REAL
n is V11() real ext-real Element of REAL
g2 is V11() real ext-real Element of REAL
f . n is V11() real ext-real Element of REAL
f . g2 is V11() real ext-real Element of REAL
f " {0} is set
(dom f) \ (f " {0}) is Element of K6((dom f))
K6((dom f)) is set
{x0} is V69() V70() V71() set
(dom (f ^)) \ {x0} is Element of K6((dom (f ^)))
K6((dom (f ^))) is set
g is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
lim g is V11() real ext-real Element of REAL
rng g is V69() V70() V71() set
(f ^) /* g is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
f " {0} is set
(dom f) \ (f " {0}) is Element of K6((dom f))
K6((dom f)) is set
g ^\ k is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued subsequence of g
f /* (g ^\ k) is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(f /* (g ^\ k)) " is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
f /* g is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(f /* g) ^\ k is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued subsequence of f /* g
((f /* g) ^\ k) " is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(f /* g) " is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
((f /* g) ") ^\ k is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued subsequence of (f /* g) "
((f ^) /* g) ^\ k is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued subsequence of (f ^) /* g
rng (g ^\ k) is V69() V70() V71() set
(dom f) \ {x0} is Element of K6((dom f))
n is set
lim (g ^\ k) is V11() real ext-real Element of REAL
lim (f /* (g ^\ k)) is V11() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
n + k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
g . (n + k) is V11() real ext-real Element of REAL
(g ^\ k) . n is V11() real ext-real Element of REAL
{ b1 where b1 is V11() real ext-real Element of REAL : ( not b1 <= x0 - r & not x0 + r <= b1 ) } is set
].(x0 - r),(x0 + r).[ is V69() V70() V71() Element of K6(REAL)
].(x0 - r),(x0 + r).[ \ {x0} is V69() V70() V71() Element of K6(REAL)
f . ((g ^\ k) . n) is V11() real ext-real Element of REAL
(f /* (g ^\ k)) . n is V11() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
(f /* (g ^\ k)) . n is V11() real ext-real Element of REAL
x0 is V11() real ext-real Element of REAL
f is Relation-like REAL -defined REAL -valued V21() complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
(f,x0) is V11() real ext-real Element of REAL
dom f is set
f ^ is Relation-like REAL -defined REAL -valued V21() complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
r is V11() real ext-real Element of REAL
x0 - r is V11() real ext-real Element of REAL
].(x0 - r),x0.[ is V69() V70() V71() Element of K6(REAL)
x0 + r is V11() real ext-real Element of REAL
].x0,(x0 + r).[ is V69() V70() V71() Element of K6(REAL)
].(x0 - r),x0.[ \/ ].x0,(x0 + r).[ is V69() V70() V71() Element of K6(REAL)
(dom f) /\ (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) is V69() V70() V71() Element of K6(REAL)
dom (f ^) is set
g is V11() real ext-real Element of REAL
k is V11() real ext-real Element of REAL
n is V11() real ext-real Element of REAL
g2 is V11() real ext-real Element of REAL
f . n is V11() real ext-real Element of REAL
f . g2 is V11() real ext-real Element of REAL
f " {0} is set
(dom f) \ (f " {0}) is Element of K6((dom f))
K6((dom f)) is set
{x0} is V69() V70() V71() set
(dom (f ^)) \ {x0} is Element of K6((dom (f ^)))
K6((dom (f ^))) is set
g is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
lim g is V11() real ext-real Element of REAL
rng g is V69() V70() V71() set
(f ^) /* g is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
f " {0} is set
(dom f) \ (f " {0}) is Element of K6((dom f))
K6((dom f)) is set
g ^\ k is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued subsequence of g
f /* (g ^\ k) is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(f /* (g ^\ k)) " is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
f /* g is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(f /* g) ^\ k is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued subsequence of f /* g
((f /* g) ^\ k) " is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(f /* g) " is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
((f /* g) ") ^\ k is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued subsequence of (f /* g) "
((f ^) /* g) ^\ k is non empty Relation-like NAT -defined REAL -valued V21() total quasi_total complex-valued ext-real-valued real-valued subsequence of (f ^) /* g
rng (g ^\ k) is V69() V70() V71() set
(dom f) \ {x0} is Element of K6((dom f))
n is set
lim (g ^\ k) is V11() real ext-real Element of REAL
lim (f /* (g ^\ k)) is V11() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
n + k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
g . (n + k) is V11() real ext-real Element of REAL
(g ^\ k) . n is V11() real ext-real Element of REAL
{ b1 where b1 is V11() real ext-real Element of REAL : ( not b1 <= x0 - r & not x0 + r <= b1 ) } is set
].(x0 - r),(x0 + r).[ is V69() V70() V71() Element of K6(REAL)
].(x0 - r),(x0 + r).[ \ {x0} is V69() V70() V71() Element of K6(REAL)
f . ((g ^\ k) . n) is V11() real ext-real Element of REAL
(f /* (g ^\ k)) . n is V11() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() Element of NAT
(f /* (g ^\ k)) . n is V11() real ext-real Element of REAL
x0 is V11() real ext-real Element of REAL
f is Relation-like REAL -defined REAL -valued V21() complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
(f,x0) is V11() real ext-real Element of REAL
dom f is set
f ^ is Relation-like REAL -defined REAL -valued V21() complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
r is V11() real ext-real Element of REAL
x0 - r is V11() real ext-real Element of REAL
].(x0 - r),x0.[ is V69() V70() V71() Element of K6(REAL)
x0 + r is V11() real ext-real Element of REAL
].x0,(x0 + r).[ is V69() V70() V71() Element of K6(REAL)
].(x0 - r),x0.[ \/ ].x0,(x0 + r).[ is V69() V70() V71() Element of K6(REAL)
(dom f) /\ (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) is V69() V70() V71() Element of K6(REAL)
g is V11() real ext-real Element of REAL
(dom f) /\ ].x0,(x0 + r).[ is V69() V70() V71() Element of K6(REAL)
f . g is V11() real ext-real Element of REAL
g is V11() real ext-real Element of REAL
(dom f) /\ ].(x0 - r),x0.[ is V69() V70() V71() Element of K6(REAL)
f . g is V11() real ext-real Element of REAL
lim_right (f,x0) is V11() real ext-real Element of REAL
lim_left (f,x0) is V11() real ext-real Element of REAL
x0 is V11() real ext-real Element of REAL
f is Relation-like REAL -defined REAL -valued V21() complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
(f,x0) is V11() real ext-real Element of REAL
dom f is set
f ^ is Relation-like REAL -defined REAL -valued V21() complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
r is V11() real ext-real Element of REAL
x0 - r is V11() real ext-real Element of REAL
].(x0 - r),x0.[ is V69() V70() V71() Element of K6(REAL)
x0 + r is V11() real ext-real Element of REAL
].x0,(x0 + r).[ is V69() V70() V71() Element of K6(REAL)
].(x0 - r),x0.[ \/ ].x0,(x0 + r).[ is V69() V70() V71() Element of K6(REAL)
(dom f) /\ (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) is V69() V70() V71() Element of K6(REAL)
g is V11() real ext-real Element of REAL
(dom f) /\ ].x0,(x0 + r).[ is V69() V70() V71() Element of K6(REAL)
f . g is V11() real ext-real Element of REAL
g is V11() real ext-real Element of REAL
(dom f) /\ ].(x0 - r),x0.[ is V69() V70() V71() Element of K6(REAL)
f . g is V11() real ext-real Element of REAL
lim_right (f,x0) is V11() real ext-real Element of REAL
lim_left (f,x0) is V11() real ext-real Element of REAL