let n be Element of NAT ; :: thesis: for r being Real
for p1, p2, p 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; :: thesis: for p1, p2, p 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 p1, p2, p be Point of (TOP-REAL n); :: thesis: 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); :: thesis: 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); :: thesis: ( 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 A1:
( f is continuous & f . 0 = p1 & f . 1 = p2 & p in Ball u,r & p2 in Ball u,r )
; :: thesis: 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
;
:: thesis: 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:15;
then consider f1 being
Function of
I[01] ,
((TOP-REAL n) | (LSeg p2,p)) such that A2:
(
f1 is
being_homeomorphism &
f1 . 0 = p2 &
f1 . 1
= p )
by TOPREAL1:def 2;
A3:
(
dom f1 = [#] I[01] &
rng f1 = [#] ((TOP-REAL n) | (LSeg p2,p)) &
f1 is
one-to-one &
f1 is
continuous &
f1 " is
continuous )
by A2, TOPS_2:def 5;
reconsider f2 =
f1 as
Function of
I[01] ,
(TOP-REAL n) by JORDAN6:4;
A4:
f2 is
continuous
by A3, JORDAN6:4;
A5:
rng f2 = LSeg p2,
p
by A3, PRE_TOPC:def 10;
consider h3 being
Function of
I[01] ,
(TOP-REAL n) such that A6:
(
h3 is
continuous &
p1 = h3 . 0 &
p = h3 . 1 &
rng h3 c= (rng f) \/ (rng f2) )
by A1, A2, A4, BORSUK_2:16;
(rng f) \/ (rng f2) c= (rng f) \/ (Ball u,r)
by A1, A5, TOPREAL3:28, XBOOLE_1:9;
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 A6, XBOOLE_1:1;
:: thesis: verum end; end;