:: FCONT_3 semantic presentation

REAL is non empty V48() V84() V85() V86() V90() V97() V98() V100() set

NAT is non empty epsilon-transitive epsilon-connected ordinal V84() V85() V86() V87() V88() V89() V90() V95() V97() Element of K19(REAL)

K19(REAL) is set

COMPLEX is non empty V48() V84() V90() set

omega is non empty epsilon-transitive epsilon-connected ordinal V84() V85() V86() V87() V88() V89() V90() V95() V97() set

K19(omega) is set

K20(NAT,REAL) is V1() V33() V34() V35() set

K19(K20(NAT,REAL)) is set

K19(K19(REAL)) is set

K20(REAL,REAL) is V1() V33() V34() V35() set

K19(K20(REAL,REAL)) is set

RAT is non empty V48() V84() V85() V86() V87() V90() set

INT is non empty V48() V84() V85() V86() V87() V88() V90() set

K20(COMPLEX,COMPLEX) is V1() V33() set

K19(K20(COMPLEX,COMPLEX)) is set

K20(K20(COMPLEX,COMPLEX),COMPLEX) is V1() V33() set

K19(K20(K20(COMPLEX,COMPLEX),COMPLEX)) is set

K20(K20(REAL,REAL),REAL) is V1() V33() V34() V35() set

K19(K20(K20(REAL,REAL),REAL)) is set

K20(RAT,RAT) is V1() V5( RAT ) V33() V34() V35() set

K19(K20(RAT,RAT)) is set

K20(K20(RAT,RAT),RAT) is V1() V5( RAT ) V33() V34() V35() set

K19(K20(K20(RAT,RAT),RAT)) is set

K20(INT,INT) is V1() V5( RAT ) V5( INT ) V33() V34() V35() set

K19(K20(INT,INT)) is set

K20(K20(INT,INT),INT) is V1() V5( RAT ) V5( INT ) V33() V34() V35() set

K19(K20(K20(INT,INT),INT)) is set

K20(NAT,NAT) is V1() V5( RAT ) V5( INT ) V33() V34() V35() V36() set

K20(K20(NAT,NAT),NAT) is V1() V5( RAT ) V5( INT ) V33() V34() V35() V36() set

K19(K20(K20(NAT,NAT),NAT)) is set

K19(NAT) is set

1 is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V82() V83() V84() V85() V86() V87() V88() V89() V95() V97() Element of NAT

{} is set

the V1() non-empty empty-yielding V5( RAT ) empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() real ext-real non positive non negative V33() V34() V35() V36() V84() V85() V86() V87() V88() V89() V90() V97() V100() set is V1() non-empty empty-yielding V5( RAT ) empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() real ext-real non positive non negative V33() V34() V35() V36() V84() V85() V86() V87() V88() V89() V90() V97() V100() set

0 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V82() V83() V84() V85() V86() V87() V88() V89() V97() Element of NAT

2 is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V82() V83() V84() V85() V86() V87() V88() V89() V95() V97() Element of NAT

-infty is non empty non real ext-real non positive negative set

+infty is non empty non real ext-real positive non negative set

K195(-infty,+infty) is V95() V96() V100() set

{ b

[#] REAL is V84() V85() V86() Element of K19(REAL)

f is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))

rng f is non empty V84() V85() V86() set

lim f is V22() real ext-real Element of REAL

f is V84() V85() V86() Element of K19(REAL)

L is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))

rng L is non empty V84() V85() V86() set

lim L is V22() real ext-real Element of REAL

rng L is non empty V84() V85() V86() Element of K19(REAL)

([#] REAL) ` is V84() V85() V86() Element of K19(REAL)

REAL \ ([#] REAL) is V84() V85() V86() set

{} REAL is V84() V85() V86() Element of K19(REAL)

f is V84() V85() V86() Element of K19(REAL)

f ` is V84() V85() V86() Element of K19(REAL)

REAL \ f is V84() V85() V86() set

f is V22() real ext-real set

right_closed_halfline f is V84() V85() V86() Element of K19(REAL)

K193(f,+infty) is V96() V100() set

{ b

NAT --> f is V1() V4( NAT ) V5({f}) Function-like constant non empty total quasi_total V33() V34() V35() Element of K19(K20(NAT,{f}))

{f} is V84() V85() V86() set

K20(NAT,{f}) is V1() V33() V34() V35() set

K19(K20(NAT,{f})) is set

r1 is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))

rng r1 is non empty V84() V85() V86() set

lim r1 is V22() real ext-real Element of REAL

rng r1 is non empty V84() V85() V86() Element of K19(REAL)

x0 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V82() V83() V84() V85() V86() V87() V88() V89() V97() Element of NAT

r1 . x0 is V22() real ext-real Element of REAL

{ b

L is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))

L . x0 is V22() real ext-real Element of REAL

N is V22() real ext-real Element of REAL

lim L is V22() real ext-real Element of REAL

L . 0 is V22() real ext-real Element of REAL

left_closed_halfline f is V84() V85() V86() Element of K19(REAL)

K194(-infty,f) is V95() V100() set

{ b

NAT --> f is V1() V4( NAT ) V5({f}) Function-like constant non empty total quasi_total V33() V34() V35() Element of K19(K20(NAT,{f}))

{f} is V84() V85() V86() set

K20(NAT,{f}) is V1() V33() V34() V35() set

K19(K20(NAT,{f})) is set

r1 is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))

rng r1 is non empty V84() V85() V86() set

lim r1 is V22() real ext-real Element of REAL

rng r1 is non empty V84() V85() V86() Element of K19(REAL)

x0 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V82() V83() V84() V85() V86() V87() V88() V89() V97() Element of NAT

r1 . x0 is V22() real ext-real Element of REAL

{ b

L is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))

L . x0 is V22() real ext-real Element of REAL

N is V22() real ext-real Element of REAL

lim L is V22() real ext-real Element of REAL

L . 0 is V22() real ext-real Element of REAL

right_open_halfline f is V84() V85() V86() Element of K19(REAL)

K195(f,+infty) is V95() V96() V100() set

{ b

(right_open_halfline f) ` is V84() V85() V86() Element of K19(REAL)

REAL \ (right_open_halfline f) is V84() V85() V86() set

halfline f is V84() V85() V86() Element of K19(REAL)

K195(-infty,f) is V95() V96() V100() set

{ b

(halfline f) ` is V84() V85() V86() Element of K19(REAL)

REAL \ (halfline f) is V84() V85() V86() set

f is V22() real ext-real Element of REAL

L is V22() real ext-real Element of REAL

f - L is V22() real ext-real Element of REAL

abs (f - L) is V22() real ext-real Element of REAL

r1 is V22() real ext-real set

L - r1 is V22() real ext-real Element of REAL

L + r1 is V22() real ext-real Element of REAL

].(L - r1),(L + r1).[ is open V84() V85() V86() V95() V96() V100() Element of K19(REAL)

{ b

(L + r1) - L is V22() real ext-real Element of REAL

x0 is V22() real ext-real Element of REAL

L - f is V22() real ext-real Element of REAL

- (f - L) is V22() real ext-real Element of REAL

abs (- (f - L)) is V22() real ext-real Element of REAL

L - (L - r1) is V22() real ext-real Element of REAL

x0 is V22() real ext-real Element of REAL

f is V22() real ext-real Element of REAL

L is V22() real ext-real Element of REAL

f - L is V22() real ext-real Element of REAL

r1 is V22() real ext-real set

L - r1 is V22() real ext-real Element of REAL

L + r1 is V22() real ext-real Element of REAL

].(L - r1),(L + r1).[ is open V84() V85() V86() V95() V96() V100() Element of K19(REAL)

{ b

- r1 is V22() real ext-real set

].(- r1),r1.[ is open V84() V85() V86() V95() V96() V100() Element of K19(REAL)

{ b

abs (f - L) is V22() real ext-real Element of REAL

(f - L) - 0 is V22() real ext-real Element of REAL

abs ((f - L) - 0) is V22() real ext-real Element of REAL

0 - r1 is V22() real ext-real Element of REAL

0 + r1 is V22() real ext-real Element of REAL

].(0 - r1),(0 + r1).[ is open V84() V85() V86() V95() V96() V100() Element of K19(REAL)

{ b

f is V22() real ext-real Element of REAL

L is V22() real ext-real Element of REAL

r1 is V22() real ext-real Element of REAL

L + r1 is V22() real ext-real Element of REAL

abs r1 is V22() real ext-real Element of REAL

x0 is V22() real ext-real set

L - x0 is V22() real ext-real Element of REAL

L + x0 is V22() real ext-real Element of REAL

].(L - x0),(L + x0).[ is open V84() V85() V86() V95() V96() V100() Element of K19(REAL)

{ b

f - L is V22() real ext-real Element of REAL

abs (f - L) is V22() real ext-real Element of REAL

f is V22() real ext-real Element of REAL

L is V22() real ext-real Element of REAL

f - L is V22() real ext-real Element of REAL

r1 is V22() real ext-real set

- r1 is V22() real ext-real set

].(- r1),r1.[ is open V84() V85() V86() V95() V96() V100() Element of K19(REAL)

{ b

L - r1 is V22() real ext-real Element of REAL

L + r1 is V22() real ext-real Element of REAL

].(L - r1),(L + r1).[ is open V84() V85() V86() V95() V96() V100() Element of K19(REAL)

{ b

abs (f - L) is V22() real ext-real Element of REAL

N is V22() real ext-real Element of REAL

L + (f - L) is V22() real ext-real Element of REAL

f is V22() real ext-real Element of REAL

L is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))

lim L is V22() real ext-real Element of REAL

r1 is V22() real ext-real set

x0 is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))

NAT --> r1 is V1() V4( NAT ) V5({r1}) Function-like constant non empty total quasi_total V33() V34() V35() Element of K19(K20(NAT,{r1}))

{r1} is V84() V85() V86() set

K20(NAT,{r1}) is V1() V33() V34() V35() set

K19(K20(NAT,{r1})) is set

N is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))

N - x0 is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))

r is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V82() V83() V84() V85() V86() V87() V88() V89() V97() Element of NAT

(N - x0) . r is V22() real ext-real Element of REAL

N . r is V22() real ext-real Element of REAL

x0 . r is V22() real ext-real Element of REAL

(N . r) - (x0 . r) is V22() real ext-real Element of REAL

r1 - (x0 . r) is V22() real ext-real Element of REAL

r + 1 is V22() real ext-real Element of REAL

f / (r + 1) is V22() real ext-real Element of REAL

r1 - (f / (r + 1)) is V22() real ext-real Element of REAL

L . r is V22() real ext-real Element of REAL

lim N is V22() real ext-real Element of REAL

N . 0 is V22() real ext-real Element of REAL

lim x0 is V22() real ext-real Element of REAL

r1 - 0 is V22() real ext-real Element of REAL

f is V22() real ext-real Element of REAL

L is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))

lim L is V22() real ext-real Element of REAL

r1 is V22() real ext-real set

x0 is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))

NAT --> r1 is V1() V4( NAT ) V5({r1}) Function-like constant non empty total quasi_total V33() V34() V35() Element of K19(K20(NAT,{r1}))

{r1} is V84() V85() V86() set

K20(NAT,{r1}) is V1() V33() V34() V35() set

K19(K20(NAT,{r1})) is set

N is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))

N + x0 is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))

r is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V82() V83() V84() V85() V86() V87() V88() V89() V97() Element of NAT

(N + x0) . r is V22() real ext-real Element of REAL

N . r is V22() real ext-real Element of REAL

x0 . r is V22() real ext-real Element of REAL

(N . r) + (x0 . r) is V22() real ext-real Element of REAL

r1 + (x0 . r) is V22() real ext-real Element of REAL

r + 1 is V22() real ext-real Element of REAL

f / (r + 1) is V22() real ext-real Element of REAL

r1 + (f / (r + 1)) is V22() real ext-real Element of REAL

L . r is V22() real ext-real Element of REAL

lim N is V22() real ext-real Element of REAL

N . 0 is V22() real ext-real Element of REAL

lim x0 is V22() real ext-real Element of REAL

r1 + 0 is V22() real ext-real Element of REAL

f is V22() real ext-real Element of REAL

L is V22() real ext-real set

r1 is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))

r1 . f is V22() real ext-real Element of REAL

dom r1 is V84() V85() V86() Element of K19(REAL)

x0 is open V84() V85() V86() Neighbourhood of f

N is V22() real ext-real set

f - N is V22() real ext-real Element of REAL

f + N is V22() real ext-real Element of REAL

].(f - N),(f + N).[ is open V84() V85() V86() V95() V96() V100() Element of K19(REAL)

{ b

r is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V82() V83() V84() V85() V86() V87() V88() V89() V97() Element of NAT

r + 1 is V22() real ext-real Element of REAL

N / (r + 1) is V22() real ext-real Element of REAL

f - (N / (r + 1)) is V22() real ext-real Element of REAL

f + (N / (r + 1)) is V22() real ext-real Element of REAL

].(f - (N / (r + 1))),(f + (N / (r + 1))).[ is open V84() V85() V86() V95() V96() V100() Element of K19(REAL)

{ b

r is open V84() V85() V86() Neighbourhood of f

fp is set

fm is V22() real ext-real Element of REAL

0 + 1 is V22() real ext-real Element of REAL

N / 1 is V22() real ext-real Element of REAL

fp is V22() real ext-real Element of REAL

r1 . fp is V22() real ext-real Element of REAL

fm is V22() real ext-real Element of REAL

r is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))

rng r is non empty V84() V85() V86() Element of K19(REAL)

r is set

fp is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V82() V83() V84() V85() V86() V87() V88() V89() V97() Element of NAT

r . fp is V22() real ext-real Element of REAL

r is V22() real ext-real set

fp is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V82() V83() V84() V85() V86() V87() V88() V89() V97() Element of NAT

fm is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V82() V83() V84() V85() V86() V87() V88() V89() V97() Element of NAT

r1 /* r is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))

(r1 /* r) . fm is V22() real ext-real Element of REAL

((r1 /* r) . fm) - L is V22() real ext-real Element of REAL

abs (((r1 /* r) . fm) - L) is V22() real ext-real Element of REAL

r . fm is V22() real ext-real Element of REAL

r1 . (r . fm) is V22() real ext-real Element of REAL

(r1 . (r . fm)) - L is V22() real ext-real Element of REAL

abs ((r1 . (r . fm)) - L) is V22() real ext-real Element of REAL

L - L is V22() real ext-real set

abs (L - L) is V22() real ext-real Element of REAL

r is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))

fp is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))

fm is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V82() V83() V84() V85() V86() V87() V88() V89() V97() Element of NAT

r . fm is V22() real ext-real Element of REAL

fm + 1 is V22() real ext-real Element of REAL

N / (fm + 1) is V22() real ext-real Element of REAL

f - (N / (fm + 1)) is V22() real ext-real Element of REAL

f + (N / (fm + 1)) is V22() real ext-real Element of REAL

r . fm is V22() real ext-real Element of REAL

fp . fm is V22() real ext-real Element of REAL

lim fp is V22() real ext-real Element of REAL

lim r is V22() real ext-real Element of REAL

lim r is V22() real ext-real Element of REAL

lim (r1 /* r) is V22() real ext-real Element of REAL

f is set

L is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))

L | f is V1() V4( REAL ) V4(f) V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))

dom (L | f) is Element of K19(f)

K19(f) is set

r1 is V22() real ext-real Element of REAL

x0 is V22() real ext-real Element of REAL

(L | f) . r1 is V22() real ext-real Element of REAL

(L | f) . x0 is V22() real ext-real Element of REAL

dom L is V84() V85() V86() Element of K19(REAL)

f /\ (dom L) is V84() V85() V86() Element of K19(REAL)

L . x0 is V22() real ext-real Element of REAL

L . r1 is V22() real ext-real Element of REAL

L . r1 is V22() real ext-real Element of REAL

L . x0 is V22() real ext-real Element of REAL

dom (L | f) is Element of K19(f)

K19(f) is set

r1 is V22() real ext-real Element of REAL

x0 is V22() real ext-real Element of REAL

(L | f) . r1 is V22() real ext-real Element of REAL

(L | f) . x0 is V22() real ext-real Element of REAL

dom L is V84() V85() V86() Element of K19(REAL)

f /\ (dom L) is V84() V85() V86() Element of K19(REAL)

L . r1 is V22() real ext-real Element of REAL

L . x0 is V22() real ext-real Element of REAL

L . x0 is V22() real ext-real Element of REAL

L . r1 is V22() real ext-real Element of REAL

f is set

L is V1() V4( REAL ) V5( REAL ) Function-like one-to-one V33() V34() V35() Element of K19(K20(REAL,REAL))

L | f is V1() V4( REAL ) V4(f) V4( REAL ) V5( REAL ) Function-like one-to-one V33() V34() V35() Element of K19(K20(REAL,REAL))

(L | f) " is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))

L .: f is V84() V85() V86() Element of K19(REAL)

((L | f) ") | (L .: f) is V1() V4( REAL ) V4(L .: f) V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))

dom ((L | f) ") is V84() V85() V86() Element of K19(REAL)

(L .: f) /\ (dom ((L | f) ")) is V84() V85() V86() Element of K19(REAL)

r1 is V22() real ext-real Element of REAL

x0 is V22() real ext-real Element of REAL

((L | f) ") . x0 is V22() real ext-real Element of REAL

((L | f) ") . r1 is V22() real ext-real Element of REAL

rng (L | f) is V84() V85() V86() Element of K19(REAL)

(L | f) | f is V1() V4( REAL ) V4(f) V4( REAL ) V5( REAL ) Function-like one-to-one V33() V34() V35() Element of K19(K20(REAL,REAL))

(L | f) . (((L | f) ") . x0) is V22() real ext-real Element of REAL

dom (L | f) is Element of K19(f)

K19(f) is set

dom ((L | f) | f) is Element of K19(f)

f /\ (dom (L | f)) is Element of K19(f)

(L | f) . (((L | f) ") . r1) is V22() real ext-real Element of REAL

(L | f) . (((L | f) ") . x0) is V22() real ext-real Element of REAL

f is set

L is V1() V4( REAL ) V5( REAL ) Function-like one-to-one V33() V34() V35() Element of K19(K20(REAL,REAL))

L | f is V1() V4( REAL ) V4(f) V4( REAL ) V5( REAL ) Function-like one-to-one V33() V34() V35() Element of K19(K20(REAL,REAL))

(L | f) " is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))

L .: f is V84() V85() V86() Element of K19(REAL)

((L | f) ") | (L .: f) is V1() V4( REAL ) V4(L .: f) V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))

dom ((L | f) ") is V84() V85() V86() Element of K19(REAL)

(L .: f) /\ (dom ((L | f) ")) is V84() V85() V86() Element of K19(REAL)

r1 is V22() real ext-real Element of REAL

x0 is V22() real ext-real Element of REAL

((L | f) ") . r1 is V22() real ext-real Element of REAL

((L | f) ") . x0 is V22() real ext-real Element of REAL

rng (L | f) is V84() V85() V86() Element of K19(REAL)

(L | f) | f is V1() V4( REAL ) V4(f) V4( REAL ) V5( REAL ) Function-like one-to-one V33() V34() V35() Element of K19(K20(REAL,REAL))

(L | f) . (((L | f) ") . x0) is V22() real ext-real Element of REAL

dom (L | f) is Element of K19(f)

K19(f) is set

dom ((L | f) | f) is Element of K19(f)

f /\ (dom (L | f)) is Element of K19(f)

(L | f) . (((L | f) ") . r1) is V22() real ext-real Element of REAL

(L | f) . (((L | f) ") . x0) is V22() real ext-real Element of REAL

f is set

L is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))

dom L is V84() V85() V86() Element of K19(REAL)

L | f is V1() V4( REAL ) V4(f) V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))

L .: f is V84() V85() V86() Element of K19(REAL)

r1 is V22() real ext-real Element of REAL

halfline r1 is open V84() V85() V86() Element of K19(REAL)

K195(-infty,r1) is V95() V96() V100() set

{ b

(L | f) | f is V1() V4( REAL ) V4(f) V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))

dom (L | f) is Element of K19(f)

K19(f) is set

N is V22() real ext-real set

(L | f) .: f is V84() V85() V86() Element of K19(REAL)

(dom L) /\ f is V84() V85() V86() Element of K19(REAL)

(L | f) . N is V22() real ext-real Element of REAL

r is open V84() V85() V86() Neighbourhood of (L | f) . N

r is open V84() V85() V86() Neighbourhood of (L | f) . N

fp is open V84() V85() V86() Neighbourhood of (L | f) . N

fm is V22() real ext-real set

((L | f) . N) - fm is V22() real ext-real Element of REAL

((L | f) . N) + fm is V22() real ext-real Element of REAL

].(((L | f) . N) - fm),(((L | f) . N) + fm).[ is open V84() V85() V86() V95() V96() V100() Element of K19(REAL)

{ b

R is V22() real ext-real Element of REAL

R / 2 is V22() real ext-real Element of REAL

((L | f) . N) + (R / 2) is V22() real ext-real Element of REAL

(((L | f) . N) + (R / 2)) + (R / 2) is V22() real ext-real Element of REAL

((L | f) . N) + R is V22() real ext-real Element of REAL

(((L | f) . N) + R) - R is V22() real ext-real Element of REAL

((L | f) . N) - R is V22() real ext-real Element of REAL

].(((L | f) . N) - R),(((L | f) . N) + R).[ is open V84() V85() V86() V95() V96() V100() Element of K19(REAL)

{ b

N1 is V22() real ext-real Element of REAL

(L | f) . N1 is V22() real ext-real Element of REAL

f /\ (dom (L | f)) is Element of K19(f)

((L | f) . N) - (R / 2) is V22() real ext-real Element of REAL

(((L | f) . N) - R) + (R / 2) is V22() real ext-real Element of REAL

r2 is V22() real ext-real Element of REAL

(L | f) . r2 is V22() real ext-real Element of REAL

N1 - N is V22() real ext-real Element of REAL

N - r2 is V22() real ext-real Element of REAL

min ((N - r2),(N1 - N)) is V22() real ext-real set

N - (min ((N - r2),(N1 - N))) is V22() real ext-real set

N + (min ((N - r2),(N1 - N))) is V22() real ext-real set

].(N - (min ((N - r2),(N1 - N)))),(N + (min ((N - r2),(N1 - N)))).[ is open V84() V85() V86() V95() V96() V100() Element of K19(REAL)

{ b

r2 is open V84() V85() V86() Neighbourhood of N

N is V22() real ext-real set

s is open V84() V85() V86() Neighbourhood of N

(min ((N - r2),(N1 - N))) + N is V22() real ext-real set

x is V22() real ext-real Element of REAL

((min ((N - r2),(N1 - N))) + N) - N is V22() real ext-real set

N - N is V22() real ext-real set

- (N - N) is V22() real ext-real set

- (N - r2) is V22() real ext-real Element of REAL

N - N is V22() real ext-real set

(N - N) + N is V22() real ext-real set

r2 - N is V22() real ext-real Element of REAL

(r2 - N) + N is V22() real ext-real Element of REAL

(L | f) . N is V22() real ext-real Element of REAL

x is V22() real ext-real Element of REAL

(N1 - N) + N is V22() real ext-real Element of REAL

[.(((L | f) . N) - (R / 2)),(((L | f) . N) + (R / 2)).] is closed V84() V85() V86() V100() Element of K19(REAL)

{ b

(L | f) | f is V1() V4( REAL ) V4(f) V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))

dom (L | f) is Element of K19(f)

K19(f) is set

N is V22() real ext-real set

(L | f) .: f is V84() V85() V86() Element of K19(REAL)

(dom L) /\ f is V84() V85() V86() Element of K19(REAL)

(L | f) . N is V22() real ext-real Element of REAL

r is open V84() V85() V86() Neighbourhood of (L | f) . N

r is open V84() V85() V86() Neighbourhood of (L | f) . N

fp is open V84() V85() V86() Neighbourhood of (L | f) . N

fm is V22() real ext-real set

((L | f) . N) - fm is V22() real ext-real Element of REAL

((L | f) . N) + fm is V22() real ext-real Element of REAL

].(((L | f) . N) - fm),(((L | f) . N) + fm).[ is open V84() V85() V86() V95() V96() V100() Element of K19(REAL)

{ b

R is V22() real ext-real Element of REAL

R / 2 is V22() real ext-real Element of REAL

((L | f) . N) + (R / 2) is V22() real ext-real Element of REAL

(((L | f) . N) + (R / 2)) + (R / 2) is V22() real ext-real Element of REAL

((L | f) . N) + R is V22() real ext-real Element of REAL

(((L | f) . N) + R) - R is V22() real ext-real Element of REAL

((L | f) . N) - R is V22() real ext-real Element of REAL

].(((L | f) . N) - R),(((L | f) . N) + R).[ is open V84() V85() V86() V95() V96() V100() Element of K19(REAL)

{ b

N1 is V22() real ext-real Element of REAL

(L | f) . N1 is V22() real ext-real Element of REAL

f /\ (dom (L | f)) is Element of K19(f)

((L | f) . N) - (R / 2) is V22() real ext-real Element of REAL

(((L | f) . N) - R) + (R / 2) is V22() real ext-real Element of REAL

r2 is V22() real ext-real Element of REAL

(L | f) . r2 is V22() real ext-real Element of REAL

N - N1 is V22() real ext-real Element of REAL

r2 - N is V22() real ext-real Element of REAL

min ((r2 - N),(N - N1)) is V22() real ext-real set

N - (min ((r2 - N),(N - N1))) is V22() real ext-real set

N + (min ((r2 - N),(N - N1))) is V22() real ext-real set

].(N - (min ((r2 - N),(N - N1)))),(N + (min ((r2 - N),(N - N1)))).[ is open V84() V85() V86() V95() V96() V100() Element of K19(REAL)

{ b

r2 is open V84() V85() V86() Neighbourhood of N

N is V22() real ext-real set

s is open V84() V85() V86() Neighbourhood of N

(min ((r2 - N),(N - N1))) + N is V22() real ext-real set

x is V22() real ext-real Element of REAL

((min ((r2 - N),(N - N1))) + N) - N is V22() real ext-real set

N - N is V22() real ext-real set

N - N is V22() real ext-real set

x is V22() real ext-real Element of REAL

(r2 - N) + N is V22() real ext-real Element of REAL

(N - N) + N is V22() real ext-real set

(L | f) . N is V22() real ext-real Element of REAL

- (N - N) is V22() real ext-real set

- (N - N1) is V22() real ext-real Element of REAL

N1 - N is V22() real ext-real Element of REAL

(N1 - N) + N is V22() real ext-real Element of REAL

[.(((L | f) . N) - (R / 2)),(((L | f) . N) + (R / 2)).] is closed V84() V85() V86() V100() Element of K19(REAL)

{ b

f is set

L is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))

dom L is V84() V85() V86() Element of K19(REAL)

L | f is V1() V4( REAL ) V4(f) V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))

L .: f is V84() V85() V86() Element of K19(REAL)

r1 is V22() real ext-real Element of REAL

right_open_halfline r1 is open V84() V85() V86() Element of K19(REAL)

K195(r1,+infty) is V95() V96() V100() set

{ b

(L | f) | f is V1() V4( REAL ) V4(f) V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))

dom (L | f) is Element of K19(f)

K19(f) is set

N is V22() real ext-real set

(L | f) .: f is V84() V85() V86() Element of K19(REAL)

(dom L) /\ f is V84() V85() V86() Element of K19(REAL)

(L | f) . N is V22() real ext-real Element of REAL

r is open V84() V85() V86() Neighbourhood of (L | f) . N

r is open V84() V85() V86() Neighbourhood of (L | f) . N

fp is open V84() V85() V86() Neighbourhood of (L | f) . N

fm is V22() real ext-real set

((L | f) . N) - fm is V22() real ext-real Element of REAL

((L | f) . N) + fm is V22() real ext-real Element of REAL

].(((L | f) . N) - fm),(((L | f) . N) + fm).[ is open V84() V85() V86() V95() V96() V100() Element of K19(REAL)

{ b

R is V22() real ext-real Element of REAL

R / 2 is V22() real ext-real Element of REAL

((L | f) . N) + (R / 2) is V22() real ext-real Element of REAL

(((L | f) . N) + (R / 2)) + (R / 2) is V22() real ext-real Element of REAL

((L | f) . N) + R is V22() real ext-real Element of REAL

(((L | f) . N) + R) - R is V22() real ext-real Element of REAL

((L | f) . N) - R is V22() real ext-real Element of REAL

].(((L | f) . N) - R),(((L | f) . N) + R).[ is open V84() V85() V86() V95() V96() V100() Element of K19(REAL)

{ b

N1 is V22() real ext-real Element of REAL

(L | f) . N1 is V22() real ext-real Element of REAL

f /\ (dom (L | f)) is Element of K19(f)

((L | f) . N) - (R / 2) is V22() real ext-real Element of REAL

(((L | f) . N) - R) + (R / 2) is V22() real ext-real Element of REAL

r2 is V22() real ext-real Element of REAL

(L | f) . r2 is V22() real ext-real Element of REAL

N1 - N is V22() real ext-real Element of REAL

N - r2 is V22() real ext-real Element of REAL

min ((N - r2),(N1 - N)) is V22() real ext-real set

N - (min ((N - r2),(N1 - N))) is V22() real ext-real set

N + (min ((N - r2),(N1 - N))) is V22() real ext-real set

].(N - (min ((N - r2),(N1 - N)))),(N + (min ((N - r2),(N1 - N)))).[ is open V84() V85() V86() V95() V96() V100() Element of K19(REAL)

{ b

r2 is open V84() V85() V86() Neighbourhood of N

N is V22() real ext-real set

s is open V84() V85() V86() Neighbourhood of N

(min ((N - r2),(N1 - N))) + N is V22() real ext-real set

x is V22() real ext-real Element of REAL

((min ((N - r2),(N1 - N))) + N) - N is V22() real ext-real set

N - N is V22() real ext-real set

- (N - N) is V22() real ext-real set

- (N - r2) is V22() real ext-real Element of REAL

N - N is V22() real ext-real set

(N - N) + N is V22() real ext-real set

r2 - N is V22() real ext-real Element of REAL

(r2 - N) + N is V22() real ext-real Element of REAL

(L | f) . N is V22() real ext-real Element of REAL

x is V22() real ext-real Element of REAL

(N1 - N) + N is V22() real ext-real Element of REAL

[.(((L | f) . N) - (R / 2)),(((L | f) . N) + (R / 2)).] is closed V84() V85() V86() V100() Element of K19(REAL)

{ b

(L | f) | f is V1() V4( REAL ) V4(f) V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))

dom (L | f) is Element of K19(f)

K19(f) is set

N is V22() real ext-real set

(L | f) .: f is V84() V85() V86() Element of K19(REAL)

(dom L) /\ f is V84() V85() V86() Element of K19(REAL)

(L | f) . N is V22() real ext-real Element of REAL

r is open V84() V85() V86() Neighbourhood of (L | f) . N

r is open V84() V85() V86() Neighbourhood of (L | f) . N

fp is open V84() V85() V86() Neighbourhood of (L | f) . N

fm is V22() real ext-real set

((L | f) . N) - fm is V22() real ext-real Element of REAL

((L | f) . N) + fm is V22() real ext-real Element of REAL

].(((L | f) . N) - fm),(((L | f) . N) + fm).[ is open V84() V85() V86() V95() V96() V100() Element of K19(REAL)

{ b

R is V22() real ext-real Element of REAL

R / 2 is V22() real ext-real Element of REAL

((L | f) . N) + (R / 2) is V22() real ext-real Element of REAL

(((L | f) . N) + (R / 2)) + (R / 2) is V22() real ext-real Element of REAL

((L | f) . N) + R is V22() real ext-real Element of REAL

(((L | f) . N) + R) - R is V22() real ext-real Element of REAL

((L | f) . N) - R is V22() real ext-real Element of REAL

].(((L | f) . N) - R),(((L | f) . N) + R).[ is open V84() V85() V86() V95() V96() V100() Element of K19(REAL)

{ b

N1 is V22() real ext-real Element of REAL

(L | f) . N1 is V22() real ext-real Element of REAL

f /\ (dom (L | f)) is Element of K19(f)

((L | f) . N) - (R / 2) is V22() real ext-real Element of REAL

(((L | f) . N) - R) + (R / 2) is V22() real ext-real Element of REAL

r2 is V22() real ext-real Element of REAL

(L | f) . r2 is V22() real ext-real Element of REAL

N - N1 is V22() real ext-real Element of REAL

r2 - N is V22() real ext-real Element of REAL

min ((r2 - N),(N - N1)) is V22() real ext-real set

N - (min ((r2 - N),(N - N1))) is V22() real ext-real set

N + (min ((r2 - N),(N - N1))) is V22() real ext-real set

].(N - (min ((r2 - N),(N - N1)))),(N + (min ((r2 - N),(N - N1)))).[ is open V84() V85() V86() V95() V96() V100() Element of K19(REAL)

{ b

r2 is open V84() V85() V86() Neighbourhood of N

N is V22() real ext-real set

s is open V84() V85() V86() Neighbourhood of N

(min ((r2 - N),(N - N1))) + N is V22() real ext-real set

x is V22() real ext-real Element of REAL

((min ((r2 - N),(N - N1))) + N) - N is V22() real ext-real set

N - N is V22() real ext-real set

N - N is V22() real ext-real set

x is V22() real ext-real Element of REAL

(r2 - N) + N is V22() real ext-real Element of REAL

(N - N) + N is V22() real ext-real set

(L | f) . N is V22() real ext-real Element of REAL

- (N - N) is V22() real ext-real set

- (N - N1) is V22() real ext-real Element of REAL

N1 - N is V22() real ext-real Element of REAL

(N1 - N) + N is V22() real ext-real Element of REAL

[.(((L | f) . N) - (R / 2)),(((L | f) . N) + (R / 2)).] is closed V84() V85() V86() V100() Element of K19(REAL)

{ b

f is set

L is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))

dom L is V84() V85() V86() Element of K19(REAL)

L | f is V1() V4( REAL ) V4(f) V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))

L .: f is V84() V85() V86() Element of K19(REAL)

r1 is V22() real ext-real Element of REAL

left_closed_halfline r1 is closed V84() V85() V86() Element of K19(REAL)

K194(-infty,r1) is V95() V100() set

{ b

halfline r1 is open V84() V85() V86() Element of K19(REAL)

K195(-infty,r1) is V95() V96() V100() set

{ b

dom (L | f) is Element of K19(f)

K19(f) is set

r is V22() real ext-real set

(L | f) .: f is V84() V85() V86() Element of K19(REAL)

(dom L) /\ f is V84() V85() V86() Element of K19(REAL)

(L | f) . r is V22() real ext-real Element of REAL

{r1} is V84() V85() V86() set

{r1} \/ (halfline r1) is V84() V85() V86() set

(L | f) | f is V1() V4( REAL ) V4(f) V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))

fp is open V84() V85() V86() Neighbourhood of (L | f) . r

r is open V84() V85() V86() Neighbourhood of (L | f) . r

fm is open V84() V85() V86() Neighbourhood of (L | f) . r

R is V22() real ext-real set

((L | f) . r) - R is V22() real ext-real Element of REAL

((L | f) . r) + R is V22() real ext-real Element of REAL

].(((L | f) . r) - R),(((L | f) . r) + R).[ is open V84() V85() V86() V95() V96() V100() Element of K19(REAL)

{ b

N1 is V22() real ext-real Element of REAL

N1 / 2 is V22() real ext-real Element of REAL

((L | f) . r) + (N1 / 2) is V22() real ext-real Element of REAL

(((L | f) . r) + (N1 / 2)) + (N1 / 2) is V22() real ext-real Element of REAL

((L | f) . r) + N1 is V22() real ext-real Element of REAL

(((L | f) . r) + N1) - N1 is V22() real ext-real Element of REAL

((L | f) . r) - N1 is V22() real ext-real Element of REAL

].(((L | f) . r) - N1),(((L | f) . r) + N1).[ is open V84() V85() V86() V95() V96() V100() Element of K19(REAL)

{ b

x is V22() real ext-real Element of REAL

(L | f) . x is V22() real ext-real Element of REAL

f /\ (dom (L | f)) is Element of K19(f)

((L | f) . r) - (N1 / 2) is V22() real ext-real Element of REAL

(((L | f) . r) - N1) + (N1 / 2) is V22() real ext-real Element of REAL

s is V22() real ext-real Element of REAL

(L | f) . s is V22() real ext-real Element of REAL

x - r is V22() real ext-real Element of REAL

r - s is V22() real ext-real Element of REAL

min ((r - s),(x - r)) is V22() real ext-real set

r - (min ((r - s),(x - r))) is V22() real ext-real set

r + (min ((r - s),(x - r))) is V22() real ext-real set

].(r - (min ((r - s),(x - r)))),(r + (min ((r - s),(x - r)))).[ is open V84() V85() V86() V95() V96() V100() Element of K19(REAL)

{ b

s is open V84() V85() V86() Neighbourhood of r

x is V22() real ext-real set

N is open V84() V85() V86() Neighbourhood of r

(min ((r - s),(x - r))) + x is V22() real ext-real set

c

((min ((r - s),(x - r))) + x) - x is V22() real ext-real set

r - x is V22() real ext-real set

- (r - x) is V22() real ext-real set

- (r - s) is V22() real ext-real Element of REAL

x - r is V22() real ext-real set

(x - r) + r is V22() real ext-real set

s - r is V22() real ext-real Element of REAL

(s - r) + r is V22() real ext-real Element of REAL

(L | f) . x is V22() real ext-real Element of REAL

c

(x - r) + r is V22() real ext-real Element of REAL

[.(((L | f) . r) - (N1 / 2)),(((L | f) . r) + (N1 / 2)).] is closed V84() V85() V86() V100() Element of K19(REAL)

{ b

r is open V84() V85() V86() Neighbourhood of (L | f) . r

fp is V22() real ext-real set

r1 - fp is V22() real ext-real Element of REAL

r1 + fp is V22() real ext-real Element of REAL

].(r1 - fp),(r1 + fp).[ is open V84() V85() V86() V95() V96() V100() Element of K19(REAL)

{ b

fm is V22() real ext-real Element of REAL

fm / 2 is V22() real ext-real Element of REAL

r1 + (fm / 2) is V22() real ext-real Element of REAL

r1 - (fm / 2) is V22() real ext-real Element of REAL

{ b

N1 is V22() real ext-real Element of REAL

(L | f) . N1 is V22() real ext-real Element of REAL

f /\ (dom (L | f)) is Element of K19(f)

r - N1 is V22() real ext-real Element of REAL

r - (r - N1) is V22() real ext-real Element of REAL

r + (r - N1) is V22() real ext-real Element of REAL

].(r - (r - N1)),(r + (r - N1)).[ is open V84() V85() V86() V95() V96() V100() Element of K19(REAL)

{ b

N1 is open V84() V85() V86() Neighbourhood of r

r2 is V22() real ext-real set

x is open V84() V85() V86() Neighbourhood of r

r1 - fm is V22() real ext-real Element of REAL

(L | f) . r2 is V22() real ext-real Element of REAL

{ b

s is V22() real ext-real Element of REAL

s is V22() real ext-real Element of REAL

[.(r1 - (fm / 2)),(r1 + (fm / 2)).] is closed V84() V85() V86() V100() Element of K19(REAL)

{ b

r1 + fm is V22() real ext-real Element of REAL

].(r1 - fm),(r1 + fm).[ is open V84() V85() V86() V95() V96() V100() Element of K19(REAL)

{ b

r is open V84() V85() V86() Neighbourhood of (L | f) . r

r is open V84() V85() V86() Neighbourhood of (L | f) . r

fp is open V84() V85() V86() Neighbourhood of r

(L | f) | f is V1() V4( REAL ) V4(f) V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))

fp is open V84() V85() V86() Neighbourhood of (L | f) . r

r is open V84() V85() V86() Neighbourhood of (L | f) . r

fm is open V84() V85() V86() Neighbourhood of (L | f) . r

R is V22() real ext-real set

((L | f) . r) - R is V22() real ext-real Element of REAL

((L | f) . r) + R is V22() real ext-real Element of REAL

].(((L | f) . r) - R),(((L | f) . r) + R).[ is open V84() V85() V86() V95() V96() V100() Element of K19(REAL)

{ b

N1 is V22() real ext-real Element of REAL

N1 / 2 is V22() real ext-real Element of REAL

((L | f) . r) + (N1 / 2) is V22() real ext-real Element of REAL

(((L | f) . r) + (N1 / 2)) + (N1 / 2) is V22() real ext-real Element of REAL

((L | f) . r) + N1 is V22() real ext-real Element of REAL

(((L | f) . r) + N1) - N1 is V22() real ext-real Element of REAL

((L | f) . r) - N1 is V22() real ext-real Element of REAL

].(((L | f) . r) - N1),(((L | f) . r) + N1).[ is open V84() V85() V86() V95() V96() V100() Element of K19(REAL)

{ b

x is V22() real ext-real Element of REAL

(L | f) . x is V22() real ext-real Element of REAL

f /\ (dom (L | f)) is Element of K19(f)

((L | f) . r) - (N1 / 2) is V22() real ext-real Element of REAL

(((L | f) . r) - N1) + (N1 / 2) is V22() real ext-real Element of REAL

s is V22() real ext-real Element of REAL

(L | f) . s is V22() real ext-real Element of REAL

r - x is V22() real ext-real Element of REAL

s - r is V22() real ext-real Element of REAL

min ((s - r),(r - x)) is V22() real ext-real set

r - (min ((s - r),(r - x))) is V22() real ext-real set

r + (min ((s - r),(r - x))) is V22() real ext-real set

].(r - (min ((s - r),(r - x)))),(r + (min ((s - r),(r - x)))).[ is open V84() V85() V86() V95() V96() V100() Element of K19(REAL)

{ b

s is open V84() V85() V86() Neighbourhood of r

x is V22() real ext-real set

N is open V84() V85() V86() Neighbourhood of r

(min ((s - r),(r - x))) + x is V22() real ext-real set

c

((min ((s - r),(r - x))) + x) - x is V22() real ext-real set

r - x is V22() real ext-real set

x - r is V22() real ext-real set

c

(s - r) + r is V22() real ext-real Element of REAL

(x - r) + r is V22() real ext-real set

(L | f) . x is V22() real ext-real Element of REAL

- (r - x) is V22() real ext-real set

- (r - x) is V22() real ext-real Element of REAL

x - r is V22() real ext-real Element of REAL

(x - r) + r is V22() real ext-real Element of REAL

[.(((L | f) . r) - (N1 / 2)),(((L | f) . r) + (N1 / 2)).] is closed V84() V85() V86() V100() Element of K19(REAL)

{ b

r is open V84() V85() V86() Neighbourhood of (L | f) . r

fp is V22() real ext-real set

r1 - fp is V22() real ext-real Element of REAL

r1 + fp is V22() real ext-real Element of REAL

].(r1 - fp),(r1 + fp).[ is open V84() V85() V86() V95() V96() V100() Element of K19(REAL)

{ b

fm is V22() real ext-real Element of REAL

fm / 2 is V22() real ext-real Element of REAL

r1 + (fm / 2) is V22() real ext-real Element of REAL

r1 - (fm / 2) is V22() real ext-real Element of REAL

{ b

N1 is V22() real ext-real Element of REAL

(L | f) . N1 is V22() real ext-real Element of REAL

f /\ (dom (L | f)) is Element of K19(f)

N1 - r is V22() real ext-real Element of REAL

r - (N1 - r) is V22() real ext-real Element of REAL

r + (N1 - r) is V22() real ext-real Element of REAL

].(r - (N1 - r)),(r + (N1 - r)).[ is open V84() V85() V86() V95() V96() V100() Element of K19(REAL)

{ b

N1 is open V84() V85() V86() Neighbourhood of r

r2 is V22() real ext-real set

x is open V84() V85() V86() Neighbourhood of r

r1 - fm is V22() real ext-real Element of REAL

(L | f) . r2 is V22() real ext-real Element of REAL

{ b

s is V22() real ext-real Element of REAL

s is V22() real ext-real Element of REAL

[.(r1 - (fm / 2)),(r1 + (fm / 2)).] is closed V84() V85() V86() V100() Element of K19(REAL)

{ b

r1 + fm is V22() real ext-real Element of REAL

].(r1 - fm),(r1 + fm).[ is open V84() V85() V86() V95() V96() V100() Element of K19(REAL)

{ b

r is open V84() V85() V86() Neighbourhood of (L | f) . r

r is open V84() V85() V86() Neighbourhood of (L | f) . r

fp is open V84() V85() V86() Neighbourhood of r

r is open V84() V85() V86() Neighbourhood of (L | f) . r

r is open V84() V85() V86() Neighbourhood of (L | f) . r

fp is open V84() V85() V86() Neighbourhood of r

f is set

L is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))

dom L is V84() V85() V86() Element of K19(REAL)

L | f is V1() V4( REAL ) V4(f) V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))

L .: f is V84() V85() V86() Element of K19(REAL)

r1 is V22() real ext-real Element of REAL

right_closed_halfline r1 is closed V84() V85() V86() Element of K19(REAL)

K193(r1,+infty) is V96() V100() set

{ b

right_open_halfline r1 is open V84() V85() V86() Element of K19(REAL)

K195(r1,+infty) is V95() V96() V100() set

{ b

dom (L | f) is Element of K19(f)

K19(f) is set

r is V22() real ext-real set

(L | f) .: f is V84() V85() V86() Element of K19(REAL)

(dom L) /\ f is V84() V85() V86() Element of K19(REAL)

(L | f) . r is V22() real ext-real Element of REAL

{r1} is V84() V85() V86() set

{r1} \/ (right_open_halfline r1) is V84() V85() V86() set

(L | f) | f is V1() V4( REAL ) V4(f) V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))

fp is open V84() V85() V86() Neighbourhood of (L | f) . r

r is open V84() V85() V86() Neighbourhood of (L | f) . r

fm is open V84() V85() V86() Neighbourhood of (L | f) . r

R is V22() real ext-real set

((L | f) . r) - R is V22() real ext-real Element of REAL

((L | f) . r) + R is V22() real ext-real Element of REAL

].(((L | f) . r) - R),(((L | f) . r) + R).[ is open V84() V85() V86() V95() V96() V100() Element of K19(REAL)

{ b

N1 is V22() real ext-real Element of REAL

N1 / 2 is V22() real ext-real Element of REAL

((L | f) . r) + (N1 / 2) is V22() real ext-real Element of REAL

(((L | f) . r) + (N1 / 2)) + (N1 / 2) is V22() real ext-real Element of REAL

((L | f) . r) + N1 is V22() real ext-real Element of REAL

(((L | f) . r) + N1) - N1 is V22() real ext-real Element of REAL

((L | f) . r) - N1 is V22() real ext-real Element of REAL

].(((L | f) . r) - N1),(((L | f) . r) + N1).[ is open V84() V85() V86() V95() V96() V100() Element of K19(REAL)

{ b

x is V22() real ext-real Element of REAL

(L | f) . x is V22() real ext-real Element of REAL

f /\ (dom (L | f)) is Element of K19(f)

((L | f) . r) - (N1 / 2) is V22() real ext-real Element of REAL

(((L | f) . r) - N1) + (N1 / 2) is V22() real ext-real Element of REAL

s is V22() real ext-real Element of REAL

(L | f) . s is V22() real ext-real Element of REAL

x - r is V22() real ext-real Element of REAL

r - s is V22() real ext-real Element of REAL

min ((r - s),(x - r)) is V22() real ext-real set

r - (min ((r - s),(x - r))) is V22() real ext-real set

r + (min ((r - s),(x - r))) is V22() real ext-real set

].(r - (min ((r - s),(x - r)))),(r + (min ((r - s),(x - r)))).[ is open V84() V85() V86() V95() V96() V100() Element of K19(REAL)

{ b

s is open V84() V85() V86() Neighbourhood of r

x is V22() real ext-real set

N is open V84() V85() V86() Neighbourhood of r

(min ((r - s),(x - r))) + x is V22() real ext-real set

c

((min ((r - s),(x - r))) + x) - x is V22() real ext-real set

r - x is V22() real ext-real set

- (r - x) is V22() real ext-real set

- (r - s) is V22() real ext-real Element of REAL

x - r is V22() real ext-real set

(x - r) + r is V22() real ext-real set

s - r is V22() real ext-real Element of REAL

(s - r) + r is V22() real ext-real Element of REAL

(L | f) . x is V22() real ext-real Element of REAL

c

(x - r) + r is V22() real ext-real Element of REAL

[.(((L | f) . r) - (N1