let n be Nat; for r being Real
for p, p1, p2 being Point of (TOP-REAL n)
for u being Point of (Euclid n)
for f being Function of I[01],(TOP-REAL n) st f is continuous & f . 0 = p1 & f . 1 = p2 & p in Ball (u,r) & p2 in Ball (u,r) holds
ex h being Function of I[01],(TOP-REAL n) st
( h is continuous & h . 0 = p1 & h . 1 = p & rng h c= (rng f) \/ (Ball (u,r)) )
let r be Real; for p, p1, p2 being Point of (TOP-REAL n)
for u being Point of (Euclid n)
for f being Function of I[01],(TOP-REAL n) st f is continuous & f . 0 = p1 & f . 1 = p2 & p in Ball (u,r) & p2 in Ball (u,r) holds
ex h being Function of I[01],(TOP-REAL n) st
( h is continuous & h . 0 = p1 & h . 1 = p & rng h c= (rng f) \/ (Ball (u,r)) )
let p, p1, p2 be Point of (TOP-REAL n); for u being Point of (Euclid n)
for f being Function of I[01],(TOP-REAL n) st f is continuous & f . 0 = p1 & f . 1 = p2 & p in Ball (u,r) & p2 in Ball (u,r) holds
ex h being Function of I[01],(TOP-REAL n) st
( h is continuous & h . 0 = p1 & h . 1 = p & rng h c= (rng f) \/ (Ball (u,r)) )
let u be Point of (Euclid n); for f being Function of I[01],(TOP-REAL n) st f is continuous & f . 0 = p1 & f . 1 = p2 & p in Ball (u,r) & p2 in Ball (u,r) holds
ex h being Function of I[01],(TOP-REAL n) st
( h is continuous & h . 0 = p1 & h . 1 = p & rng h c= (rng f) \/ (Ball (u,r)) )
let f be Function of I[01],(TOP-REAL n); ( f is continuous & f . 0 = p1 & f . 1 = p2 & p in Ball (u,r) & p2 in Ball (u,r) implies ex h being Function of I[01],(TOP-REAL n) st
( h is continuous & h . 0 = p1 & h . 1 = p & rng h c= (rng f) \/ (Ball (u,r)) ) )
assume that
A1:
( f is continuous & f . 0 = p1 & f . 1 = p2 )
and
A2:
( p in Ball (u,r) & p2 in Ball (u,r) )
; ex h being Function of I[01],(TOP-REAL n) st
( h is continuous & h . 0 = p1 & h . 1 = p & rng h c= (rng f) \/ (Ball (u,r)) )
per cases
( p2 <> p or p2 = p )
;
suppose
p2 <> p
;
ex h being Function of I[01],(TOP-REAL n) st
( h is continuous & h . 0 = p1 & h . 1 = p & rng h c= (rng f) \/ (Ball (u,r)) )then
LSeg (
p2,
p)
is_an_arc_of p2,
p
by TOPREAL1:9;
then consider f1 being
Function of
I[01],
((TOP-REAL n) | (LSeg (p2,p))) such that A3:
f1 is
being_homeomorphism
and A4:
(
f1 . 0 = p2 &
f1 . 1
= p )
by TOPREAL1:def 1;
reconsider f2 =
f1 as
Function of
I[01],
(TOP-REAL n) by JORDAN6:3;
rng f1 = [#] ((TOP-REAL n) | (LSeg (p2,p)))
by A3;
then
rng f2 = LSeg (
p2,
p)
by PRE_TOPC:def 5;
then A5:
(rng f) \/ (rng f2) c= (rng f) \/ (Ball (u,r))
by A2, TOPREAL3:21, XBOOLE_1:9;
f1 is
continuous
by A3;
then
f2 is
continuous
by JORDAN6:3;
then
ex
h3 being
Function of
I[01],
(TOP-REAL n) st
(
h3 is
continuous &
p1 = h3 . 0 &
p = h3 . 1 &
rng h3 c= (rng f) \/ (rng f2) )
by A1, A4, BORSUK_2:13;
hence
ex
h being
Function of
I[01],
(TOP-REAL n) st
(
h is
continuous &
h . 0 = p1 &
h . 1
= p &
rng h c= (rng f) \/ (Ball (u,r)) )
by A5, XBOOLE_1:1;
verum end; end;