:: L_HOSPIT semantic presentation

NAT is non empty epsilon-transitive epsilon-connected ordinal V71() V72() V73() V74() V75() V76() V77() V99() V101() Element of K19(REAL)
REAL is non empty V51() V71() V72() V73() V77() V101() V102() V104() set
K19(REAL) is set
omega is non empty epsilon-transitive epsilon-connected ordinal V71() V72() V73() V74() V75() V76() V77() V99() V101() set
K19(omega) is set
K20(NAT,REAL) is V35() V36() V37() set
K19(K20(NAT,REAL)) is set
K19(K19(REAL)) is set
{} is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() real ext-real V71() V72() V73() V74() V75() V76() V77() V101() V104() set
1 is non empty set
{{},1} is non empty set
COMPLEX is non empty V51() V71() V77() set
K20(REAL,REAL) is V35() V36() V37() set
K19(K20(REAL,REAL)) is set
RAT is non empty V51() V71() V72() V73() V74() V77() set
INT is non empty V51() V71() V72() V73() V74() V75() V77() set
K19(NAT) is set
K20(COMPLEX,COMPLEX) is V35() set
K19(K20(COMPLEX,COMPLEX)) is set
K20(COMPLEX,REAL) is V35() V36() V37() set
K19(K20(COMPLEX,REAL)) is set
0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() real ext-real V71() V72() V73() V74() V75() V76() V77() V93() V94() V101() V104() Element of NAT
{0} is non empty V71() V72() V73() V74() V75() V76() V99() V101() set
-infty is non real set
+infty is non real set
f is V1() V4( REAL ) V5( REAL ) V6() V35() V36() V37() Element of K19(K20(REAL,REAL))
dom f is V71() V72() V73() Element of K19(REAL)
g is V30() real ext-real Element of REAL
x0 is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total V35() V36() V37() Element of K19(K20(NAT,REAL))
lim x0 is V30() real ext-real Element of REAL
rng x0 is V71() V72() V73() Element of K19(REAL)
{g} is non empty V71() V72() V73() set
(dom f) \ {g} is V71() V72() V73() Element of K19(REAL)
f /* x0 is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total V35() V36() V37() Element of K19(K20(NAT,REAL))
lim (f /* x0) is V30() real ext-real Element of REAL
f . g is V30() real ext-real Element of REAL
f is V1() V4( REAL ) V5( REAL ) V6() V35() V36() V37() Element of K19(K20(REAL,REAL))
dom f is V71() V72() V73() Element of K19(REAL)
g is V30() real ext-real Element of REAL
lim_right (f,g) is V30() real ext-real Element of REAL
right_open_halfline g is V71() V72() V73() Element of K19(REAL)
K195(g,+infty) is set
(dom f) /\ (right_open_halfline g) is V71() V72() V73() Element of K19(REAL)
x0 is V30() real ext-real Element of REAL
N is V30() real ext-real Element of REAL
r is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total V35() V36() V37() Element of K19(K20(NAT,REAL))
lim r is V30() real ext-real Element of REAL
rng r is V71() V72() V73() Element of K19(REAL)
f /* r is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total V35() V36() V37() Element of K19(K20(NAT,REAL))
lim (f /* r) is V30() real ext-real Element of REAL
f is V1() V4( REAL ) V5( REAL ) V6() V35() V36() V37() Element of K19(K20(REAL,REAL))
dom f is V71() V72() V73() Element of K19(REAL)
g is V30() real ext-real Element of REAL
lim_left (f,g) is V30() real ext-real Element of REAL
left_open_halfline g is V71() V72() V73() Element of K19(REAL)
K195(-infty,g) is set
(dom f) /\ (left_open_halfline g) is V71() V72() V73() Element of K19(REAL)
x0 is V30() real ext-real Element of REAL
N is V30() real ext-real Element of REAL
r is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total V35() V36() V37() Element of K19(K20(NAT,REAL))
lim r is V30() real ext-real Element of REAL
rng r is V71() V72() V73() Element of K19(REAL)
f /* r is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total V35() V36() V37() Element of K19(K20(NAT,REAL))
lim (f /* r) is V30() real ext-real Element of REAL
f is V1() V4( REAL ) V5( REAL ) V6() V35() V36() V37() Element of K19(K20(REAL,REAL))
dom f is V71() V72() V73() Element of K19(REAL)
g is V30() real ext-real Element of REAL
{g} is non empty V71() V72() V73() set
x0 is open V71() V72() V73() Neighbourhood of g
x0 \ {g} is V71() V72() V73() Element of K19(REAL)
N is V30() real ext-real set
g - N is V30() real ext-real Element of REAL
g + N is V30() real ext-real Element of REAL
].(g - N),(g + N).[ is open V71() V72() V73() V99() V100() V104() Element of K19(REAL)
].(g - N),g.[ is open V71() V72() V73() V99() V100() V104() Element of K19(REAL)
].g,(g + N).[ is open V71() V72() V73() V99() V100() V104() Element of K19(REAL)
].(g - N),g.[ \/ ].g,(g + N).[ is V71() V72() V73() Element of K19(REAL)
r is V30() real ext-real Element of REAL
d is V30() real ext-real Element of REAL
f is V1() V4( REAL ) V5( REAL ) V6() V35() V36() V37() Element of K19(K20(REAL,REAL))
dom f is V71() V72() V73() Element of K19(REAL)
g is V1() V4( REAL ) V5( REAL ) V6() V35() V36() V37() Element of K19(K20(REAL,REAL))
dom g is V71() V72() V73() Element of K19(REAL)
f / g is V1() V4( REAL ) V5( REAL ) V6() V35() V36() V37() Element of K19(K20(REAL,REAL))
dom (f / g) is V71() V72() V73() Element of K19(REAL)
x0 is V30() real ext-real Element of REAL
{x0} is non empty V71() V72() V73() set
f . x0 is V30() real ext-real Element of REAL
g . x0 is V30() real ext-real Element of REAL
N is open V71() V72() V73() Neighbourhood of x0
N \ {x0} is V71() V72() V73() Element of K19(REAL)
f `| N is V1() V4( REAL ) V5( REAL ) V6() V35() V36() V37() Element of K19(K20(REAL,REAL))
g `| N is V1() V4( REAL ) V5( REAL ) V6() V35() V36() V37() Element of K19(K20(REAL,REAL))
(f `| N) / (g `| N) is V1() V4( REAL ) V5( REAL ) V6() V35() V36() V37() Element of K19(K20(REAL,REAL))
dom ((f `| N) / (g `| N)) is V71() V72() V73() Element of K19(REAL)
r is V30() real ext-real set
x0 - r is V30() real ext-real Element of REAL
x0 + r is V30() real ext-real Element of REAL
].(x0 - r),(x0 + r).[ is open V71() V72() V73() V99() V100() V104() Element of K19(REAL)
x0 + 0 is V30() real ext-real Element of REAL
{ b₁ where b₁ is V30() real ext-real Element of REAL : ( not b₁ <= x0 - r & not x0 + r <= b₁ ) } is set
dom (f `| N) is V71() V72() V73() Element of K19(REAL)
dom (g `| N) is V71() V72() V73() Element of K19(REAL)
(g `| N) " {0} is V71() V72() V73() Element of K19(REAL)
(dom (g `| N)) \ ((g `| N) " {0}) is V71() V72() V73() Element of K19(REAL)
(dom (f `| N)) /\ ((dom (g `| N)) \ ((g `| N) " {0})) is V71() V72() V73() Element of K19(REAL)
g " {0} is V71() V72() V73() Element of K19(REAL)
(dom g) \ (g " {0}) is V71() V72() V73() Element of K19(REAL)
(dom f) /\ ((dom g) \ (g " {0})) is V71() V72() V73() Element of K19(REAL)
d is V30() real ext-real Element of REAL
].d,x0.[ is open V71() V72() V73() V99() V100() V104() Element of K19(REAL)
(f / g) . d is V30() real ext-real Element of REAL
f . d is V30() real ext-real Element of REAL
(f . d) (#) g is V1() V4( REAL ) V5( REAL ) V6() V35() V36() V37() Element of K19(K20(REAL,REAL))
g . d is V30() real ext-real Element of REAL
(g . d) (#) f is V1() V4( REAL ) V5( REAL ) V6() V35() V36() V37() Element of K19(K20(REAL,REAL))
((f . d) (#) g) - ((g . d) (#) f) is V1() V4( REAL ) V5( REAL ) V6() V35() V36() V37() Element of K19(K20(REAL,REAL))
dom ((f . d) (#) g) is V71() V72() V73() Element of K19(REAL)
dom ((g . d) (#) f) is V71() V72() V73() Element of K19(REAL)
dom (((f . d) (#) g) - ((g . d) (#) f)) is V71() V72() V73() Element of K19(REAL)
(dom f) /\ (dom g) is V71() V72() V73() Element of K19(REAL)
[.d,x0.] is closed V71() V72() V73() V104() Element of K19(REAL)
g | N is V1() V4( REAL ) V5( REAL ) V6() V35() V36() V37() Element of K19(K20(REAL,REAL))
g | [.d,x0.] is V1() V4( REAL ) V5( REAL ) V6() V35() V36() V37() Element of K19(K20(REAL,REAL))
((f . d) (#) g) | [.d,x0.] is V1() V4( REAL ) V5( REAL ) V6() V35() V36() V37() Element of K19(K20(REAL,REAL))
f | N is V1() V4( REAL ) V5( REAL ) V6() V35() V36() V37() Element of K19(K20(REAL,REAL))
f | [.d,x0.] is V1() V4( REAL ) V5( REAL ) V6() V35() V36() V37() Element of K19(K20(REAL,REAL))
((g . d) (#) f) | [.d,x0.] is V1() V4( REAL ) V5( REAL ) V6() V35() V36() V37() Element of K19(K20(REAL,REAL))
(((f . d) (#) g) - ((g . d) (#) f)) | [.d,x0.] is V1() V4( REAL ) V5( REAL ) V6() V35() V36() V37() Element of K19(K20(REAL,REAL))
(dom ((f . d) (#) g)) /\ (dom ((g . d) (#) f)) is V71() V72() V73() Element of K19(REAL)
(((f . d) (#) g) - ((g . d) (#) f)) . d is V30() real ext-real Element of REAL
((f . d) (#) g) . d is V30() real ext-real Element of REAL
((g . d) (#) f) . d is V30() real ext-real Element of REAL
(((f . d) (#) g) . d) - (((g . d) (#) f) . d) is V30() real ext-real Element of REAL
(f . d) * (g . d) is V30() real ext-real Element of REAL
((f . d) * (g . d)) - (((g . d) (#) f) . d) is V30() real ext-real Element of REAL
(g . d) * (f . d) is V30() real ext-real Element of REAL
((g . d) * (f . d)) - ((g . d) * (f . d)) is V30() real ext-real Element of REAL
[.d,x0.] \ {x0} is V71() V72() V73() Element of K19(REAL)
(((f . d) (#) g) - ((g . d) (#) f)) . x0 is V30() real ext-real Element of REAL
((f . d) (#) g) . x0 is V30() real ext-real Element of REAL
((g . d) (#) f) . x0 is V30() real ext-real Element of REAL
(((f . d) (#) g) . x0) - (((g . d) (#) f) . x0) is V30() real ext-real Element of REAL
(f . d) * (g . x0) is V30() real ext-real Element of REAL
((f . d) * (g . x0)) - (((g . d) (#) f) . x0) is V30() real ext-real Element of REAL
(g . d) * 0 is V30() real ext-real Element of REAL
0 - ((g . d) * 0) is V30() real ext-real Element of REAL
k is V30() real ext-real Element of REAL
diff ((((f . d) (#) g) - ((g . d) (#) f)),k) is V30() real ext-real Element of REAL
diff (((f . d) (#) g),k) is V30() real ext-real Element of REAL
diff (((g . d) (#) f),k) is V30() real ext-real Element of REAL
(diff (((f . d) (#) g),k)) - (diff (((g . d) (#) f),k)) is V30() real ext-real Element of REAL
diff (f,k) is V30() real ext-real Element of REAL
(g . d) * (diff (f,k)) is V30() real ext-real Element of REAL
(diff (((f . d) (#) g),k)) - ((g . d) * (diff (f,k))) is V30() real ext-real Element of REAL
((f `| N) / (g `| N)) . k is V30() real ext-real Element of REAL
diff (g,k) is V30() real ext-real Element of REAL
(g `| N) . k is V30() real ext-real Element of REAL
(f . d) * (diff (g,k)) is V30() real ext-real Element of REAL
((f . d) * (diff (g,k))) - ((g . d) * (diff (f,k))) is V30() real ext-real Element of REAL
(f . d) / (g . d) is V30() real ext-real Element of REAL
(diff (f,k)) / (diff (g,k)) is V30() real ext-real Element of REAL
(g . d) " is V30() real ext-real Element of REAL
(f . d) * ((g . d) ") is V30() real ext-real Element of REAL
(diff (g,k)) " is V30() real ext-real Element of REAL
(diff (f,k)) * ((diff (g,k)) ") is V30() real ext-real Element of REAL
(f `| N) . k is V30() real ext-real Element of REAL
((f `| N) . k) * ((diff (g,k)) ") is V30() real ext-real Element of REAL
((g `| N) . k) " is V30() real ext-real Element of REAL
((f `| N) . k) * (((g `| N) . k) ") is V30() real ext-real Element of REAL
left_open_halfline x0 is V71() V72() V73() Element of K19(REAL)
K195(-infty,x0) is set
(dom (f / g)) /\ (left_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
NAT --> x0 is V1() V4( NAT ) V5( REAL ) V6() constant non empty total quasi_total V35() V36() V37() convergent Element of K19(K20(NAT,REAL))
a is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total V35() V36() V37() Element of K19(K20(NAT,REAL))
lim a is V30() real ext-real Element of REAL
rng a is V71() V72() V73() Element of K19(REAL)
(f / g) /* a is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total V35() V36() V37() Element of K19(K20(NAT,REAL))
k is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V71() V72() V73() V74() V75() V76() V93() V94() V101() Element of NAT
a ^\ k is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total V35() V36() V37() M7( REAL ,a)
((f / g) /* a) ^\ k is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total V35() V36() V37() M7( REAL ,(f / g) /* a)
b is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V71() V72() V73() V74() V75() V76() V93() V94() V101() Element of NAT
b + k is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V71() V72() V73() V74() V75() V76() V93() V94() V101() Element of NAT
a . (b + k) is V30() real ext-real Element of REAL
{ b₁ where b₁ is V30() real ext-real Element of REAL : not x0 <= b₁ } is set
(a ^\ k) . b is V30() real ext-real Element of REAL
m is V30() real ext-real Element of REAL
b is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V71() V72() V73() V74() V75() V76() V93() V94() V101() Element of NAT
(a ^\ k) . b is V30() real ext-real Element of REAL
].((a ^\ k) . b),x0.[ is open V71() V72() V73() V99() V100() V104() Element of K19(REAL)
(((f / g) /* a) ^\ k) . b is V30() real ext-real Element of REAL
rng (a ^\ k) is V71() V72() V73() Element of K19(REAL)
(f / g) . ((a ^\ k) . b) is V30() real ext-real Element of REAL
m is V30() real ext-real Element of REAL
((f `| N) / (g `| N)) . m is V30() real ext-real Element of REAL
(f / g) /* (a ^\ k) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total V35() V36() V37() Element of K19(K20(NAT,REAL))
((f / g) /* (a ^\ k)) . b is V30() real ext-real Element of REAL
b is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total V35() V36() V37() Element of K19(K20(NAT,REAL))
m is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V71() V72() V73() V74() V75() V76() V93() V94() V101() Element of NAT
b . m is V30() real ext-real Element of REAL
(a ^\ k) . m is V30() real ext-real Element of REAL
].((a ^\ k) . m),x0.[ is open V71() V72() V73() V99() V100() V104() Element of K19(REAL)
{ b₁ where b₁ is V30() real ext-real Element of REAL : ( not b₁ <= (a ^\ k) . m & not x0 <= b₁ ) } is set
d is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total V35() V36() V37() Element of K19(K20(NAT,REAL))
d . m is V30() real ext-real Element of REAL
n is V30() real ext-real Element of REAL
lim d is V30() real ext-real Element of REAL
d . 0 is V30() real ext-real Element of REAL
{ b₁ where b₁ is V30() real ext-real Element of REAL : ( not b₁ <= x0 - r & not x0 + r <= b₁ ) } is set
rng b is V71() V72() V73() Element of K19(REAL)
(dom ((f `| N) / (g `| N))) \ {x0} is V71() V72() V73() Element of K19(REAL)
m is set
n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V71() V72() V73() V74() V75() V76() V93() V94() V101() Element of NAT
b . n is V30() real ext-real Element of REAL
(a ^\ k) . n is V30() real ext-real Element of REAL
].((a ^\ k) . n),x0.[ is open V71() V72() V73() V99() V100() V104() Element of K19(REAL)
[.((a ^\ k) . n),x0.] is closed V71() V72() V73() V104() Element of K19(REAL)
{ b₁ where b₁ is V30() real ext-real Element of REAL : ( not b₁ <= (a ^\ k) . n & not x0 <= b₁ ) } is set
c₁₃ is V30() real ext-real Element of REAL
m is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V71() V72() V73() V74() V75() V76() V93() V94() V101() Element of NAT
(((f / g) /* a) ^\ k) . m is V30() real ext-real Element of REAL
b . m is V30() real ext-real Element of REAL
((f `| N) / (g `| N)) . (b . m) is V30() real ext-real Element of REAL
((f `| N) / (g `| N)) /* b is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total V35() V36() V37() Element of K19(K20(NAT,REAL))
(((f `| N) / (g `| N)) /* b) . m is V30() real ext-real Element of REAL
lim (a ^\ k) is V30() real ext-real Element of REAL
lim b is V30() real ext-real Element of REAL
d is V30() real ext-real Element of REAL
a is V30() real ext-real Element of REAL
d is V30() real ext-real Element of REAL
x0 + 0 is V30() real ext-real Element of REAL
{ b₁ where b₁ is V30() real ext-real Element of REAL : ( not b₁ <= x0 - r & not x0 + r <= b₁ ) } is set
dom (f `| N) is V71() V72() V73() Element of K19(REAL)
dom (g `| N) is V71() V72() V73() Element of K19(REAL)
(g `| N) " {0} is V71() V72() V73() Element of K19(REAL)
(dom (g `| N)) \ ((g `| N) " {0}) is V71() V72() V73() Element of K19(REAL)
(dom (f `| N)) /\ ((dom (g `| N)) \ ((g `| N) " {0})) is V71() V72() V73() Element of K19(REAL)
g " {0} is V71() V72() V73() Element of K19(REAL)
(dom g) \ (g " {0}) is V71() V72() V73() Element of K19(REAL)
(dom f) /\ ((dom g) \ (g " {0})) is V71() V72() V73() Element of K19(REAL)
d is V30() real ext-real Element of REAL
].x0,d.[ is open V71() V72() V73() V99() V100() V104() Element of K19(REAL)
(f / g) . d is V30() real ext-real Element of REAL
f . d is V30() real ext-real Element of REAL
(f . d) (#) g is V1() V4( REAL ) V5( REAL ) V6() V35() V36() V37() Element of K19(K20(REAL,REAL))
g . d is V30() real ext-real Element of REAL
(g . d) (#) f is V1() V4( REAL ) V5( REAL ) V6() V35() V36() V37() Element of K19(K20(REAL,REAL))
((f . d) (#) g) - ((g . d) (#) f) is V1() V4( REAL ) V5( REAL ) V6() V35() V36() V37() Element of K19(K20(REAL,REAL))
dom ((f . d) (#) g) is V71() V72() V73() Element of K19(REAL)
dom ((g . d) (#) f) is V71() V72() V73() Element of K19(REAL)
[.x0,d.] is closed V71() V72() V73() V104() Element of K19(REAL)
(dom f) /\ (dom g) is V71() V72() V73() Element of K19(REAL)
dom (((f . d) (#) g) - ((g . d) (#) f)) is V71() V72() V73() Element of K19(REAL)
g | N is V1() V4( REAL ) V5( REAL ) V6() V35() V36() V37() Element of K19(K20(REAL,REAL))
g | [.x0,d.] is V1() V4( REAL ) V5( REAL ) V6() V35() V36() V37() Element of K19(K20(REAL,REAL))
((f . d) (#) g) | [.x0,d.] is V1() V4( REAL ) V5( REAL ) V6() V35() V36() V37() Element of K19(K20(REAL,REAL))
f | N is V1() V4( REAL ) V5( REAL ) V6() V35() V36() V37() Element of K19(K20(REAL,REAL))
f | [.x0,d.] is V1() V4( REAL ) V5( REAL ) V6() V35() V36() V37() Element of K19(K20(REAL,REAL))
((g . d) (#) f) | [.x0,d.] is V1() V4( REAL ) V5( REAL ) V6() V35() V36() V37() Element of K19(K20(REAL,REAL))
(((f . d) (#) g) - ((g . d) (#) f)) | [.x0,d.] is V1() V4( REAL ) V5( REAL ) V6() V35() V36() V37() Element of K19(K20(REAL,REAL))
(dom ((f . d) (#) g)) /\ (dom ((g . d) (#) f)) is V71() V72() V73() Element of K19(REAL)
(((f . d) (#) g) - ((g . d) (#) f)) . d is V30() real ext-real Element of REAL
((f . d) (#) g) . d is V30() real ext-real Element of REAL
((g . d) (#) f) . d is V30() real ext-real Element of REAL
(((f . d) (#) g) . d) - (((g . d) (#) f) . d) is V30() real ext-real Element of REAL
(f . d) * (g . d) is V30() real ext-real Element of REAL
((f . d) * (g . d)) - (((g . d) (#) f) . d) is V30() real ext-real Element of REAL
(g . d) * (f . d) is V30() real ext-real Element of REAL
((g . d) * (f . d)) - ((g . d) * (f . d)) is V30() real ext-real Element of REAL
[.x0,d.] \ {x0} is V71() V72() V73() Element of K19(REAL)
(((f . d) (#) g) - ((g . d) (#) f)) . x0 is V30() real ext-real Element of REAL
((f . d) (#) g) . x0 is V30() real ext-real Element of REAL
((g . d) (#) f) . x0 is V30() real ext-real Element of REAL
(((f . d) (#) g) . x0) - (((g . d) (#) f) . x0) is V30() real ext-real Element of REAL
(f . d) * (g . x0) is V30() real ext-real Element of REAL
((f . d) * (g . x0)) - (((g . d) (#) f) . x0) is V30() real ext-real Element of REAL
(g . d) * 0 is V30() real ext-real Element of REAL
0 - ((g . d) * 0) is V30() real ext-real Element of REAL
k is V30() real ext-real Element of REAL
diff ((((f . d) (#) g) - ((g . d) (#) f)),k) is V30() real ext-real Element of REAL
diff (((f . d) (#) g),k) is V30() real ext-real Element of REAL
diff (((g . d) (#) f),k) is V30() real ext-real Element of REAL
(diff (((f . d) (#) g),k)) - (diff (((g . d) (#) f),k)) is V30() real ext-real Element of REAL
diff (f,k) is V30() real ext-real Element of REAL
(g . d) * (diff (f,k)) is V30() real ext-real Element of REAL
(diff (((f . d) (#) g),k)) - ((g . d) * (diff (f,k))) is V30() real ext-real Element of REAL
((f `| N) / (g `| N)) . k is V30() real ext-real Element of REAL
diff (g,k) is V30() real ext-real Element of REAL
(g `| N) . k is V30() real ext-real Element of REAL
(f . d) * (diff (g,k)) is V30() real ext-real Element of REAL
((f . d) * (diff (g,k))) - ((g . d) * (diff (f,k))) is V30() real ext-real Element of REAL
(f . d) / (g . d) is V30() real ext-real Element of REAL
(diff (f,k)) / (diff (g,k)) is V30() real ext-real Element of REAL
(g . d) " is V30() real ext-real Element of REAL
(f . d) * ((g . d) ") is V30() real ext-real Element of REAL
(diff (g,k)) " is V30() real ext-real Element of REAL
(diff (f,k)) * ((diff (g,k)) ") is V30() real ext-real Element of REAL
(f `| N) . k is V30() real ext-real Element of REAL
((f `| N) . k) * ((diff (g,k)) ") is V30() real ext-real Element of REAL
((g `| N) . k) " is V30() real ext-real Element of REAL
((f `| N) . k) * (((g `| N) . k) ") is V30() real ext-real Element of REAL
right_open_halfline x0 is V71() V72() V73() Element of K19(REAL)
K195(x0,+infty) is set
(dom (f / g)) /\ (right_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
NAT --> x0 is V1() V4( NAT ) V5( REAL ) V6() constant non empty total quasi_total V35() V36() V37() convergent Element of K19(K20(NAT,REAL))
a is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total V35() V36() V37() Element of K19(K20(NAT,REAL))
lim a is V30() real ext-real Element of REAL
rng a is V71() V72() V73() Element of K19(REAL)
(f / g) /* a is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total V35() V36() V37() Element of K19(K20(NAT,REAL))
k is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V71() V72() V73() V74() V75() V76() V93() V94() V101() Element of NAT
a ^\ k is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total V35() V36() V37() M7( REAL ,a)
((f / g) /* a) ^\ k is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total V35() V36() V37() M7( REAL ,(f / g) /* a)
b is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V71() V72() V73() V74() V75() V76() V93() V94() V101() Element of NAT
b + k is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V71() V72() V73() V74() V75() V76() V93() V94() V101() Element of NAT
a . (b + k) is V30() real ext-real Element of REAL
{ b₁ where b₁ is V30() real ext-real Element of REAL : not b₁ <= x0 } is set
(a ^\ k) . b is V30() real ext-real Element of REAL
m is V30() real ext-real Element of REAL
b is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V71() V72() V73() V74() V75() V76() V93() V94() V101() Element of NAT
(a ^\ k) . b is V30() real ext-real Element of REAL
].x0,((a ^\ k) . b).[ is open V71() V72() V73() V99() V100() V104() Element of K19(REAL)
(((f / g) /* a) ^\ k) . b is V30() real ext-real Element of REAL
rng (a ^\ k) is V71() V72() V73() Element of K19(REAL)
(f / g) . ((a ^\ k) . b) is V30() real ext-real Element of REAL
m is V30() real ext-real Element of REAL
((f `| N) / (g `| N)) . m is V30() real ext-real Element of REAL
(f / g) /* (a ^\ k) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total V35() V36() V37() Element of K19(K20(NAT,REAL))
((f / g) /* (a ^\ k)) . b is V30() real ext-real Element of REAL
b is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total V35() V36() V37() Element of K19(K20(NAT,REAL))
m is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V71() V72() V73() V74() V75() V76() V93() V94() V101() Element of NAT
b . m is V30() real ext-real Element of REAL
(a ^\ k) . m is V30() real ext-real Element of REAL
].x0,((a ^\ k) . m).[ is open V71() V72() V73() V99() V100() V104() Element of K19(REAL)
{ b₁ where b₁ is V30() real ext-real Element of REAL : ( not b₁ <= x0 & not (a ^\ k) . m <= b₁ ) } is set
d is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total V35() V36() V37() Element of K19(K20(NAT,REAL))
d . m is V30() real ext-real Element of REAL
n is V30() real ext-real Element of REAL
lim d is V30() real ext-real Element of REAL
d . 0 is V30() real ext-real Element of REAL
{ b₁ where b₁ is V30() real ext-real Element of REAL : ( not b₁ <= x0 - r & not x0 + r <= b₁ ) } is set
rng b is V71() V72() V73() Element of K19(REAL)
(dom ((f `| N) / (g `| N))) \ {x0} is V71() V72() V73() Element of K19(REAL)
m is set
n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V71() V72() V73() V74() V75() V76() V93() V94() V101() Element of NAT
b . n is V30() real ext-real Element of REAL
(a ^\ k) . n is V30() real ext-real Element of REAL
].x0,((a ^\ k) . n).[ is open V71() V72() V73() V99() V100() V104() Element of K19(REAL)
[.x0,((a ^\ k) . n).] is closed V71() V72() V73() V104() Element of K19(REAL)
{ b₁ where b₁ is V30() real ext-real Element of REAL : ( not b₁ <= x0 & not (a ^\ k) . n <= b₁ ) } is set
c₁₃ is V30() real ext-real Element of REAL
m is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V71() V72() V73() V74() V75() V76() V93() V94() V101() Element of NAT
(((f / g) /* a) ^\ k) . m is V30() real ext-real Element of REAL
b . m is V30() real ext-real Element of REAL
((f `| N) / (g `| N)) . (b . m) is V30() real ext-real Element of REAL
((f `| N) / (g `| N)) /* b is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total V35() V36() V37() Element of K19(K20(NAT,REAL))
(((f `| N) / (g `| N)) /* b) . m is V30() real ext-real Element of REAL
lim (a ^\ k) is V30() real ext-real Element of REAL
lim b is V30() real ext-real Element of REAL
d is V30() real ext-real Element of REAL
f is V1() V4( REAL ) V5( REAL ) V6() V35() V36() V37() Element of K19(K20(REAL,REAL))
dom f is V71() V72() V73() Element of K19(REAL)
g is V1() V4( REAL ) V5( REAL ) V6() V35() V36() V37() Element of K19(K20(REAL,REAL))
dom g is V71() V72() V73() Element of K19(REAL)
f / g is V1() V4( REAL ) V5( REAL ) V6() V35() V36() V37() Element of K19(K20(REAL,REAL))
dom (f / g) is V71() V72() V73() Element of K19(REAL)
x0 is V30() real ext-real Element of REAL
{x0} is non empty V71() V72() V73() set
f . x0 is V30() real ext-real Element of REAL
g . x0 is V30() real ext-real Element of REAL
N is open V71() V72() V73() Neighbourhood of x0
N \ {x0} is V71() V72() V73() Element of K19(REAL)
f `| N is V1() V4( REAL ) V5( REAL ) V6() V35() V36() V37() Element of K19(K20(REAL,REAL))
g `| N is V1() V4( REAL ) V5( REAL ) V6() V35() V36() V37() Element of K19(K20(REAL,REAL))
(f `| N) / (g `| N) is V1() V4( REAL ) V5( REAL ) V6() V35() V36() V37() Element of K19(K20(REAL,REAL))
dom ((f `| N) / (g `| N)) is V71() V72() V73() Element of K19(REAL)
r is V30() real ext-real set
x0 - r is V30() real ext-real Element of REAL
x0 + r is V30() real ext-real Element of REAL
].(x0 - r),(x0 + r).[ is open V71() V72() V73() V99() V100() V104() Element of K19(REAL)
x0 + 0 is V30() real ext-real Element of REAL
{ b₁ where b₁ is V30() real ext-real Element of REAL : ( not b₁ <= x0 - r & not x0 + r <= b₁ ) } is set
dom (f `| N) is V71() V72() V73() Element of K19(REAL)
dom (g `| N) is V71() V72() V73() Element of K19(REAL)
(g `| N) " {0} is V71() V72() V73() Element of K19(REAL)
(dom (g `| N)) \ ((g `| N) " {0}) is V71() V72() V73() Element of K19(REAL)
(dom (f `| N)) /\ ((dom (g `| N)) \ ((g `| N) " {0})) is V71() V72() V73() Element of K19(REAL)
g " {0} is V71() V72() V73() Element of K19(REAL)
(dom g) \ (g " {0}) is V71() V72() V73() Element of K19(REAL)
(dom f) /\ ((dom g) \ (g " {0})) is V71() V72() V73() Element of K19(REAL)
d is V30() real ext-real Element of REAL
].d,x0.[ is open V71() V72() V73() V99() V100() V104() Element of K19(REAL)
(f / g) . d is V30() real ext-real Element of REAL
f . d is V30() real ext-real Element of REAL
(f . d) (#) g is V1() V4( REAL ) V5( REAL ) V6() V35() V36() V37() Element of K19(K20(REAL,REAL))
g . d is V30() real ext-real Element of REAL
(g . d) (#) f is V1() V4( REAL ) V5( REAL ) V6() V35() V36() V37() Element of K19(K20(REAL,REAL))
((f . d) (#) g) - ((g . d) (#) f) is V1() V4( REAL ) V5( REAL ) V6() V35() V36() V37() Element of K19(K20(REAL,REAL))
dom ((f . d) (#) g) is V71() V72() V73() Element of K19(REAL)
dom ((g . d) (#) f) is V71() V72() V73() Element of K19(REAL)
dom (((f . d) (#) g) - ((g . d) (#) f)) is V71() V72() V73() Element of K19(REAL)
(dom f) /\ (dom g) is V71() V72() V73() Element of K19(REAL)
[.d,x0.] is closed V71() V72() V73() V104() Element of K19(REAL)
g | N is V1() V4( REAL ) V5( REAL ) V6() V35() V36() V37() Element of K19(K20(REAL,REAL))
g | [.d,x0.] is V1() V4( REAL ) V5( REAL ) V6() V35() V36() V37() Element of K19(K20(REAL,REAL))
((f . d) (#) g) | [.d,x0.] is V1() V4( REAL ) V5( REAL ) V6() V35() V36() V37() Element of K19(K20(REAL,REAL))
f | N is V1() V4( REAL ) V5( REAL ) V6() V35() V36() V37() Element of K19(K20(REAL,REAL))
f | [.d,x0.] is V1() V4( REAL ) V5( REAL ) V6() V35() V36() V37() Element of K19(K20(REAL,REAL))
((g . d) (#) f) | [.d,x0.] is V1() V4( REAL ) V5( REAL ) V6() V35() V36() V37() Element of K19(K20(REAL,REAL))
(((f . d) (#) g) - ((g . d) (#) f)) | [.d,x0.] is V1() V4( REAL ) V5( REAL ) V6() V35() V36() V37() Element of K19(K20(REAL,REAL))
(dom ((f . d) (#) g)) /\ (dom ((g . d) (#) f)) is V71() V72() V73() Element of K19(REAL)
(((f . d) (#) g) - ((g . d) (#) f)) . d is V30() real ext-real Element of REAL
((f . d) (#) g) . d is V30() real ext-real Element of REAL
((g . d) (#) f) . d is V30() real ext-real Element of REAL
(((f . d) (#) g) . d) - (((g . d) (#) f) . d) is V30() real ext-real Element of REAL
(f . d) * (g . d) is V30() real ext-real Element of REAL
((f . d) * (g . d)) - (((g . d) (#) f) . d) is V30() real ext-real Element of REAL
(g . d) * (f . d) is V30() real ext-real Element of REAL
((g . d) * (f . d)) - ((g . d) * (f . d)) is V30() real ext-real Element of REAL
[.d,x0.] \ {x0} is V71() V72() V73() Element of K19(REAL)
(((f . d) (#) g) - ((g . d) (#) f)) . x0 is V30() real ext-real Element of REAL
((f . d) (#) g) . x0 is V30() real ext-real Element of REAL
((g . d) (#) f) . x0 is V30() real ext-real Element of REAL
(((f . d) (#) g) . x0) - (((g . d) (#) f) . x0) is V30() real ext-real Element of REAL
(f . d) * (g . x0) is V30() real ext-real Element of REAL
((f . d) * (g . x0)) - (((g . d) (#) f) . x0) is V30() real ext-real Element of REAL
(g . d) * 0 is V30() real ext-real Element of REAL
0 - ((g . d) * 0) is V30() real ext-real Element of REAL
k is V30() real ext-real Element of REAL
diff ((((f . d) (#) g) - ((g . d) (#) f)),k) is V30() real ext-real Element of REAL
diff (((f . d) (#) g),k) is V30() real ext-real Element of REAL
diff (((g . d) (#) f),k) is V30() real ext-real Element of REAL
(diff (((f . d) (#) g),k)) - (diff (((g . d) (#) f),k)) is V30() real ext-real Element of REAL
diff (f,k) is V30() real ext-real Element of REAL
(g . d) * (diff (f,k)) is V30() real ext-real Element of REAL
(diff (((f . d) (#) g),k)) - ((g . d) * (diff (f,k))) is V30() real ext-real Element of REAL
((f `| N) / (g `| N)) . k is V30() real ext-real Element of REAL
diff (g,k) is V30() real ext-real Element of REAL
(g `| N) . k is V30() real ext-real Element of REAL
(f . d) * (diff (g,k)) is V30() real ext-real Element of REAL
((f . d) * (diff (g,k))) - ((g . d) * (diff (f,k))) is V30() real ext-real Element of REAL
(f . d) / (g . d) is V30() real ext-real Element of REAL
(diff (f,k)) / (diff (g,k)) is V30() real ext-real Element of REAL
(g . d) " is V30() real ext-real Element of REAL
(f . d) * ((g . d) ") is V30() real ext-real Element of REAL
(diff (g,k)) " is V30() real ext-real Element of REAL
(diff (f,k)) * ((diff (g,k)) ") is V30() real ext-real Element of REAL
(f `| N) . k is V30() real ext-real Element of REAL
((f `| N) . k) * ((diff (g,k)) ") is V30() real ext-real Element of REAL
((g `| N) . k) " is V30() real ext-real Element of REAL
((f `| N) . k) * (((g `| N) . k) ") is V30() real ext-real Element of REAL
left_open_halfline x0 is V71() V72() V73() Element of K19(REAL)
K195(-infty,x0) is set
(dom (f / g)) /\ (left_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
NAT --> x0 is V1() V4( NAT ) V5( REAL ) V6() constant non empty total quasi_total V35() V36() V37() convergent Element of K19(K20(NAT,REAL))
a is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total V35() V36() V37() Element of K19(K20(NAT,REAL))
lim a is V30() real ext-real Element of REAL
rng a is V71() V72() V73() Element of K19(REAL)
(f / g) /* a is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total V35() V36() V37() Element of K19(K20(NAT,REAL))
k is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V71() V72() V73() V74() V75() V76() V93() V94() V101() Element of NAT
a ^\ k is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total V35() V36() V37() M7( REAL ,a)
((f / g) /* a) ^\ k is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total V35() V36() V37() M7( REAL ,(f / g) /* a)
b is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V71() V72() V73() V74() V75() V76() V93() V94() V101() Element of NAT
b + k is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V71() V72() V73() V74() V75() V76() V93() V94() V101() Element of NAT
a . (b + k) is V30() real ext-real Element of REAL
{ b₁ where b₁ is V30() real ext-real Element of REAL : not x0 <= b₁ } is set
(a ^\ k) . b is V30() real ext-real Element of REAL
m is V30() real ext-real Element of REAL
b is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V71() V72() V73() V74() V75() V76() V93() V94() V101() Element of NAT
(a ^\ k) . b is V30() real ext-real Element of REAL
].((a ^\ k) . b),x0.[ is open V71() V72() V73() V99() V100() V104() Element of K19(REAL)
(((f / g) /* a) ^\ k) . b is V30() real ext-real Element of REAL
rng (a ^\ k) is V71() V72() V73() Element of K19(REAL)
(f / g) . ((a ^\ k) . b) is V30() real ext-real Element of REAL
m is V30() real ext-real Element of REAL
((f `| N) / (g `| N)) . m is V30() real ext-real Element of REAL
(f / g) /* (a ^\ k) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total V35() V36() V37() Element of K19(K20(NAT,REAL))
((f / g) /* (a ^\ k)) . b is V30() real ext-real Element of REAL
b is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total V35() V36() V37() Element of K19(K20(NAT,REAL))
m is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V71() V72() V73() V74() V75() V76() V93() V94() V101() Element of NAT
b . m is V30() real ext-real Element of REAL
(a ^\ k) . m is V30() real ext-real Element of REAL
].((a ^\ k) . m),x0.[ is open V71() V72() V73() V99() V100() V104() Element of K19(REAL)
{ b₁ where b₁ is V30() real ext-real Element of REAL : ( not b₁ <= (a ^\ k) . m & not x0 <= b₁ ) } is set
d is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total V35() V36() V37() Element of K19(K20(NAT,REAL))
d . m is V30() real ext-real Element of REAL
n is V30() real ext-real Element of REAL
lim d is V30() real ext-real Element of REAL
d . 0 is V30() real ext-real Element of REAL
{ b₁ where b₁ is V30() real ext-real Element of REAL : ( not b₁ <= x0 - r & not x0 + r <= b₁ ) } is set
rng b is V71() V72() V73() Element of K19(REAL)
(dom ((f `| N) / (g `| N))) \ {x0} is V71() V72() V73() Element of K19(REAL)
m is set
n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V71() V72() V73() V74() V75() V76() V93() V94() V101() Element of NAT
b . n is V30() real ext-real Element of REAL
(a ^\ k) . n is V30() real ext-real Element of REAL
].((a ^\ k) . n),x0.[ is open V71() V72() V73() V99() V100() V104() Element of K19(REAL)
[.((a ^\ k) . n),x0.] is closed V71() V72() V73() V104() Element of K19(REAL)
{ b₁ where b₁ is V30() real ext-real Element of REAL : ( not b₁ <= (a ^\ k) . n & not x0 <= b₁ ) } is set
c₁₃ is V30() real ext-real Element of REAL
m is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V71() V72() V73() V74() V75() V76() V93() V94() V101() Element of NAT
(((f / g) /* a) ^\ k) . m is V30() real ext-real Element of REAL
b . m is V30() real ext-real Element of REAL
((f `| N) / (g `| N)) . (b . m) is V30() real ext-real Element of REAL
((f `| N) / (g `| N)) /* b is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total V35() V36() V37() Element of K19(K20(NAT,REAL))
(((f `| N) / (g `| N)) /* b) . m is V30() real ext-real Element of REAL
lim (a ^\ k) is V30() real ext-real Element of REAL
lim b is V30() real ext-real Element of REAL
d is V30() real ext-real Element of REAL
a is V30() real ext-real Element of REAL
d is V30() real ext-real Element of REAL
dom (f `| N) is V71() V72() V73() Element of K19(REAL)
dom (g `| N) is V71() V72() V73() Element of K19(REAL)
(g `| N) " {0} is V71() V72() V73() Element of K19(REAL)
(dom (g `| N)) \ ((g `| N) " {0}) is V71() V72() V73() Element of K19(REAL)
(dom (f `| N)) /\ ((dom (g `| N)) \ ((g `| N) " {0})) is V71() V72() V73() Element of K19(REAL)
x0 + 0 is V30() real ext-real Element of REAL
{ b₁ where b₁ is V30() real ext-real Element of REAL : ( not b₁ <= x0 - r & not x0 + r <= b₁ ) } is set
d is V30() real ext-real Element of REAL
].x0,d.[ is open V71() V72() V73() V99() V100() V104() Element of K19(REAL)
(f / g) . d is V30() real ext-real Element of REAL
[.x0,d.] is closed V71() V72() V73() V104() Element of K19(REAL)
g | N is V1() V4( REAL ) V5( REAL ) V6() V35() V36() V37() Element of K19(K20(REAL,REAL))
g | [.x0,d.] is V1() V4( REAL ) V5( REAL ) V6() V35() V36() V37() Element of K19(K20(REAL,REAL))
f . d is V30() real ext-real Element of REAL
(f . d) (#) g is V1() V4( REAL ) V5( REAL ) V6() V35() V36() V37() Element of K19(K20(REAL,REAL))
((f . d) (#) g) | [.x0,d.] is V1() V4( REAL ) V5( REAL ) V6() V35() V36() V37() Element of K19(K20(REAL,REAL))
f | N is V1() V4( REAL ) V5( REAL ) V6() V35() V36() V37() Element of K19(K20(REAL,REAL))
f | [.x0,d.] is V1() V4( REAL ) V5( REAL ) V6() V35() V36() V37() Element of K19(K20(REAL,REAL))
g . d is V30() real ext-real Element of REAL
(g . d) (#) f is V1() V4( REAL ) V5( REAL ) V6() V35() V36() V37() Element of K19(K20(REAL,REAL))
((g . d) (#) f) | [.x0,d.] is V1() V4( REAL ) V5( REAL ) V6() V35() V36() V37() Element of K19(K20(REAL,REAL))
dom ((f . d) (#) g) is V71() V72() V73() Element of K19(REAL)
dom ((g . d) (#) f) is V71() V72() V73() Element of K19(REAL)
((f . d) (#) g) - ((g . d) (#) f) is V1() V4( REAL ) V5( REAL ) V6() V35() V36() V37() Element of K19(K20(REAL,REAL))
dom (((f . d) (#) g) - ((g . d) (#) f)) is V71() V72() V73() Element of K19(REAL)
(dom f) /\ (dom g) is V71() V72() V73() Element of K19(REAL)
(((f . d) (#) g) - ((g . d) (#) f)) | [.x0,d.] is V1() V4( REAL ) V5( REAL ) V6() V35() V36() V37() Element of K19(K20(REAL,REAL))
(dom ((f . d) (#) g)) /\ (dom ((g . d) (#) f)) is V71() V72() V73() Element of K19(REAL)
g " {0} is V71() V72() V73() Element of K19(REAL)
(dom g) \ (g " {0}) is V71() V72() V73() Element of K19(REAL)
(dom f) /\ ((dom g) \ (g " {0})) is V71() V72() V73() Element of K19(REAL)
(((f . d) (#) g) - ((g . d) (#) f)) . d is V30() real ext-real Element of REAL
((f . d) (#) g) . d is V30() real ext-real Element of REAL
((g . d) (#) f) . d is V30() real ext-real Element of REAL
(((f . d) (#) g) . d) - (((g . d) (#) f) . d) is V30() real ext-real Element of REAL
(f . d) * (g . d) is V30() real ext-real Element of REAL
((f . d) * (g . d)) - (((g . d) (#) f) . d) is V30() real ext-real Element of REAL
(g . d) * (f . d) is V30() real ext-real Element of REAL
((g . d) * (f . d)) - ((g . d) * (f . d)) is V30() real ext-real Element of REAL
[.x0,d.] \ {x0} is V71() V72() V73() Element of K19(REAL)
(((f . d) (#) g) - ((g . d) (#) f)) . x0 is V30() real ext-real Element of REAL
((f . d) (#) g) . x0 is V30() real ext-real Element of REAL
((g . d) (#) f) . x0 is V30() real ext-real Element of REAL
(((f . d) (#) g) . x0) - (((g . d) (#) f) . x0) is V30() real ext-real Element of REAL
(f . d) * (g . x0) is V30() real ext-real Element of REAL
((f . d) * (g . x0)) - (((g . d) (#) f) . x0) is V30() real ext-real Element of REAL
(g . d) * 0 is V30() real ext-real Element of REAL
0 - ((g . d) * 0) is V30() real ext-real Element of REAL
k is V30() real ext-real Element of REAL
diff ((((f . d) (#) g) - ((g . d) (#) f)),k) is V30() real ext-real Element of REAL
diff (((f . d) (#) g),k) is V30() real ext-real Element of REAL
diff (((g . d) (#) f),k) is V30() real ext-real Element of REAL
(diff (((f . d) (#) g),k)) - (diff (((g . d) (#) f),k)) is V30() real ext-real Element of REAL
diff (f,k) is V30() real ext-real Element of REAL
(g . d) * (diff (f,k)) is V30() real ext-real Element of REAL
(diff (((f . d) (#) g),k)) - ((g . d) * (diff (f,k))) is V30() real ext-real Element of REAL
((f `| N) / (g `| N)) . k is V30() real ext-real Element of REAL
diff (g,k) is V30() real ext-real Element of REAL
(g `| N) . k is V30() real ext-real Element of REAL
(f . d) * (diff (g,k)) is V30() real ext-real Element of REAL
((f . d) * (diff (g,k))) - ((g . d) * (diff (f,k))) is V30() real ext-real Element of REAL
(f . d) / (g . d) is V30() real ext-real Element of REAL
(diff (f,k)) / (diff (g,k)) is V30() real ext-real Element of REAL
(g . d) " is V30() real ext-real Element of REAL
(f . d) * ((g . d) ") is V30() real ext-real Element of REAL
(diff (g,k)) " is V30() real ext-real Element of REAL
(diff (f,k)) * ((diff (g,k)) ") is V30() real ext-real Element of REAL
(f `| N) . k is V30() real ext-real Element of REAL
((f `| N) . k) * ((diff (g,k)) ") is V30() real ext-real Element of REAL
((g `| N) . k) " is V30() real ext-real Element of REAL
((f `| N) . k) * (((g `| N) . k) ") is V30() real ext-real Element of REAL
right_open_halfline x0 is V71() V72() V73() Element of K19(REAL)
K195(x0,+infty) is set
(dom (f / g)) /\ (right_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
NAT --> x0 is V1() V4( NAT ) V5( REAL ) V6() constant non empty total quasi_total V35() V36() V37() convergent Element of K19(K20(NAT,REAL))
a is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total V35() V36() V37() Element of K19(K20(NAT,REAL))
lim a is V30() real ext-real Element of REAL
rng a is V71() V72() V73() Element of K19(REAL)
(f / g) /* a is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total V35() V36() V37() Element of K19(K20(NAT,REAL))
k is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V71() V72() V73() V74() V75() V76() V93() V94() V101() Element of NAT
a ^\ k is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total V35() V36() V37() M7( REAL ,a)
((f / g) /* a) ^\ k is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total V35() V36() V37() M7( REAL ,(f / g) /* a)
b is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V71() V72() V73() V74() V75() V76() V93() V94() V101() Element of NAT
b + k is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V71() V72() V73() V74() V75() V76() V93() V94() V101() Element of NAT
a . (b + k) is V30() real ext-real Element of REAL
{ b₁ where b₁ is V30() real ext-real Element of REAL : not b₁ <= x0 } is set
(a ^\ k) . b is V30() real ext-real Element of REAL
m is V30() real ext-real Element of REAL
b is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V71() V72() V73() V74() V75() V76() V93() V94() V101() Element of NAT
(a ^\ k) . b is V30() real ext-real Element of REAL
].x0,((a ^\ k) . b).[ is open V71() V72() V73() V99() V100() V104() Element of K19(REAL)
(((f / g) /* a) ^\ k) . b is V30() real ext-real Element of REAL
rng (a ^\ k) is V71() V72() V73() Element of K19(REAL)
(f / g) . ((a ^\ k) . b) is V30() real ext-real Element of REAL
m is V30() real ext-real Element of REAL
((f `| N) / (g `| N)) . m is V30() real ext-real Element of REAL
(f / g) /* (a ^\ k) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total V35() V36() V37() Element of K19(K20(NAT,REAL))
((f / g) /* (a ^\ k)) . b is V30() real ext-real Element of REAL
b is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total V35() V36() V37() Element of K19(K20(NAT,REAL))
m is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V71() V72() V73() V74() V75() V76() V93() V94() V101() Element of NAT
b . m is V30() real ext-real Element of REAL
(a ^\ k) . m is V30() real ext-real Element of REAL
].x0,((a ^\ k) . m).[ is open V71() V72() V73() V99() V100() V104() Element of K19(REAL)
{ b₁ where b₁ is V30() real ext-real Element of REAL : ( not b₁ <= x0 & not (a ^\ k) . m <= b₁ ) } is set
d is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total V35() V36() V37() Element of K19(K20(NAT,REAL))
d . m is V30() real ext-real Element of REAL
n is V30() real ext-real Element of REAL
lim d is V30() real ext-real Element of REAL
d . 0 is V30() real ext-real Element of REAL
{ b₁ where b₁ is V30() real ext-real Element of REAL : ( not b₁ <= x0 - r & not x0 + r <= b₁ ) } is set
rng b is V71() V72() V73() Element of K19(REAL)
(dom ((f `| N) / (g `| N))) \ {x0} is V71() V72() V73() Element of K19(REAL)
m is set
n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V71() V72() V73() V74() V75() V76() V93() V94() V101() Element of NAT
b . n is V30() real ext-real Element of REAL
(a ^\ k) . n is V30() real ext-real Element of REAL
].x0,((a ^\ k) . n).[ is open V71() V72() V73() V99() V100() V104() Element of K19(REAL)
[.x0,((a ^\ k) . n).] is closed V71() V72() V73() V104() Element of K19(REAL)
{ b₁ where b₁ is V30() real ext-real Element of REAL : ( not b₁ <= x0 & not (a ^\ k) . n <= b₁ ) } is set
c₁₃ is V30() real ext-real Element of REAL
m is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V71() V72() V73() V74() V75() V76() V93() V94() V101() Element of NAT
(((f / g) /* a) ^\ k) . m is V30() real ext-real Element of REAL
b . m is V30() real ext-real Element of REAL
((f `| N) / (g `| N)) . (b . m) is V30() real ext-real Element of REAL
((f `| N) / (g `| N)) /* b is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total V35() V36() V37() Element of K19(K20(NAT,REAL))
(((f `| N) / (g `| N)) /* b) . m is V30() real ext-real Element of REAL
lim (a ^\ k) is V30() real ext-real Element of REAL
lim b is V30() real ext-real Element of REAL
d is V30() real ext-real Element of REAL
f is V1() V4( REAL ) V5( REAL ) V6() V35() V36() V37() Element of K19(K20(REAL,REAL))
dom f is V71() V72() V73() Element of K19(REAL)
g is V1() V4( REAL ) V5( REAL ) V6() V35() V36() V37() Element of K19(K20(REAL,REAL))
dom g is V71() V72() V73() Element of K19(REAL)
(dom f) /\ (dom g) is V71() V72() V73() Element of K19(REAL)
f / g is V1() V4( REAL ) V5( REAL ) V6() V35() V36() V37() Element of K19(K20(REAL,REAL))
dom (f / g) is V71() V72() V73() Element of K19(REAL)
x0 is V30() real ext-real Element of REAL
f . x0 is V30() real ext-real Element of REAL
g . x0 is V30() real ext-real Element of REAL
lim_right ((f / g),x0) is V30() real ext-real Element of REAL
N is V30() real ext-real Element of REAL
x0 + N is V30() real ext-real Element of REAL
[.x0,(x0 + N).] is closed V71() V72() V73() V104() Element of K19(REAL)
].x0,(x0 + N).[ is open V71() V72() V73() V99() V100() V104() Element of K19(REAL)
f `| ].x0,(x0 + N).[ is V1() V4( REAL ) V5( REAL ) V6() V35() V36() V37() Element of K19(K20(REAL,REAL))
g `| ].x0,(x0 + N).[ is V1() V4( REAL ) V5( REAL ) V6() V35() V36() V37() Element of K19(K20(REAL,REAL))
(f `| ].x0,(x0 + N).[) / (g `| ].x0,(x0 + N).[) is V1() V4( REAL ) V5( REAL ) V6() V35() V36() V37() Element of K19(K20(REAL,REAL))
dom ((f `| ].x0,(x0 + N).[) / (g `| ].x0,(x0 + N).[)) is V71() V72() V73() Element of K19(REAL)
r is V30() real ext-real Element of REAL
].x0,r.[ is open V71() V72() V73() V99() V100() V104() Element of K19(REAL)
(f / g) . r is V30() real ext-real Element of REAL
f . r is V30() real ext-real Element of REAL
(f . r) (#) g is V1() V4( REAL ) V5( REAL ) V6() V35() V36() V37() Element of K19(K20(REAL,REAL))
g . r is V30() real ext-real Element of REAL
(g . r) (#) f is V1() V4( REAL ) V5( REAL ) V6() V35() V36() V37() Element of K19(K20(REAL,REAL))
((f . r) (#) g) - ((g . r) (#) f) is V1() V4( REAL ) V5( REAL ) V6() V35() V36() V37() Element of K19(K20(REAL,REAL))
dom ((g . r) (#) f) is V71() V72() V73() Element of K19(REAL)
dom ((f . r) (#) g) is V71() V72() V73() Element of K19(REAL)
dom (((f . r) (#) g) - ((g . r) (#) f)) is V71() V72() V73() Element of K19(REAL)
[.x0,r.] is closed V71() V72() V73() V104() Element of K19(REAL)
a is set
k is V30() real ext-real set
(dom ((f . r) (#) g)) /\ (dom ((g . r) (#) f)) is V71() V72() V73() Element of K19(REAL)
(((f . r) (#) g) - ((g . r) (#) f)) . r is V30() real ext-real Element of REAL
((f . r) (#) g) . r is V30() real ext-real Element of REAL
((g . r) (#) f) . r is V30() real ext-real Element of REAL
(((f . r) (#) g) . r) - (((g . r) (#) f) . r) is V30() real ext-real Element of REAL
(f . r) * (g . r) is V30() real ext-real Element of REAL
((f . r) * (g . r)) - (((g . r) (#) f) . r) is V30() real ext-real Element of REAL
(g . r) * (f . r) is V30() real ext-real Element of REAL
((g . r) * (f . r)) - ((g . r) * (f . r)) is V30() real ext-real Element of REAL
{x0} is non empty V71() V72() V73() set
[.x0,r.] \ {x0} is V71() V72() V73() Element of K19(REAL)
{ b₁ where b₁ is V30() real ext-real Element of REAL : ( not b₁ <= x0 & not x0 + N <= b₁ ) } is set
a is set
{ b₁ where b₁ is V30() real ext-real Element of REAL : ( not b₁ <= x0 & not r <= b₁ ) } is set
k is V30() real ext-real Element of REAL
{x0,r} is non empty V71() V72() V73() set
].x0,r.[ \/ {x0,r} is non empty V71() V72() V73() set
a is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total V35() V36() V37() Element of K19(K20(NAT,REAL))
rng a is V71() V72() V73() Element of K19(REAL)
lim a is V30() real ext-real Element of REAL
g /* a is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total V35() V36() V37() Element of K19(K20(NAT,REAL))
g . (lim a) is V30() real ext-real Element of REAL
lim (g /* a) is V30() real ext-real Element of REAL
g | [.x0,r.] is V1() V4( REAL ) V5( REAL ) V6() V35() V36() V37() Element of K19(K20(REAL,REAL))
((f . r) (#) g) | [.x0,r.] is V1() V4( REAL ) V5( REAL ) V6() V35() V36() V37() Element of K19(K20(REAL,REAL))
a is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total V35() V36() V37() Element of K19(K20(NAT,REAL))
rng a is V71() V72() V73() Element of K19(REAL)
lim a is V30() real ext-real Element of REAL
f /* a is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total V35() V36() V37() Element of K19(K20(NAT,REAL))
f . (lim a) is V30() real ext-real Element of REAL
lim (f /* a) is V30() real ext-real Element of REAL
f | [.x0,r.] is V1() V4( REAL ) V5( REAL ) V6() V35() V36() V37() Element of K19(K20(REAL,REAL))
((g . r) (#) f) | [.x0,r.] is V1() V4( REAL ) V5( REAL ) V6() V35() V36() V37() Element of K19(K20(REAL,REAL))
(((f . r) (#) g) - ((g . r) (#) f)) | [.x0,r.] is V1() V4( REAL ) V5( REAL ) V6() V35() V36() V37() Element of K19(K20(REAL,REAL))
(((f . r) (#) g) - ((g . r) (#) f)) . x0 is V30() real ext-real Element of REAL
((f . r) (#) g) . x0 is V30() real ext-real Element of REAL
((g . r) (#) f) . x0 is V30() real ext-real Element of REAL
(((f . r) (#) g) . x0) - (((g . r) (#) f) . x0) is V30() real ext-real Element of REAL
(f . r) * (g . x0) is V30() real ext-real Element of REAL
((f . r) * (g . x0)) - (((g . r) (#) f) . x0) is V30() real ext-real Element of REAL
(g . r) * 0 is V30() real ext-real Element of REAL
0 - ((g . r) * 0) is V30() real ext-real Element of REAL
a is V30() real ext-real Element of REAL
diff ((((f . r) (#) g) - ((g . r) (#) f)),a) is V30() real ext-real Element of REAL
diff (((f . r) (#) g),a) is V30() real ext-real Element of REAL
diff (((g . r) (#) f),a) is V30() real ext-real Element of REAL
(diff (((f . r) (#) g),a)) - (diff (((g . r) (#) f),a)) is V30() real ext-real Element of REAL
diff (f,a) is V30() real ext-real Element of REAL
(g . r) * (diff (f,a)) is V30() real ext-real Element of REAL
(diff (((f . r) (#) g),a)) - ((g . r) * (diff (f,a))) is V30() real ext-real Element of REAL
dom (f `| ].x0,(x0 + N).[) is V71() V72() V73() Element of K19(REAL)
dom (g `| ].x0,(x0 + N).[) is V71() V72() V73() Element of K19(REAL)
(g `| ].x0,(x0 + N).[) " {0} is V71() V72() V73() Element of K19(REAL)
(dom (g `| ].x0,(x0 + N).[)) \ ((g `| ].x0,(x0 + N).[) " {0}) is V71() V72() V73() Element of K19(REAL)
(dom (f `| ].x0,(x0 + N).[)) /\ ((dom (g `| ].x0,(x0 + N).[)) \ ((g `| ].x0,(x0 + N).[) " {0})) is V71() V72() V73() Element of K19(REAL)
g " {0} is V71() V72() V73() Element of K19(REAL)
(dom g) \ (g " {0}) is V71() V72() V73() Element of K19(REAL)
(dom f) /\ ((dom g) \ (g " {0})) is V71() V72() V73() Element of K19(REAL)
k is set
{ b₁ where b₁ is V30() real ext-real Element of REAL : ( x0 <= b₁ & b₁ <= r ) } is set
a1 is V30() real ext-real Element of REAL
((f `| ].x0,(x0 + N).[) / (g `| ].x0,(x0 + N).[)) . a is V30() real ext-real Element of REAL
{ b₁ where b₁ is V30() real ext-real Element of REAL : ( x0 <= b₁ & b₁ <= x0 + N ) } is set
diff (g,a) is V30() real ext-real Element of REAL
(g `| ].x0,(x0 + N).[) . a is V30() real ext-real Element of REAL
(f . r) * (diff (g,a)) is V30() real ext-real Element of REAL
((f . r) * (diff (g,a))) - ((g . r) * (diff (f,a))) is V30() real ext-real Element of REAL
(f . r) / (g . r) is V30() real ext-real Element of REAL
(diff (f,a)) / (diff (g,a)) is V30() real ext-real Element of REAL
(g . r) " is V30() real ext-real Element of REAL
(f . r) * ((g . r) ") is V30() real ext-real Element of REAL
(diff (g,a)) " is V30() real ext-real Element of REAL
(diff (f,a)) * ((diff (g,a)) ") is V30() real ext-real Element of REAL
(f `| ].x0,(x0 + N).[) . a is V30() real ext-real Element of REAL
((f `| ].x0,(x0 + N).[) . a) * ((diff (g,a)) ") is V30() real ext-real Element of REAL
((g `| ].x0,(x0 + N).[) . a) " is V30() real ext-real Element of REAL
((f `| ].x0,(x0 + N).[) . a) * (((g `| ].x0,(x0 + N).[) . a) ") is V30() real ext-real Element of REAL
right_open_halfline x0 is V71() V72() V73() Element of K19(REAL)
K195(x0,+infty) is set
(dom (f / g)) /\ (right_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
lim_right (((f `| ].x0,(x0 + N).[) / (g `| ].x0,(x0 + N).[)),x0) is V30() real ext-real Element of REAL
NAT --> x0 is V1() V4( NAT ) V5( REAL ) V6() constant non empty total quasi_total V35() V36() V37() convergent Element of K19(K20(NAT,REAL))
d is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total V35() V36() V37() Element of K19(K20(NAT,REAL))
lim d is V30() real ext-real Element of REAL
rng d is V71() V72() V73() Element of K19(REAL)
(f / g) /* d is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total V35() V36() V37() Element of K19(K20(NAT,REAL))
lim ((f / g) /* d) is V30() real ext-real Element of REAL
x0 - N is V30() real ext-real Element of REAL
a is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V71() V72() V73() V74() V75() V76() V93() V94() V101() Element of NAT
d ^\ a is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total V35() V36() V37() M7( REAL ,d)
((f / g) /* d) ^\ a is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total V35() V36() V37() M7( REAL ,(f / g) /* d)
a1 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V71() V72() V73() V74() V75() V76() V93() V94() V101() Element of NAT
a1 + a is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V71() V72() V73() V74() V75() V76() V93() V94() V101() Element of NAT
d . (a1 + a) is V30() real ext-real Element of REAL
{ b₁ where b₁ is V30() real ext-real Element of REAL : not b₁ <= x0 } is set
(d ^\ a) . a1 is V30() real ext-real Element of REAL
b is V30() real ext-real Element of REAL
a1 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V71() V72() V73() V74() V75() V76() V93() V94() V101() Element of NAT
(d ^\ a) . a1 is V30() real ext-real Element of REAL
].x0,((d ^\ a) . a1).[ is open V71() V72() V73() V99() V100() V104() Element of K19(REAL)
(((f / g) /* d) ^\ a) . a1 is V30() real ext-real Element of REAL
rng (d ^\ a) is V71() V72() V73() Element of K19(REAL)
(f / g) . ((d ^\ a) . a1) is V30() real ext-real Element of REAL
b is V30() real ext-real Element of REAL
((f `| ].x0,(x0 + N).[) / (g `| ].x0,(x0 + N).[)) . b is V30() real ext-real Element of REAL
(f / g) /* (d ^\ a) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total V35() V36() V37() Element of K19(K20(NAT,REAL))
((f / g) /* (d ^\ a)) . a1 is V30() real ext-real Element of REAL
a1 is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total V35() V36() V37() Element of K19(K20(NAT,REAL))
rng a1 is V71() V72() V73() Element of K19(REAL)
(dom ((f `| ].x0,(x0 + N).[) / (g `| ].x0,(x0 + N).[))) /\ (right_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
b is set
m is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V71() V72() V73() V74() V75() V76() V93() V94() V101() Element of NAT
a1 . m is V30() real ext-real Element of REAL
{ b₁ where b₁ is V30() real ext-real Element of REAL : ( x0 <= b₁ & b₁ <= x0 + N ) } is set
(d ^\ a) . m is V30() real ext-real Element of REAL
].x0,((d ^\ a) . m).[ is open V71() V72() V73() V99() V100() V104() Element of K19(REAL)
[.x0,((d ^\ a) . m).] is closed V71() V72() V73() V104() Element of K19(REAL)
{ b₁ where b₁ is V30() real ext-real Element of REAL : ( not b₁ <= x0 & not (d ^\ a) . m <= b₁ ) } is set
n is V30() real ext-real Element of REAL
b is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V71() V72() V73() V74() V75() V76() V93() V94() V101() Element of NAT
a1 . b is V30() real ext-real Element of REAL
(d ^\ a) . b is V30() real ext-real Element of REAL
].x0,((d ^\ a) . b).[ is open V71() V72() V73() V99() V100() V104() Element of K19(REAL)
{ b₁ where b₁ is V30() real ext-real Element of REAL : ( not b₁ <= x0 & not (d ^\ a) . b <= b₁ ) } is set
r is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total V35() V36() V37() Element of K19(K20(NAT,REAL))
r . b is V30() real ext-real Element of REAL
m is V30() real ext-real Element of REAL
lim r is V30() real ext-real Element of REAL
r . 0 is V30() real ext-real Element of REAL
lim (d ^\ a) is V30() real ext-real Element of REAL
lim a1 is V30() real ext-real Element of REAL
b is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() real ext-real V71() V72() V73() V74() V75() V76() V77() V93() V94() V101() V104() Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V71() V72() V73() V74() V75() V76() V93() V94() V101() Element of NAT
(((f / g) /* d) ^\ a) . m is V30() real ext-real Element of REAL
a1 . m is V30() real ext-real Element of REAL
((f `| ].x0,(x0 + N).[) / (g `| ].x0,(x0 + N).[)) . (a1 . m) is V30() real ext-real Element of REAL
((f `| ].x0,(x0 + N).[) / (g `| ].x0,(x0 + N).[)) /* a1 is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total V35() V36() V37() Element of K19(K20(NAT,REAL))
(((f `| ].x0,(x0 + N).[) / (g `| ].x0,(x0 + N).[)) /* a1) . m is V30() real ext-real Element of REAL
b is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() real ext-real V71() V72() V73() V74() V75() V76() V77() V93() V94() V101() V104() Element of NAT
lim (((f `| ].x0,(x0 + N).[) / (g `| ].x0,(x0 + N).[)) /* a1) is V30() real ext-real Element of REAL
lim (((f / g) /* d) ^\ a) is V30() real ext-real Element of REAL
b is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() real ext-real V71() V72() V73() V74() V75() V76() V77() V93() V94() V101() V104() Element of NAT
r is V30() real ext-real Element of REAL
f is V1() V4( REAL ) V5( REAL ) V6() V35() V36() V37() Element of K19(K20(REAL,REAL))
dom f is V71() V72() V73() Element of K19(REAL)
g is V1() V4( REAL ) V5( REAL ) V6() V35() V36() V37() Element of K19(K20(REAL,REAL))
dom g is V71() V72() V73() Element of K19(REAL)
(dom f) /\ (dom g) is V71() V72() V73() Element of K19(REAL)
f / g is V1() V4( REAL ) V5( REAL ) V6() V35() V36() V37() Element of K19(K20(REAL,REAL))
dom (f / g) is V71() V72() V73() Element of K19(REAL)
x0 is V30() real ext-real Element of REAL
f . x0 is V30() real ext-real Element of REAL
g . x0 is V30() real ext-real Element of REAL
lim_left ((f / g),x0) is V30() real ext-real Element of REAL
N is V30() real ext-real Element of REAL
x0 - N is V30() real ext-real Element of REAL
[.(x0 - N),x0.] is closed V71() V72() V73() V104() Element of K19(REAL)
].(x0 - N),x0.[ is open V71() V72() V73() V99() V100() V104() Element of K19(REAL)
f `| ].(x0 - N),x0.[ is V1() V4( REAL ) V5( REAL ) V6() V35() V36() V37() Element of K19(K20(REAL,REAL))
g `| ].(x0 - N),x0.[ is V1() V4( REAL ) V5( REAL ) V6() V35() V36() V37() Element of K19(K20(REAL,REAL))
(f `| ].(x0 - N),x0.[) / (g `| ].(x0 - N),x0.[) is V1() V4( REAL ) V5( REAL ) V6() V35() V36() V37() Element of K19(K20(REAL,REAL))
dom ((f `| ].(x0 - N),x0.[) / (g `| ].(x0 - N),x0.[)) is V71() V72() V73() Element of K19(REAL)
r is V30() real ext-real Element of REAL
].r,x0.[ is open V71() V72() V73() V99() V100() V104() Element of K19(REAL)
(f / g) . r is V30() real ext-real Element of REAL
{ b₁ where b₁ is V30() real ext-real Element of REAL : ( not b₁ <= x0 - N & not x0 <= b₁ ) } is set
{r,x0} is non empty V71() V72() V73() set
d is set
{ b₁ where b₁ is V30() real ext-real Element of REAL : ( not b₁ <= r & not x0 <= b₁ ) } is set
a is V30() real ext-real Element of REAL
].r,x0.[ \/ {r,x0} is non empty V71() V72() V73() set
[.r,x0.] is closed V71() V72() V73() V104() Element of K19(REAL)
f . r is V30() real ext-real Element of REAL
(f . r) (#) g is V1() V4( REAL ) V5( REAL ) V6() V35() V36() V37() Element of K19(K20(REAL,REAL))
dom ((f . r) (#) g) is V71() V72() V73() Element of K19(REAL)
g . r is V30() real ext-real Element of REAL
(g . r) (#) f is V1() V4( REAL ) V5( REAL ) V6() V35() V36() V37() Element of K19(K20(REAL,REAL))
dom ((g . r) (#) f) is V71() V72() V73() Element of K19(REAL)
(dom ((f . r) (#) g)) /\ (dom ((g . r) (#) f)) is V71() V72() V73() Element of K19(REAL)
((f . r) (#) g) - ((g . r) (#) f) is V1() V4( REAL ) V5( REAL ) V6() V35() V36() V37() Element of K19(K20(REAL,REAL))
dom (((f . r) (#) g) - ((g . r) (#) f)) is V71() V72() V73() Element of K19(REAL)
a is set
k is V30() real ext-real set
(((f . r) (#) g) - ((g . r) (#) f)) . r is V30() real ext-real Element of REAL
((f . r) (#) g) . r is V30() real ext-real Element of REAL
((g . r) (#) f) . r is V30() real ext-real Element of REAL
(((f . r) (#) g) . r) - (((g . r) (#) f) . r) is V30() real ext-real Element of REAL
(f . r) * (g . r) is V30() real ext-real Element of REAL
((f . r) * (g . r)) - (((g . r) (#) f) . r) is V30() real ext-real Element of REAL
(g . r) * (f . r) is V30() real ext-real Element of REAL
((g . r) * (f . r)) - ((g . r) * (f . r)) is V30() real ext-real Element of REAL
{x0} is non empty V71() V72() V73() set
[.r,x0.] \ {x0} is V71() V72() V73() Element of K19(REAL)
a is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total V35() V36() V37() Element of K19(K20(NAT,REAL))
rng a is V71() V72() V73() Element of K19(REAL)
lim a is V30() real ext-real Element of REAL
g /* a is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total V35() V36() V37() Element of K19(K20(NAT,REAL))
g . (lim a) is V30() real ext-real Element of REAL
lim (g /* a) is V30() real ext-real Element of REAL
g | [.r,x0.] is V1() V4( REAL ) V5( REAL ) V6() V35() V36() V37() Element of K19(K20(REAL,REAL))
((f . r) (#) g) | [.r,x0.] is V1() V4( REAL ) V5( REAL ) V6() V35() V36() V37() Element of K19(K20(REAL,REAL))
a is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total V35() V36() V37() Element of K19(K20(NAT,REAL))
rng a is V71() V72() V73() Element of K19(REAL)
lim a is V30() real ext-real Element of REAL
f /* a is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total V35() V36() V37() Element of K19(K20(NAT,REAL))
f . (lim a) is V30() real ext-real Element of REAL
lim (f /* a) is V30() real ext-real Element of REAL
f | [.r,x0.] is V1() V4( REAL ) V5( REAL ) V6() V35() V36() V37() Element of K19(K20(REAL,REAL))
((g . r) (#) f) | [.r,x0.] is V1() V4( REAL ) V5( REAL ) V6() V35() V36() V37() Element of K19(K20(REAL,REAL))
(((f . r) (#) g) - ((g . r) (#) f)) | [.r,x0.] is V1() V4( REAL ) V5( REAL ) V6() V35() V36() V37() Element of K19(K20(REAL,REAL))
(((f . r) (#) g) - ((g . r) (#) f)) . x0 is V30() real ext-real Element of REAL
((f . r) (#) g) . x0 is V30() real ext-real Element of REAL
((g . r) (#) f) . x0 is V30() real ext-real Element of REAL
(((f . r) (#) g) . x0) - (((g . r) (#) f) . x0) is V30() real ext-real Element of REAL
(f . r) * (g . x0) is V30() real ext-real Element of REAL
((f . r) * (g . x0)) - (((g . r) (#) f) . x0) is V30() real ext-real Element of REAL
(g . r) * 0 is V30() real ext-real Element of REAL
0 - ((g . r) * 0) is V30() real ext-real Element of REAL
a is V30() real ext-real Element of REAL
diff ((((f . r) (#) g) - ((g . r) (#) f)),a) is V30() real ext-real Element of REAL
diff (((f . r) (#) g),a) is V30() real ext-real Element of REAL
diff (((g . r) (#) f),a) is V30() real ext-real Element of REAL
(diff (((f . r) (#) g),a)) - (diff (((g . r) (#) f),a)) is V30() real ext-real Element of REAL
diff (f,a) is V30() real ext-real Element of REAL
(g . r) * (diff (f,a)) is V30() real ext-real Element of REAL
(diff (((f . r) (#) g),a)) - ((g . r) * (diff (f,a))) is V30() real ext-real Element of REAL
dom (f `| ].(x0 - N),x0.[) is V71() V72() V73() Element of K19(REAL)
dom (g `| ].(x0 - N),x0.[) is V71() V72() V73() Element of K19(REAL)
(g `| ].(x0 - N),x0.[) " {0} is V71() V72() V73() Element of K19(REAL)
(dom (g `| ].(x0 - N),x0.[)) \ ((g `| ].(x0 - N),x0.[) " {0}) is V71() V72() V73() Element of K19(REAL)
(dom (f `| ].(x0 - N),x0.[)) /\ ((dom (g `| ].(x0 - N),x0.[)) \ ((g `| ].(x0 - N),x0.[) " {0})) is V71() V72() V73() Element of K19(REAL)
g " {0} is V71() V72() V73() Element of K19(REAL)
(dom g) \ (g " {0}) is V71() V72() V73() Element of K19(REAL)
(dom f) /\ ((dom g) \ (g " {0})) is V71() V72() V73() Element of K19(REAL)
k is set
{ b₁ where b₁ is V30() real ext-real Element of REAL : ( r <= b₁ & b₁ <= x0 ) } is set
a1 is V30() real ext-real Element of REAL
((f `| ].(x0 - N),x0.[) / (g `| ].(x0 - N),x0.[)) . a is V30() real ext-real Element of REAL
{ b₁ where b₁ is V30() real ext-real Element of REAL : ( x0 - N <= b₁ & b₁ <= x0 ) } is set
diff (g,a) is V30() real ext-real Element of REAL
(g `| ].(x0 - N),x0.[) . a is V30() real ext-real Element of REAL
(f . r) * (diff (g,a)) is V30() real ext-real Element of REAL
((f . r) * (diff (g,a))) - ((g . r) * (diff (f,a))) is V30() real ext-real Element of REAL
(f . r) / (g . r) is V30() real ext-real Element of REAL
(diff (f,a)) / (diff (g,a)) is V30() real ext-real Element of REAL
(g . r) " is V30() real ext-real Element of REAL
(f . r) * ((g . r) ") is V30() real ext-real Element of REAL
(diff (g,a)) " is V30() real ext-real Element of REAL
(diff (f,a)) * ((diff (g,a)) ") is V30() real ext-real Element of REAL
(f `| ].(x0 - N),x0.[) . a is V30() real ext-real Element of REAL
((f `| ].(x0 - N),x0.[) . a) * ((diff (g,a)) ") is V30() real ext-real Element of REAL
((g `| ].(x0 - N),x0.[) . a) " is V30() real ext-real Element of REAL
((f `| ].(x0 - N),x0.[) . a) * (((g `| ].(x0 - N),x0.[) . a) ") is V30() real ext-real Element of REAL
left_open_halfline x0 is V71() V72() V73() Element of K19(REAL)
K195(-infty,x0) is set
(dom (f / g)) /\ (left_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
lim_left (((f `| ].(x0 - N),x0.[) / (g `| ].(x0 - N),x0.[)),x0) is V30() real ext-real Element of REAL
NAT --> x0 is V1() V4( NAT ) V5( REAL ) V6() constant non empty total quasi_total V35() V36() V37() convergent Element of K19(K20(NAT,REAL))
d is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total V35() V36() V37() Element of K19(K20(NAT,REAL))
lim d is V30() real ext-real Element of REAL
rng d is V71() V72() V73() Element of K19(REAL)
(f / g) /* d is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total V35() V36() V37() Element of K19(K20(NAT,REAL))
lim ((f / g) /* d) is V30() real ext-real Element of REAL
x0 + N is V30() real ext-real Element of REAL
a is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V71() V72() V73() V74() V75() V76() V93() V94() V101() Element of NAT
d ^\ a is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total V35() V36() V37() M7( REAL ,d)
((f / g) /* d) ^\ a is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total V35() V36() V37() M7( REAL ,(f / g) /* d)
a1 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V71() V72() V73() V74() V75() V76() V93() V94() V101() Element of NAT
a1 + a is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V71() V72() V73() V74() V75() V76() V93() V94() V101() Element of NAT
d . (a1 + a) is V30() real ext-real Element of REAL
{ b₁ where b₁ is V30() real ext-real Element of REAL : not x0 <= b₁ } is set
(d ^\ a) . a1 is V30() real ext-real Element of REAL
b is V30() real ext-real Element of REAL
a1 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V71() V72() V73() V74() V75() V76() V93() V94() V101() Element of NAT
(d ^\ a) . a1 is V30() real ext-real Element of REAL
].((d ^\ a) . a1),x0.[ is open V71() V72() V73() V99() V100() V104() Element of K19(REAL)
(((f / g) /* d) ^\ a) . a1 is V30() real ext-real Element of REAL
rng (d ^\ a) is V71() V72() V73() Element of K19(REAL)
(f / g) . ((d ^\ a) . a1) is V30() real ext-real Element of REAL
b is V30() real ext-real Element of REAL
((f `| ].(x0 - N),x0.[) / (g `| ].(x0 - N),x0.[)) . b is V30() real ext-real Element of REAL
(f / g) /* (d ^\ a) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total V35() V36() V37() Element of K19(K20(NAT,REAL))
((f / g) /* (d ^\ a)) . a1 is V30() real ext-real Element of REAL
a1 is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total V35() V36() V37() Element of K19(K20(NAT,REAL))
rng a1 is V71() V72() V73() Element of K19(REAL)
(dom ((f `| ].(x0 - N),x0.[) / (g `| ].(x0 - N),x0.[))) /\ (left_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
b is set
m is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V71() V72() V73() V74() V75() V76() V93() V94() V101() Element of NAT
a1 . m is V30() real ext-real Element of REAL
{ b₁ where b₁ is V30() real ext-real Element of REAL : ( x0 - N <= b₁ & b₁ <= x0 ) } is set
(d ^\ a) . m is V30() real ext-real Element of REAL
].((d ^\ a) . m),x0.[ is open V71() V72() V73() V99() V100() V104() Element of K19(REAL)
[.((d ^\ a) . m),x0.] is closed V71() V72() V73() V104() Element of K19(REAL)
{ b₁ where b₁ is V30() real ext-real Element of REAL : ( not b₁ <= (d ^\ a) . m & not x0 <= b₁ ) } is set
n is V30() real ext-real Element of REAL
b is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V71() V72() V73() V74() V75() V76() V93() V94() V101() Element of NAT
a1 . b is V30() real ext-real Element of REAL
(d ^\ a) . b is V30() real ext-real Element of REAL
].((d ^\ a) . b),x0.[ is open V71() V72() V73() V99() V100() V104() Element of K19(REAL)
{ b₁ where b₁ is V30() real ext-real Element of REAL : ( not b₁ <= (d ^\ a) . b & not x0 <= b₁ ) } is set
r is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total V35() V36() V37() Element of K19(K20(NAT,REAL))
r . b is V30() real ext-real Element of REAL
m is V30() real ext-real Element of REAL
lim r is V30() real ext-real Element of REAL
r . 0 is V30() real ext-real Element of REAL
lim (d ^\ a) is V30() real ext-real Element of REAL
lim a1 is V30() real ext-real Element of REAL
b is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() real ext-real V71() V72() V73() V74() V75() V76() V77() V93() V94() V101() V104() Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V71() V72() V73() V74() V75() V76() V93() V94() V101() Element of NAT
(((f / g) /* d) ^\ a) . m is V30() real ext-real Element of REAL
a1 . m is V30() real ext-real Element of REAL
((f `| ].(x0 - N),x0.[) / (g `| ].(x0 - N),x0.[)) . (a1 . m) is V30() real ext-real Element of REAL
((f `| ].(x0 - N),x0.[) / (g `| ].(x0 - N),x0.[)) /* a1 is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total V35() V36() V37() Element of K19(K20(NAT,REAL))
(((f `| ].(x0 - N),x0.[) / (g `| ].(x0 - N),x0.[)) /* a1) . m is V30() real ext-real Element of REAL
b is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() real ext-real V71() V72() V73() V74() V75() V76() V77() V93() V94() V101() V104() Element of NAT
lim (((f `| ].(x0 - N),x0.[) / (g `| ].(x0 - N),x0.[)) /* a1) is V30() real ext-real Element of REAL
lim (((f / g) /* d) ^\ a) is V30() real ext-real Element of REAL
b is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() real ext-real V71() V72() V73() V74() V75() V76() V77() V93() V94() V101() V104() Element of NAT
r is V30() real ext-real Element of REAL
f is V1() V4( REAL ) V5( REAL ) V6() V35() V36() V37() Element of K19(K20(REAL,REAL))
dom f is V71() V72() V73() Element of K19(REAL)
g is V1() V4( REAL ) V5( REAL ) V6() V35() V36() V37() Element of K19(K20(REAL,REAL))
dom g is V71() V72() V73() Element of K19(REAL)
f / g is V1() V4( REAL ) V5( REAL ) V6() V35() V36() V37() Element of K19(K20(REAL,REAL))
dom (f / g) is V71() V72() V73() Element of K19(REAL)
x0 is V30() real ext-real Element of REAL
{x0} is non empty V71() V72() V73() set
f . x0 is V30() real ext-real Element of REAL
g . x0 is V30() real ext-real Element of REAL
lim ((f / g),x0) is V30() real ext-real Element of REAL
N is open V71() V72() V73() Neighbourhood of x0
N \ {x0} is V71() V72() V73() Element of K19(REAL)
f `| N is V1() V4( REAL ) V5( REAL ) V6() V35() V36() V37() Element of K19(K20(REAL,REAL))
g `| N is V1() V4( REAL ) V5( REAL ) V6() V35() V36() V37() Element of K19(K20(REAL,REAL))
(f `| N) / (g `| N) is V1() V4( REAL ) V5( REAL ) V6() V35() V36() V37() Element of K19(K20(REAL,REAL))
dom ((f `| N) / (g `| N)) is V71() V72() V73() Element of K19(REAL)
r is V30() real ext-real set
x0 - r is V30() real ext-real Element of REAL
x0 + r is V30() real ext-real Element of REAL
].(x0 - r),(x0 + r).[ is open V71() V72() V73() V99() V100() V104() Element of K19(REAL)
x0 + 0 is V30() real ext-real Element of REAL
{ b₁ where b₁ is V30() real ext-real Element of REAL : ( not b₁ <= x0 - r & not x0 + r <= b₁ ) } is set
dom (f `| N) is V71() V72() V73() Element of K19(REAL)
dom (g `| N) is V71() V72() V73() Element of K19(REAL)
(g `| N) " {0} is V71() V72() V73() Element of K19(REAL)
(dom (g `| N)) \ ((g `| N) " {0}) is V71() V72() V73() Element of K19(REAL)
(dom (f `| N)) /\ ((dom (g `| N)) \ ((g `| N) " {0})) is V71() V72() V73() Element of K19(REAL)
g " {0} is V71() V72() V73() Element of K19(REAL)
(dom g) \ (g " {0}) is V71() V72() V73() Element of K19(REAL)
(dom f) /\ ((dom g) \ (g " {0})) is V71() V72() V73() Element of K19(REAL)
d is V30() real ext-real Element of REAL
].x0,d.[ is open V71() V72() V73() V99() V100() V104() Element of K19(REAL)
(f / g) . d is V30() real ext-real Element of REAL
f . d is V30() real ext-real Element of REAL
(f . d) (#) g is V1() V4( REAL ) V5( REAL ) V6() V35() V36() V37() Element of K19(K20(REAL,REAL))
g . d is V30() real ext-real Element of REAL
(g . d) (#) f is V1() V4( REAL ) V5( REAL ) V6() V35() V36() V37() Element of K19(K20(REAL,REAL))
((f . d) (#) g) - ((g . d) (#) f) is V1() V4( REAL ) V5( REAL ) V6() V35() V36() V37() Element of K19(K20(REAL,REAL))
dom ((f . d) (#) g) is V71() V72() V73() Element of K19(REAL)
dom ((g . d) (#) f) is V71() V72() V73() Element of K19(REAL)
dom (((f . d) (#) g) - ((g . d) (#) f)) is V71() V72() V73() Element of K19(REAL)
(dom f) /\ (dom g) is V71() V72() V73() Element of K19(REAL)
[.x0,d.] is closed V71() V72() V73() V104() Element of K19(REAL)
g | N is V1() V4( REAL ) V5( REAL ) V6() V35() V36() V37() Element of K19(K20(REAL,REAL))
g | [.x0,d.] is V1() V4( REAL ) V5( REAL ) V6() V35() V36() V37() Element of K19(K20(REAL,REAL))
((f . d) (#) g) | [.x0,d.] is V1() V4( REAL ) V5( REAL ) V6() V35() V36() V37() Element of K19(K20(REAL,REAL))
f | N is V1() V4( REAL ) V5( REAL ) V6() V35() V36() V37() Element of K19(K20(REAL,REAL))
f | [.x0,d.] is V1() V4( REAL ) V5( REAL ) V6() V35() V36() V37() Element of K19(K20(REAL,REAL))
((g . d) (#) f) | [.x0,d.] is V1() V4( REAL ) V5( REAL ) V6() V35() V36() V37() Element of K19(K20(REAL,REAL))
(((f . d) (#) g) - ((g . d) (#) f)) | [.x0,d.] is V1() V4( REAL ) V5( REAL ) V6() V35() V36() V37() Element of K19(K20(REAL,REAL))
(dom ((f . d) (#) g)) /\ (dom ((g . d) (#) f)) is V71() V72() V73() Element of K19(REAL)
(((f . d) (#) g) - ((g . d) (#) f)) . d is V30() real ext-real Element of REAL
((f . d) (#) g) . d is V30() real ext-real Element of REAL
((g . d) (#) f) . d is V30() real ext-real Element of REAL
(((f . d) (#) g) . d) - (((g . d) (#) f) . d) is V30() real ext-real Element of REAL
(f . d) * (g . d) is V30() real ext-real Element of REAL
((f . d) * (g . d)) - (((g . d) (#) f) . d) is V30() real ext-real Element of REAL
(g . d) * (f . d) is V30() real ext-real Element of REAL
((g . d) * (f . d)) - ((g . d) * (f . d)) is V30() real ext-real Element of REAL
[.x0,d.] \ {x0} is V71() V72() V73() Element of K19(REAL)
(((f . d) (#) g) - ((g . d) (#) f)) . x0 is V30() real ext-real Element of REAL
((f . d) (#) g) . x0 is V30() real ext-real Element of REAL
((g . d) (#) f) . x0 is V30() real ext-real Element of REAL
(((f . d) (#) g) . x0) - (((g . d) (#) f) . x0) is V30() real ext-real Element of REAL
(f . d) * (g . x0) is V30() real ext-real Element of REAL
((f . d) * (g . x0)) - (((g . d) (#) f) . x0) is V30() real ext-real Element of REAL
(g . d) * 0 is V30() real ext-real Element of REAL
0 - ((g . d) * 0) is V30() real ext-real Element of REAL
k is V30() real ext-real Element of REAL
diff ((((f . d) (#) g) - ((g . d) (#) f)),k) is V30() real ext-real Element of REAL
diff (((f . d) (#) g),k) is V30() real ext-real Element of REAL
diff (((g . d) (#) f),k) is V30() real ext-real Element of REAL
(diff (((f . d) (#) g),k)) - (diff (((g . d) (#) f),k)) is V30() real ext-real Element of REAL
diff (f,k) is V30() real ext-real Element of REAL
(g . d) * (diff (f,k)) is V30() real ext-real Element of REAL
(diff (((f . d) (#) g),k)) - ((g . d) * (diff (f,k))) is V30() real ext-real Element of REAL
((f `| N) / (g `| N)) . k is V30() real ext-real Element of REAL
diff (g,k) is V30() real ext-real Element of REAL
(g `| N) . k is V30() real ext-real Element of REAL
(f . d) * (diff (g,k)) is V30() real ext-real Element of REAL
((f . d) * (diff (g,k))) - ((g . d) * (diff (f,k))) is V30() real ext-real Element of REAL
(f . d) / (g . d) is V30() real ext-real Element of REAL
(diff (f,k)) / (diff (g,k)) is V30() real ext-real Element of REAL
(g . d) " is V30() real ext-real Element of REAL
(f . d) * ((g . d) ") is V30() real ext-real Element of REAL
(diff (g,k)) " is V30() real ext-real Element of REAL
(diff (f,k)) * ((diff (g,k)) ") is V30() real ext-real Element of REAL
(f `| N) . k is V30() real ext-real Element of REAL
((f `| N) . k) * ((diff (g,k)) ") is V30() real ext-real Element of REAL
((g `| N) . k) " is V30() real ext-real Element of REAL
((f `| N) . k) * (((g `| N) . k) ") is V30() real ext-real Element of REAL
right_open_halfline x0 is V71() V72() V73() Element of K19(REAL)
K195(x0,+infty) is set
(dom (f / g)) /\ (right_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
lim (((f `| N) / (g `| N)),x0) is V30() real ext-real Element of REAL
NAT --> x0 is V1() V4( NAT ) V5( REAL ) V6() constant non empty total quasi_total V35() V36() V37() convergent Element of K19(K20(NAT,REAL))
a is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total V35() V36() V37() Element of K19(K20(NAT,REAL))
lim a is V30() real ext-real Element of REAL
rng a is V71() V72() V73() Element of K19(REAL)
(f / g) /* a is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total V35() V36() V37() Element of K19(K20(NAT,REAL))
lim ((f / g) /* a) is V30() real ext-real Element of REAL
k is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V71() V72() V73() V74() V75() V76() V93() V94() V101() Element of NAT
a ^\ k is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total V35() V36() V37() M7( REAL ,a)
((f / g) /* a) ^\ k is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total V35() V36() V37() M7( REAL ,(f / g) /* a)
b is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V71() V72() V73() V74() V75() V76() V93() V94() V101() Element of NAT
b + k is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V71() V72() V73() V74() V75() V76() V93() V94() V101() Element of NAT
a . (b + k) is V30() real ext-real Element of REAL
{ b₁ where b₁ is V30() real ext-real Element of REAL : not b₁ <= x0 } is set
(a ^\ k) . b is V30() real ext-real Element of REAL
m is V30() real ext-real Element of REAL
b is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V71() V72() V73() V74() V75() V76() V93() V94() V101() Element of NAT
(a ^\ k) . b is V30() real ext-real Element of REAL
].x0,((a ^\ k) . b).[ is open V71() V72() V73() V99() V100() V104() Element of K19(REAL)
(((f / g) /* a) ^\ k) . b is V30() real ext-real Element of REAL
rng (a ^\ k) is V71() V72() V73() Element of K19(REAL)
(f / g) . ((a ^\ k) . b) is V30() real ext-real Element of REAL
m is V30() real ext-real Element of REAL
((f `| N) / (g `| N)) . m is V30() real ext-real Element of REAL
(f / g) /* (a ^\ k) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total V35() V36() V37() Element of K19(K20(NAT,REAL))
((f / g) /* (a ^\ k)) . b is V30() real ext-real Element of REAL
b is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total V35() V36() V37() Element of K19(K20(NAT,REAL))
m is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V71() V72() V73() V74() V75() V76() V93() V94() V101() Element of NAT
b . m is V30() real ext-real Element of REAL
(a ^\ k) . m is V30() real ext-real Element of REAL
].x0,((a ^\ k) . m).[ is open V71() V72() V73() V99() V100() V104() Element of K19(REAL)
{ b₁ where b₁ is V30() real ext-real Element of REAL : ( not b₁ <= x0 & not (a ^\ k) . m <= b₁ ) } is set
d is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total V35() V36() V37() Element of K19(K20(NAT,REAL))
d . m is V30() real ext-real Element of REAL
n is V30() real ext-real Element of REAL
lim d is V30() real ext-real Element of REAL
d . 0 is V30() real ext-real Element of REAL
lim (a ^\ k) is V30() real ext-real Element of REAL
lim b is V30() real ext-real Element of REAL
{ b₁ where b₁ is V30() real ext-real Element of REAL : ( not b₁ <= x0 - r & not x0 + r <= b₁ ) } is set
rng b is V71() V72() V73() Element of K19(REAL)
(dom ((f `| N) / (g `| N))) \ {x0} is V71() V72() V73() Element of K19(REAL)
m is set
n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V71() V72() V73() V74() V75() V76() V93() V94() V101() Element of NAT
b . n is V30() real ext-real Element of REAL
(a ^\ k) . n is V30() real ext-real Element of REAL
].x0,((a ^\ k) . n).[ is open V71() V72() V73() V99() V100() V104() Element of K19(REAL)
[.x0,((a ^\ k) . n).] is closed V71() V72() V73() V104() Element of K19(REAL)
{ b₁ where b₁ is V30() real ext-real Element of REAL : ( not b₁ <= x0 & not (a ^\ k) . n <= b₁ ) } is set
c₁₃ is V30() real ext-real Element of REAL
m is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() real ext-real V71() V72() V73() V74() V75() V76() V77() V93() V94() V101() V104() Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V71() V72() V73() V74() V75() V76() V93() V94() V101() Element of NAT
(((f / g) /* a) ^\ k) . n is V30() real ext-real Element of REAL
b . n is V30() real ext-real Element of REAL
((f `| N) / (g `| N)) . (b . n) is V30() real ext-real Element of REAL
((f `| N) / (g `| N)) /* b is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total V35() V36() V37() Element of K19(K20(NAT,REAL))
(((f `| N) / (g `| N)) /* b) . n is V30() real ext-real Element of REAL
m is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() real ext-real V71() V72() V73() V74() V75() V76() V77() V93() V94() V101() V104() Element of NAT
lim (((f `| N) / (g `| N)) /* b) is V30() real ext-real Element of REAL
lim (((f / g) /* a) ^\ k) is V30() real ext-real Element of REAL
m is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() real ext-real V71() V72() V73() V74() V75() V76() V77() V93() V94() V101() V104() Element of NAT
d is V30() real ext-real Element of REAL
a is V30() real ext-real Element of REAL
d is V30() real ext-real Element of REAL
lim_right ((f / g),x0) is V30() real ext-real Element of REAL
x0 + 0 is V30() real ext-real Element of REAL
{ b₁ where b₁ is V30() real ext-real Element of REAL : ( not b₁ <= x0 - r & not x0 + r <= b₁ ) } is set
dom (f `| N) is V71() V72() V73() Element of K19(REAL)
dom (g `| N) is V71() V72() V73() Element of K19(REAL)
(g `| N) " {0} is V71() V72() V73() Element of K19(REAL)
(dom (g `| N)) \ ((g `| N) " {0}) is V71() V72() V73() Element of K19(REAL)
(dom (f `| N)) /\ ((dom (g `| N)) \ ((g `| N) " {0})) is V71() V72() V73() Element of K19(REAL)
g " {0} is V71() V72() V73() Element of K19(REAL)
(dom g) \ (g " {0}) is V71() V72() V73() Element of K19(REAL)
(dom f) /\ ((dom g) \ (g " {0})) is V71() V72() V73() Element of K19(REAL)
d is V30() real ext-real Element of REAL
].d,x0.[ is open V71() V72() V73() V99() V100() V104() Element of K19(REAL)
(f / g) . d is V30() real ext-real Element of REAL
f . d is V30() real ext-real Element of REAL
(f . d) (#) g is V1() V4( REAL ) V5( REAL ) V6() V35() V36() V37() Element of K19(K20(REAL,REAL))
g . d is V30() real ext-real Element of REAL
(g . d) (#) f is V1() V4( REAL ) V5( REAL ) V6() V35() V36() V37() Element of K19(K20(REAL,REAL))
((f . d) (#) g) - ((g . d) (#) f) is V1() V4( REAL ) V5( REAL ) V6() V35() V36() V37() Element of K19(K20(REAL,REAL))
dom ((f . d) (#) g) is V71() V72() V73() Element of K19(REAL)
dom ((g . d) (#) f) is V71() V72() V73() Element of K19(REAL)
dom (((f . d) (#) g) - ((g . d) (#) f)) is V71() V72() V73() Element of K19(REAL)
(dom f) /\ (dom g) is V71() V72() V73() Element of K19(REAL)
[.d,x0.] is closed V71() V72() V73() V104() Element of K19(REAL)
g | N is V1() V4( REAL ) V5( REAL ) V6() V35() V36() V37() Element of K19(K20(REAL,REAL))
g | [.d,x0.] is V1() V4( REAL ) V5( REAL ) V6() V35() V36() V37() Element of K19(K20(REAL,REAL))
((f . d) (#) g) | [.d,x0.] is V1() V4( REAL ) V5( REAL ) V6() V35() V36() V37() Element of K19(K20(REAL,REAL))
f | N is V1() V4( REAL ) V5( REAL ) V6() V35() V36() V37() Element of K19(K20(REAL,REAL))
f | [.d,x0.] is V1() V4( REAL ) V5( REAL ) V6() V35() V36() V37() Element of K19(K20(REAL,REAL))
((g . d) (#) f) | [.d,x0.] is V1() V4( REAL ) V5( REAL ) V6() V35() V36() V37() Element of K19(K20(REAL,REAL))
(((f . d) (#) g) - ((g . d) (#) f)) | [.d,x0.] is V1() V4( REAL ) V5( REAL ) V6() V35() V36() V37() Element of K19(K20(REAL,REAL))
(dom ((f . d) (#) g)) /\ (dom ((g . d) (#) f)) is V71() V72() V73() Element of K19(REAL)
(((f . d) (#) g) - ((g . d) (#) f)) . d is V30() real ext-real Element of REAL
((f . d) (#) g) . d is V30() real ext-real Element of REAL
((g . d) (#) f) . d is V30() real ext-real Element of REAL
(((f . d) (#) g) . d) - (((g . d) (#) f) . d) is V30() real ext-real Element of REAL
(f . d) * (g . d) is V30() real ext-real Element of REAL
((f . d) * (g . d)) - (((g . d) (#) f) . d) is V30() real ext-real Element of REAL
(g . d) * (f . d) is V30() real ext-real Element of REAL
((g . d) * (f . d)) - ((g . d) * (f . d)) is V30() real ext-real Element of REAL
[.d,x0.] \ {x0} is V71() V72() V73() Element of K19(REAL)
(((f . d) (#) g) - ((g . d) (#) f)) . x0 is V30() real ext-real Element of REAL
((f . d) (#) g) . x0 is V30() real ext-real Element of REAL
((g . d) (#) f) . x0 is V30() real ext-real Element of REAL
(((f . d) (#) g) . x0) - (((g . d) (#) f) . x0) is V30() real ext-real Element of REAL
(f . d) * (g . x0) is V30() real ext-real Element of REAL
((f . d) * (g . x0)) - (((g . d) (#) f) . x0) is V30() real ext-real Element of REAL
(g . d) * 0 is V30() real ext-real Element of REAL
0 - ((g . d) * 0) is V30() real ext-real Element of REAL
k is V30() real ext-real Element of REAL
diff ((((f . d) (#) g) - ((g . d) (#) f)),k) is V30() real ext-real Element of REAL
diff (((f . d) (#) g),k) is V30() real ext-real Element of REAL
diff (((g . d) (#) f),k) is V30() real ext-real Element of REAL
(diff (((f . d) (#) g),k)) - (diff (((g . d) (#) f),k)) is V30() real ext-real Element of REAL
diff (f,k) is V30() real ext-real Element of REAL
(g . d) * (diff (f,k)) is V30() real ext-real Element of REAL
(diff (((f . d) (#) g),k)) - ((g . d) * (diff (f,k))) is V30() real ext-real Element of REAL
((f `| N) / (g `| N)) . k is V30() real ext-real Element of REAL
diff (g,k) is V30() real ext-real Element of REAL
(g `| N) . k is V30() real ext-real Element of REAL
(f . d) * (diff (g,k)) is V30() real ext-real Element of REAL
((f . d) * (diff (g,k))) - ((g . d) * (diff (f,k))) is V30() real ext-real Element of REAL
(f . d) / (g . d) is V30() real ext-real Element of REAL
(diff (f,k)) / (diff (g,k)) is V30() real ext-real Element of REAL
(g . d) " is V30() real ext-real Element of REAL
(f . d) * ((g . d) ") is V30() real ext-real Element of REAL
(diff (g,k)) " is V30() real ext-real Element of REAL
(diff (f,k)) * ((diff (g,k)) ") is V30() real ext-real Element of REAL
(f `| N) . k is V30() real ext-real Element of REAL
((f `| N) . k) * ((diff (g,k)) ") is V30() real ext-real Element of REAL
((g `| N) . k) " is V30() real ext-real Element of REAL
((f `| N) . k) * (((g `| N) . k) ") is V30() real ext-real Element of REAL
left_open_halfline x0 is V71() V72() V73() Element of K19(REAL)
K195(-infty,x0) is set
(dom (f / g)) /\ (left_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
NAT --> x0 is V1() V4( NAT ) V5( REAL ) V6() constant non empty total quasi_total V35() V36() V37() convergent Element of K19(K20(NAT,REAL))
a is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total V35() V36() V37() Element of K19(K20(NAT,REAL))
lim a is V30() real ext-real Element of REAL
rng a is V71() V72() V73() Element of K19(REAL)
(f / g) /* a is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total V35() V36() V37() Element of K19(K20(NAT,REAL))
lim ((f / g) /* a) is V30() real ext-real Element of REAL
k is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V71() V72() V73() V74() V75() V76() V93() V94() V101() Element of NAT
a ^\ k is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total V35() V36() V37() M7( REAL ,a)
((f / g) /* a) ^\ k is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total V35() V36() V37() M7( REAL ,(f / g) /* a)
b is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V71() V72() V73() V74() V75() V76() V93() V94() V101() Element of NAT
b + k is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V71() V72() V73() V74() V75() V76() V93() V94() V101() Element of NAT
a . (b + k) is V30() real ext-real Element of REAL
{ b₁ where b₁ is V30() real ext-real Element of REAL : not x0 <= b₁ } is set
(a ^\ k) . b is V30() real ext-real Element of REAL
m is V30() real ext-real Element of REAL
b is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V71() V72() V73() V74() V75() V76() V93() V94() V101() Element of NAT
(a ^\ k) . b is V30() real ext-real Element of REAL
].((a ^\ k) . b),x0.[ is open V71() V72() V73() V99() V100() V104() Element of K19(REAL)
(((f / g) /* a) ^\ k) . b is V30() real ext-real Element of REAL
rng (a ^\ k) is V71() V72() V73() Element of K19(REAL)
(f / g) . ((a ^\ k) . b) is V30() real ext-real Element of REAL
m is V30() real ext-real Element of REAL
((f `| N) / (g `| N)) . m is V30() real ext-real Element of REAL
(f / g) /* (a ^\ k) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total V35() V36() V37() Element of K19(K20(NAT,REAL))
((f / g) /* (a ^\ k)) . b is V30() real ext-real Element of REAL
b is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total V35() V36() V37() Element of K19(K20(NAT,REAL))
m is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V71() V72() V73() V74() V75() V76() V93() V94() V101() Element of NAT
b . m is V30() real ext-real Element of REAL
(a ^\ k) . m is V30() real ext-real Element of REAL
].((a ^\ k) . m),x0.[ is open V71() V72() V73() V99() V100() V104() Element of K19(REAL)
{ b₁ where b₁ is V30() real ext-real Element of REAL : ( not b₁ <= (a ^\ k) . m & not x0 <= b₁ ) } is set
d is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total V35() V36() V37() Element of K19(K20(NAT,REAL))
d . m is V30() real ext-real Element of REAL
n is V30() real ext-real Element of REAL
lim d is V30() real ext-real Element of REAL
d . 0 is V30() real ext-real Element of REAL
lim (a ^\ k) is V30() real ext-real Element of REAL
lim b is V30() real ext-real Element of REAL
{ b₁ where b₁ is V30() real ext-real Element of REAL : ( not b₁ <= x0 - r & not x0 + r <= b₁ ) } is set
rng b is V71() V72() V73() Element of K19(REAL)
(dom ((f `| N) / (g `| N))) \ {x0} is V71() V72() V73() Element of K19(REAL)
m is set
n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V71() V72() V73() V74() V75() V76() V93() V94() V101() Element of NAT
b . n is V30() real ext-real Element of REAL
(a ^\ k) . n is V30() real ext-real Element of REAL
].((a ^\ k) . n),x0.[ is open V71() V72() V73() V99() V100() V104() Element of K19(REAL)
[.((a ^\ k) . n),x0.] is closed V71() V72() V73() V104() Element of K19(REAL)
{ b₁ where b₁ is V30() real ext-real Element of REAL : ( not b₁ <= (a ^\ k) . n & not x0 <= b₁ ) } is set
c₁₃ is V30() real ext-real Element of REAL
m is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() real ext-real V71() V72() V73() V74() V75() V76() V77() V93() V94() V101() V104() Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V71() V72() V73() V74() V75() V76() V93() V94() V101() Element of NAT
(((f / g) /* a) ^\ k) . n is V30() real ext-real Element of REAL
b . n is V30() real ext-real Element of REAL
((f `| N) / (g `| N)) . (b . n) is V30() real ext-real Element of REAL
((f `| N) / (g `| N)) /* b is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total V35() V36() V37() Element of K19(K20(NAT,REAL))
(((f `| N) / (g `| N)) /* b) . n is V30() real ext-real Element of REAL
m is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() real ext-real V71() V72() V73() V74() V75() V76() V77() V93() V94() V101() V104() Element of NAT
lim (((f `| N) / (g `| N)) /* b) is V30() real ext-real Element of REAL
lim (((f / g) /* a) ^\ k) is V30() real ext-real Element of REAL
m is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() real ext-real V71() V72() V73() V74() V75() V76() V77() V93() V94() V101() V104() Element of NAT
d is V30() real ext-real Element of REAL
lim_left ((f / g),x0) is V30() real ext-real Element of REAL
f is V1() V4( REAL ) V5( REAL ) V6() V35() V36() V37() Element of K19(K20(REAL,REAL))
dom f is V71() V72() V73() Element of K19(REAL)
g is V1() V4( REAL ) V5( REAL ) V6() V35() V36() V37() Element of K19(K20(REAL,REAL))
dom g is V71() V72() V73() Element of K19(REAL)
f / g is V1() V4( REAL ) V5( REAL ) V6() V35() V36() V37() Element of K19(K20(REAL,REAL))
dom (f / g) is V71() V72() V73() Element of K19(REAL)
x0 is V30() real ext-real Element of REAL
{x0} is non empty V71() V72() V73() set
f . x0 is V30() real ext-real Element of REAL
g . x0 is V30() real ext-real Element of REAL
lim ((f / g),x0) is V30() real ext-real Element of REAL
diff (f,x0) is V30() real ext-real Element of REAL
diff (g,x0) is V30() real ext-real Element of REAL
(diff (f,x0)) / (diff (g,x0)) is V30() real ext-real Element of REAL
N is open V71() V72() V73() Neighbourhood of x0
N \ {x0} is V71() V72() V73() Element of K19(REAL)
f `| N is V1() V4( REAL ) V5( REAL ) V6() V35() V36() V37() Element of K19(K20(REAL,REAL))
g `| N is V1() V4( REAL ) V5( REAL ) V6() V35() V36() V37() Element of K19(K20(REAL,REAL))
(f `| N) / (g `| N) is V1() V4( REAL ) V5( REAL ) V6() V35() V36() V37() Element of K19(K20(REAL,REAL))
dom ((f `| N) / (g `| N)) is V71() V72() V73() Element of K19(REAL)
r is V30() real ext-real set
x0 - r is V30() real ext-real Element of REAL
x0 + r is V30() real ext-real Element of REAL
].(x0 - r),(x0 + r).[ is open V71() V72() V73() V99() V100() V104() Element of K19(REAL)
x0 + 0 is V30() real ext-real Element of REAL
{ b₁ where b₁ is V30() real ext-real Element of REAL : ( not b₁ <= x0 - r & not x0 + r <= b₁ ) } is set
dom (f `| N) is V71() V72() V73() Element of K19(REAL)
dom (g `| N) is V71() V72() V73() Element of K19(REAL)
(g `| N) " {0} is V71() V72() V73() Element of K19(REAL)
(dom (g `| N)) \ ((g `| N) " {0}) is V71() V72() V73() Element of K19(REAL)
(dom (f `| N)) /\ ((dom (g `| N)) \ ((g `| N) " {0})) is V71() V72() V73() Element of K19(REAL)
g " {0} is V71() V72() V73() Element of K19(REAL)
(dom g) \ (g " {0}) is V71() V72() V73() Element of K19(REAL)
(dom f) /\ ((dom g) \ (g " {0})) is V71() V72() V73() Element of K19(REAL)
d is V30() real ext-real Element of REAL
].d,x0.[ is open V71() V72() V73() V99() V100() V104() Element of K19(REAL)
(f / g) . d is V30() real ext-real Element of REAL
f . d is V30() real ext-real Element of REAL
(f . d) (#) g is V1() V4( REAL ) V5( REAL ) V6() V35() V36() V37() Element of K19(K20(REAL,REAL))
g . d is V30() real ext-real Element of REAL
(g . d) (#) f is V1() V4( REAL ) V5( REAL ) V6() V35() V36() V37() Element of K19(K20(REAL,REAL))
((f . d) (#) g) - ((g . d) (#) f) is V1() V4( REAL ) V5( REAL ) V6() V35() V36() V37() Element of K19(K20(REAL,REAL))
dom ((f . d) (#) g) is V71() V72() V73() Element of K19(REAL)
dom ((g . d) (#) f) is V71() V72() V73() Element of K19(REAL)
dom (((f . d) (#) g) - ((g . d) (#) f)) is V71() V72() V73() Element of K19(REAL)
(dom f) /\ (dom g) is V71() V72() V73() Element of K19(REAL)
[.d,x0.] is closed V71() V72() V73() V104() Element of K19(REAL)
g | N is V1() V4( REAL ) V5( REAL ) V6() V35() V36() V37() Element of K19(K20(REAL,REAL))
g | [.d,x0.] is V1() V4( REAL ) V5( REAL ) V6() V35() V36() V37() Element of K19(K20(REAL,REAL))
((f . d) (#) g) | [.d,x0.] is V1() V4( REAL ) V5( REAL ) V6() V35() V36() V37() Element of K19(K20(REAL,REAL))
f | N is V1() V4( REAL ) V5( REAL ) V6() V35() V36() V37() Element of K19(K20(REAL,REAL))
f | [.d,x0.] is V1() V4( REAL ) V5( REAL ) V6() V35() V36() V37() Element of K19(K20(REAL,REAL))
((g . d) (#) f) | [.d,x0.] is V1() V4( REAL ) V5( REAL ) V6() V35() V36() V37() Element of K19(K20(REAL,REAL))
(((f . d) (#) g) - ((g . d) (#) f)) | [.d,x0.] is V1() V4( REAL ) V5( REAL ) V6() V35() V36() V37() Element of K19(K20(REAL,REAL))
(dom ((f . d) (#) g)) /\ (dom ((g . d) (#) f)) is V71() V72() V73() Element of K19(REAL)
(((f . d) (#) g) - ((g . d) (#) f)) . d is V30() real ext-real Element of REAL
((f . d) (#) g) . d is V30() real ext-real Element of REAL
((g . d) (#) f) . d is V30() real ext-real Element of REAL
(((f . d) (#) g) . d) - (((g . d) (#) f) . d) is V30() real ext-real Element of REAL
(f . d) * (g . d) is V30() real ext-real Element of REAL
((f . d) * (g . d)) - (((g . d) (#) f) . d) is V30() real ext-real Element of REAL
(g . d) * (f . d) is V30() real ext-real Element of REAL
((g . d) * (f . d)) - ((g . d) * (f . d)) is V30() real ext-real Element of REAL
[.d,x0.] \ {x0} is V71() V72() V73() Element of K19(REAL)
(((f . d) (#) g) - ((g . d) (#) f)) . x0 is V30() real ext-real Element of REAL
((f . d) (#) g) . x0 is V30() real ext-real Element of REAL
((g . d) (#) f) . x0 is V30() real ext-real Element of REAL
(((f . d) (#) g) . x0) - (((g . d) (#) f) . x0) is V30() real ext-real Element of REAL
(f . d) * (g . x0) is V30() real ext-real Element of REAL
((f . d) * (g . x0)) - (((g . d) (#) f) . x0) is V30() real ext-real Element of REAL
(g . d) * 0 is V30() real ext-real Element of REAL
0 - ((g . d) * 0) is V30() real ext-real Element of REAL
k is V30() real ext-real Element of REAL
diff ((((f . d) (#) g) - ((g . d) (#) f)),k) is V30() real ext-real Element of REAL
diff (((f . d) (#) g),k) is V30() real ext-real Element of REAL
diff (((g . d) (#) f),k) is V30() real ext-real Element of REAL
(diff (((f . d) (#) g),k)) - (diff (((g . d) (#) f),k)) is V30() real ext-real Element of REAL
diff (f,k) is V30() real ext-real Element of REAL
(g . d) * (diff (f,k)) is V30() real ext-real Element of REAL
(diff (((f . d) (#) g),k)) - ((g . d) * (diff (f,k))) is V30() real ext-real Element of REAL
((f `| N) / (g `| N)) . k is V30() real ext-real Element of REAL
diff (g,k) is V30() real ext-real Element of REAL
(g `| N) . k is V30() real ext-real Element of REAL
(f . d) * (diff (g,k)) is V30() real ext-real Element of REAL
((f . d) * (diff (g,k))) - ((g . d) * (diff (f,k))) is V30() real ext-real Element of REAL
(f . d) / (g . d) is V30() real ext-real Element of REAL
(diff (f,k)) / (diff (g,k)) is V30() real ext-real Element of REAL
(g . d) " is V30() real ext-real Element of REAL
(f . d) * ((g . d) ") is V30() real ext-real Element of REAL
(diff (g,k)) " is V30() real ext-real Element of REAL
(diff (f,k)) * ((diff (g,k)) ") is V30() real ext-real Element of REAL
(f `| N) . k is V30() real ext-real Element of REAL
((f `| N) . k) * ((diff (g,k)) ") is V30() real ext-real Element of REAL
((g `| N) . k) " is V30() real ext-real Element of REAL
((f `| N) . k) * (((g `| N) . k) ") is V30() real ext-real Element of REAL
left_open_halfline x0 is V71() V72() V73() Element of K19(REAL)
K195(-infty,x0) is set
(dom (f / g)) /\ (left_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
NAT --> x0 is V1() V4( NAT ) V5( REAL ) V6() constant non empty total quasi_total V35() V36() V37() convergent Element of K19(K20(NAT,REAL))
a is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total V35() V36() V37() Element of K19(K20(NAT,REAL))
lim a is V30() real ext-real Element of REAL
rng a is V71() V72() V73() Element of K19(REAL)
(f / g) /* a is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total V35() V36() V37() Element of K19(K20(NAT,REAL))
lim ((f / g) /* a) is V30() real ext-real Element of REAL
k is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V71() V72() V73() V74() V75() V76() V93() V94() V101() Element of NAT
a ^\ k is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total V35() V36() V37() M7( REAL ,a)
((f / g) /* a) ^\ k is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total V35() V36() V37() M7( REAL ,(f / g) /* a)
b is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V71() V72() V73() V74() V75() V76() V93() V94() V101() Element of NAT
b + k is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V71() V72() V73() V74() V75() V76() V93() V94() V101() Element of NAT
a . (b + k) is V30() real ext-real Element of REAL
{ b₁ where b₁ is V30() real ext-real Element of REAL : not x0 <= b₁ } is set
(a ^\ k) . b is V30() real ext-real Element of REAL
m is V30() real ext-real Element of REAL
b is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V71() V72() V73() V74() V75() V76() V93() V94() V101() Element of NAT
(a ^\ k) . b is V30() real ext-real Element of REAL
].((a ^\ k) . b),x0.[ is open V71() V72() V73() V99() V100() V104() Element of K19(REAL)
(((f / g) /* a) ^\ k) . b is V30() real ext-real Element of REAL
rng (a ^\ k) is V71() V72() V73() Element of K19(REAL)
(f / g) . ((a ^\ k) . b) is V30() real ext-real Element of REAL
m is V30() real ext-real Element of REAL
((f `| N) / (g `| N)) . m is V30() real ext-real Element of REAL
(f / g) /* (a ^\ k) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total V35() V36() V37() Element of K19(K20(NAT,REAL))
((f / g) /* (a ^\ k)) . b is V30() real ext-real Element of REAL
b is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total V35() V36() V37() Element of K19(K20(NAT,REAL))
{ b₁ where b₁ is V30() real ext-real Element of REAL : ( not b₁ <= x0 - r & not x0 + r <= b₁ ) } is set
rng b is V71() V72() V73() Element of K19(REAL)
(dom ((f `| N) / (g `| N))) /\ (left_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
m is set
n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V71() V72() V73() V74() V75() V76() V93() V94() V101() Element of NAT
b . n is V30() real ext-real Element of REAL
(a ^\ k) . n is V30() real ext-real Element of REAL
].((a ^\ k) . n),x0.[ is open V71() V72() V73() V99() V100() V104() Element of K19(REAL)
[.((a ^\ k) . n),x0.] is closed V71() V72() V73() V104() Element of K19(REAL)
{ b₁ where b₁ is V30() real ext-real Element of REAL : ( not b₁ <= (a ^\ k) . n & not x0 <= b₁ ) } is set
c₁₃ is V30() real ext-real Element of REAL
m is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V71() V72() V73() V74() V75() V76() V93() V94() V101() Element of NAT
b . m is V30() real ext-real Element of REAL
(a ^\ k) . m is V30() real ext-real Element of REAL
].((a ^\ k) . m),x0.[ is open V71() V72() V73() V99() V100() V104() Element of K19(REAL)
{ b₁ where b₁ is V30() real ext-real Element of REAL : ( not b₁ <= (a ^\ k) . m & not x0 <= b₁ ) } is set
d is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total V35() V36() V37() Element of K19(K20(NAT,REAL))
d . m is V30() real ext-real Element of REAL
n is V30() real ext-real Element of REAL
lim d is V30() real ext-real Element of REAL
d . 0 is V30() real ext-real Element of REAL
lim (a ^\ k) is V30() real ext-real Element of REAL
lim b is V30() real ext-real Element of REAL
((f `| N) / (g `| N)) /* b is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total V35() V36() V37() Element of K19(K20(NAT,REAL))
m is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() real ext-real V71() V72() V73() V74() V75() V76() V77() V93() V94() V101() V104() Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V71() V72() V73() V74() V75() V76() V93() V94() V101() Element of NAT
(((f / g) /* a) ^\ k) . n is V30() real ext-real Element of REAL
b . n is V30() real ext-real Element of REAL
((f `| N) / (g `| N)) . (b . n) is V30() real ext-real Element of REAL
(((f `| N) / (g `| N)) /* b) . n is V30() real ext-real Element of REAL
lim (((f `| N) / (g `| N)) /* b) is V30() real ext-real Element of REAL
((f `| N) / (g `| N)) . x0 is V30() real ext-real Element of REAL
(f `| N) . x0 is V30() real ext-real Element of REAL
(g `| N) . x0 is V30() real ext-real Element of REAL
((g `| N) . x0) " is V30() real ext-real Element of REAL
((f `| N) . x0) * (((g `| N) . x0) ") is V30() real ext-real Element of REAL
(diff (f,x0)) * (((g `| N) . x0) ") is V30() real ext-real Element of REAL
(diff (g,x0)) " is V30() real ext-real Element of REAL
(diff (f,x0)) * ((diff (g,x0)) ") is V30() real ext-real Element of REAL
lim (((f / g) /* a) ^\ k) is V30() real ext-real Element of REAL
m is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() real ext-real V71() V72() V73() V74() V75() V76() V77() V93() V94() V101() V104() Element of NAT
m is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() real ext-real V71() V72() V73() V74() V75() V76() V77() V93() V94() V101() V104() Element of NAT
d is V30() real ext-real Element of REAL
a is V30() real ext-real Element of REAL
d is V30() real ext-real Element of REAL
lim_left ((f / g),x0) is V30() real ext-real Element of REAL
x0 + 0 is V30() real ext-real Element of REAL
{ b₁ where b₁ is V30() real ext-real Element of REAL : ( not b₁ <= x0 - r & not x0 + r <= b₁ ) } is set
dom (f `| N) is V71() V72() V73() Element of K19(REAL)
dom (g `| N) is V71() V72() V73() Element of K19(REAL)
(g `| N) " {0} is V71() V72() V73() Element of K19(REAL)
(dom (g `| N)) \ ((g `| N) " {0}) is V71() V72() V73() Element of K19(REAL)
(dom (f `| N)) /\ ((dom (g `| N)) \ ((g `| N) " {0})) is V71() V72() V73() Element of K19(REAL)
g " {0} is V71() V72() V73() Element of K19(REAL)
(dom g) \ (g " {0}) is V71() V72() V73() Element of K19(REAL)
(dom f) /\ ((dom g) \ (g " {0})) is V71() V72() V73() Element of K19(REAL)
d is V30() real ext-real Element of REAL
].x0,d.[ is open V71() V72() V73() V99() V100() V104() Element of K19(REAL)
(f / g) . d is V30() real ext-real Element of REAL
f . d is V30() real ext-real Element of REAL
(f . d) (#) g is V1() V4( REAL ) V5( REAL ) V6() V35() V36() V37() Element of K19(K20(REAL,REAL))
g . d is V30() real ext-real Element of REAL
(g . d) (#) f is V1() V4( REAL ) V5( REAL ) V6() V35() V36() V37() Element of K19(K20(REAL,REAL))
((f . d) (#) g) - ((g . d) (#) f) is V1() V4( REAL ) V5( REAL ) V6() V35() V36() V37() Element of K19(K20(REAL,REAL))
dom ((f . d) (#) g) is V71() V72() V73() Element of K19(REAL)
dom ((g . d) (#) f) is V71() V72() V73() Element of K19(REAL)
dom (((f . d) (#) g) - ((g . d) (#) f)) is V71() V72() V73() Element of K19(REAL)
(dom f) /\ (dom g) is V71() V72() V73() Element of K19(REAL)
[.x0,d.] is closed V71() V72() V73() V104() Element of K19(REAL)
g | N is V1() V4( REAL ) V5( REAL ) V6() V35() V36() V37() Element of K19(K20(REAL,REAL))
g | [.x0,d.] is V1() V4( REAL ) V5( REAL ) V6() V35() V36() V37() Element of K19(K20(REAL,REAL))
((f . d) (#) g) | [.x0,d.] is V1() V4( REAL ) V5( REAL ) V6() V35() V36() V37() Element of K19(K20(REAL,REAL))
f | N is V1() V4( REAL ) V5( REAL ) V6() V35() V36() V37() Element of K19(K20(REAL,REAL))
f | [.x0,d.] is V1() V4( REAL ) V5( REAL ) V6() V35() V36() V37() Element of K19(K20(REAL,REAL))
((g . d) (#) f) | [.x0,d.] is V1() V4( REAL ) V5( REAL ) V6() V35() V36() V37() Element of K19(K20(REAL,REAL))
(((f . d) (#) g) - ((g . d) (#) f)) | [.x0,d.] is V1() V4( REAL ) V5( REAL ) V6() V35() V36() V37() Element of K19(K20(REAL,REAL))
(dom ((f . d) (#) g)) /\ (dom ((g . d) (#) f)) is V71() V72() V73() Element of K19(REAL)
(((f . d) (#) g) - ((g . d) (#) f)) . d is V30() real ext-real Element of REAL
((f . d) (#) g) . d is V30() real ext-real Element of REAL
((g . d) (#) f) . d is V30() real ext-real Element of REAL
(((f . d) (#) g) . d) - (((g . d) (#) f) . d) is V30() real ext-real Element of REAL
(f . d) * (g . d) is V30() real ext-real Element of REAL
((f . d) * (g . d)) - (((g . d) (#) f) . d) is V30() real ext-real Element of REAL
(g . d) * (f . d) is V30() real ext-real Element of REAL
((g . d) * (f . d)) - ((g . d) * (f . d)) is V30() real ext-real Element of REAL
[.x0,d.] \ {x0} is V71() V72() V73() Element of K19(REAL)
(((f . d) (#) g) - ((g . d) (#) f)) . x0 is V30() real ext-real Element of REAL
((f . d) (#) g) . x0 is V30() real ext-real Element of REAL
((g . d) (#) f) . x0 is V30() real ext-real Element of REAL
(((f . d) (#) g) . x0) - (((g . d) (#) f) . x0) is V30() real ext-real Element of REAL
(f . d) * (g . x0) is V30() real ext-real Element of REAL
((f . d) * (g . x0)) - (((g . d) (#) f) . x0) is V30() real ext-real Element of REAL
(g . d) * 0 is V30() real ext-real Element of REAL
0 - ((g . d) * 0) is V30() real ext-real Element of REAL
k is V30() real ext-real Element of REAL
diff ((((f . d) (#) g) - ((g . d) (#) f)),k) is V30() real ext-real Element of REAL
diff (((f . d) (#) g),k) is V30() real ext-real Element of REAL
diff (((g . d) (#) f),k) is V30() real ext-real Element of REAL
(diff (((f . d) (#) g),k)) - (diff (((g . d) (#) f),k)) is V30() real ext-real Element of REAL
diff (f,k) is V30() real ext-real Element of REAL
(g . d) * (diff (f,k)) is V30() real ext-real Element of REAL
(diff (((f . d) (#) g),k)) - ((g . d) * (diff (f,k))) is V30() real ext-real Element of REAL
((f `| N) / (g `| N)) . k is V30() real ext-real Element of REAL
diff (g,k) is V30() real ext-real Element of REAL
(g `| N) . k is V30() real ext-real Element of REAL
(f . d) * (diff (g,k)) is V30() real ext-real Element of REAL
((f . d) * (diff (g,k))) - ((g . d) * (diff (f,k))) is V30() real ext-real Element of REAL
(f . d) / (g . d) is V30() real ext-real Element of REAL
(diff (f,k)) / (diff (g,k)) is V30() real ext-real Element of REAL
(g . d) " is V30() real ext-real Element of REAL
(f . d) * ((g . d) ") is V30() real ext-real Element of REAL
(diff (g,k)) " is V30() real ext-real Element of REAL
(diff (f,k)) * ((diff (g,k)) ") is V30() real ext-real Element of REAL
(f `| N) . k is V30() real ext-real Element of REAL
((f `| N) . k) * ((diff (g,k)) ") is V30() real ext-real Element of REAL
((g `| N) . k) " is V30() real ext-real Element of REAL
((f `| N) . k) * (((g `| N) . k) ") is V30() real ext-real Element of REAL
right_open_halfline x0 is V71() V72() V73() Element of K19(REAL)
K195(x0,+infty) is set
(dom (f / g)) /\ (right_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
NAT --> x0 is V1() V4( NAT ) V5( REAL ) V6() constant non empty total quasi_total V35() V36() V37() convergent Element of K19(K20(NAT,REAL))
a is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total V35() V36() V37() Element of K19(K20(NAT,REAL))
lim a is V30() real ext-real Element of REAL
rng a is V71() V72() V73() Element of K19(REAL)
(f / g) /* a is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total V35() V36() V37() Element of K19(K20(NAT,REAL))
lim ((f / g) /* a) is V30() real ext-real Element of REAL
k is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V71() V72() V73() V74() V75() V76() V93() V94() V101() Element of NAT
a ^\ k is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total V35() V36() V37() M7( REAL ,a)
((f / g) /* a) ^\ k is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total V35() V36() V37() M7( REAL ,(f / g) /* a)
b is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V71() V72() V73() V74() V75() V76() V93() V94() V101() Element of NAT
b + k is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V71() V72() V73() V74() V75() V76() V93() V94() V101() Element of NAT
a . (b + k) is V30() real ext-real Element of REAL
{ b₁ where b₁ is V30() real ext-real Element of REAL : not b₁ <= x0 } is set
(a ^\ k) . b is V30() real ext-real Element of REAL
m is V30() real ext-real Element of REAL
b is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V71() V72() V73() V74() V75() V76() V93() V94() V101() Element of NAT
(a ^\ k) . b is V30() real ext-real Element of REAL
].x0,((a ^\ k) . b).[ is open V71() V72() V73() V99() V100() V104() Element of K19(REAL)
(((f / g) /* a) ^\ k) . b is V30() real ext-real Element of REAL
rng (a ^\ k) is V71() V72() V73() Element of K19(REAL)
(f / g) . ((a ^\ k) . b) is V30() real ext-real Element of REAL
m is V30() real ext-real Element of REAL
((f `| N) / (g `| N)) . m is V30() real ext-real Element of REAL
(f / g) /* (a ^\ k) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total V35() V36() V37() Element of K19(K20(NAT,REAL))
((f / g) /* (a ^\ k)) . b is V30() real ext-real Element of REAL
b is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total V35() V36() V37() Element of K19(K20(NAT,REAL))
{ b₁ where b₁ is V30() real ext-real Element of REAL : ( not b₁ <= x0 - r & not x0 + r <= b₁ ) } is set
rng b is V71() V72() V73() Element of K19(REAL)
(dom ((f `| N) / (g `| N))) /\ (right_open_halfline x0) is V71() V72() V73() Element of K19(REAL)
m is set
n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V71() V72() V73() V74() V75() V76() V93() V94() V101() Element of NAT
b . n is V30() real ext-real Element of REAL
(a ^\ k) . n is V30() real ext-real Element of REAL
].x0,((a ^\ k) . n).[ is open V71() V72() V73() V99() V100() V104() Element of K19(REAL)
[.x0,((a ^\ k) . n).] is closed V71() V72() V73() V104() Element of K19(REAL)
{ b₁ where b₁ is V30() real ext-real Element of REAL : ( not b₁ <= x0 & not (a ^\ k) . n <= b₁ ) } is set
c₁₃ is V30() real ext-real Element of REAL
m is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V71() V72() V73() V74() V75() V76() V93() V94() V101() Element of NAT
b . m is V30() real ext-real Element of REAL
(a ^\ k) . m is V30() real ext-real Element of REAL
].x0,((a ^\ k) . m).[ is open V71() V72() V73() V99() V100() V104() Element of K19(REAL)
{ b₁ where b₁ is V30() real ext-real Element of REAL : ( not b₁ <= x0 & not (a ^\ k) . m <= b₁ ) } is set
d is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total V35() V36() V37() Element of K19(K20(NAT,REAL))
d . m is V30() real ext-real Element of REAL
n is V30() real ext-real Element of REAL
lim d is V30() real ext-real Element of REAL
d . 0 is V30() real ext-real Element of REAL
lim (a ^\ k) is V30() real ext-real Element of REAL
lim b is V30() real ext-real Element of REAL
((f `| N) / (g `| N)) /* b is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total V35() V36() V37() Element of K19(K20(NAT,REAL))
m is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() real ext-real V71() V72() V73() V74() V75() V76() V77() V93() V94() V101() V104() Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V71() V72() V73() V74() V75() V76() V93() V94() V101() Element of NAT
(((f / g) /* a) ^\ k) . n is V30() real ext-real Element of REAL
b . n is V30() real ext-real Element of REAL
((f `| N) / (g `| N)) . (b . n) is V30() real ext-real Element of REAL
(((f `| N) / (g `| N)) /* b) . n is V30() real ext-real Element of REAL
lim (((f `| N) / (g `| N)) /* b) is V30() real ext-real Element of REAL
((f `| N) / (g `| N)) . x0 is V30() real ext-real Element of REAL
(f `| N) . x0 is V30() real ext-real Element of REAL
(g `| N) . x0 is V30() real ext-real Element of REAL
((g `| N) . x0) " is V30() real ext-real Element of REAL
((f `| N) . x0) * (((g `| N) . x0) ") is V30() real ext-real Element of REAL
(diff (f,x0)) * (((g `| N) . x0) ") is V30() real ext-real Element of REAL
(diff (g,x0)) " is V30() real ext-real Element of REAL
(diff (f,x0)) * ((diff (g,x0)) ") is V30() real ext-real Element of REAL
lim (((f / g) /* a) ^\ k) is V30() real ext-real Element of REAL
m is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() real ext-real V71() V72() V73() V74() V75() V76() V77() V93() V94() V101() V104() Element of NAT
m is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() real ext-real V71() V72() V73() V74() V75() V76() V77() V93() V94() V101() V104() Element of NAT
d is V30() real ext-real Element of REAL
lim_right ((f / g),x0) is V30() real ext-real Element of REAL